Theorem mod-by6

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 8
• Proof steps: 16
• Used lemmas: mod-zero-num, mod-add1-pospos, modby6-help,
• Used spec theorems:
  • int-mult/zero-ls
• Used simplifier rules:
  • int-abs/mone-08
  • int-abs/zero-gels-04
  • int-abs/zero-gels-01
  • int-basic2/succ-01
  • int-abs/forward-le-02
  • int-basic1/lf-02
  • int-basic1/trans
  • int-basic1/lf-01
  • int-abs/lels-02
  • int-mult/zero-ge-02
  • int-mult/square-gez
  • int-mult/zero-ge
  • int-basic2/zero-02
  • int-mult/modzero
  • int-mult/commutativity
  • int-basic1/ls-01
  • int-abs/lels-01
  • int-abs/forward-le-05
  • int-abs/leone
  • int-abs/sub-le-01
  • int-abs/Sub-def
  • int-abs/sub-pred
  • int-abs/elim-sub
  • int-abs/forward-le-01
  • int-abs/numleledel-01
  • int-abs/numle-02
  • int-abs/mone-06
  • int-abs/numls-02
  • int-mult/associativity
  • int-basic2/add-c
  • int-basic2/add-a