Theorem nummult-ls

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: div-div-pred, div-div-pred-01, div-mult-three, div-two-intro, div-twoodd-03, div2-nls-02, even-not-ex, mod-two-pred-01, nummult-ls-04,
• Used by units in proved state: int-pot, int-square,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 6
• Proof steps: 19
• Used lemmas: div-elim-pos,
• Used spec theorems:
  • int-mult/modlep
• Used simplifier rules:
  • int-abs/forward-le-04
  • int-basic2/ls
  • int-abs/forward-lele
  • int-abs/lels-03
  • int-mult/eq-succ
  • int-abs/lels
  • int-mult/zero-ge-add
  • int-abs/forward-le-05
  • int-basic1/lf-02
  • int-abs/leone
  • int-abs/sub-le-01
  • int-abs/sub-eq
  • int-abs/zero-gels-04
  • int-mult/zero-ge
  • int-abs/forward-le-01
  • int-abs/forward-lels
  • int-abs/succ-01
  • int-basic2/add-in
  • int-basic2/add-zero-rev
  • int-abs/numadd
  • int-mult/eq-dist
  • int-mult/one
  • int-mult/associativity
  • int-mult/commutativity
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/succ-02
  • int-abs/numls-02
  • int-abs/mone-06
  • int-abs/numle-02
  • int-abs/numleledel-01
  • int-mult/mods-ls-04
  • int-abs/lenls
  • int-abs/elim-sub