Theorem mod-mult-add

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: cong-mult, congmod-def-mod, congmod-inverse-smallest, mod-add-law, mod-mult-add-01, mod-mult-law, rem-mod-pos,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 11
• Proof steps: 20
• Used lemmas: mod-plus, mod-rec-plus, mod-rec-any,
• Used spec theorems:
  • Used simplifier rules:
    • int-abs/forward-le-05
    • int-abs/sub-ls-01
    • int-abs/bet
    • int-mult/one-01
    • int-abs/sub-add
    • intnat/abs-pred
    • int-abs/lels-03
    • int-basic2/add-in
    • int-abs/sub-eq
    • int-mult/eq-dist
    • int-mult/one
    • int-abs/forward-le-04
    • int-abs/forward-lels
    • intnat/abs-succ-01
    • int-abs/anti
    • int-abs/mone-05
    • int-abs/numle-03
    • int-abs/lels-02
    • int-abs/zero-gels-01
    • int-abs/lels
    • int-abs/les
    • int-abs/forward-le-02
    • int-abs/succ-02
    • int-abs/ler
    • int-abs/numls-02
    • int-abs/mone-06
    • int-basic1/ls-01
    • int-mult/Mult-zero
    • int-basic2/add-zero
    • int-mult/eq-succ
    • int-basic2/add-a
    • int-basic2/add-c
    • int-mult/associativity
    • int-mult/commutativity
    • int-abs/elim-sub