Theorem nummult-ls-02

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: div-ls-mone, div-mult-two-nls-01, div-two-intro, div-twoodd-05, mod-zero-06, nummult-ls-02-01,
• Used by units in proved state: int-pot, int-gcd,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 5
• Used lemmas: div-elim-pospos, mult-ls,
• Used spec theorems:
  • int-mult/numls-02
• Used simplifier rules:
  • int-abs/forward-le-05
  • int-abs/lels
  • int-abs/forward-le-01
  • int-abs/forward-lsle
  • int-abs/zero-gels-04
  • int-mult/zero-ge-add
  • int-abs/forward-lels
  • int-mult/zero-gr
  • int-abs/sub-ls-01
  • int-basic2/add-zero-rev
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/lenls
  • int-mult/associativity
  • int-mult/commutativity