Theorem zero-ls-02

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by: abs-eqall, abs-ls-same, abs-not-neg, mods-zero-07, square-abs, square-interval, square-lez, square-zero-01a, square-zero-02, twice-ls-zero, zero-ge-02, zero-ge-add-01, zero-ls-case,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 2
• Used lemmas: mult-com, mult-ass, zero-ls, mult-zero,
• Used spec theorems:
  • Used simplifier rules:
    • real-abs/lels-02
    • real-abs/lels
    • real-abs/lels-03
    • real-abs/forward-lsle
    • real-abs/zero-gels-01
    • real-basic/ls-num