---

Step * of Lemma implies-equal-div2

No Annotations
∀[a,c:ℤ]. ∀[b:ℤ-o].  (a ÷ b) = c ∈ ℤ supposing a = (b * c) ∈ ℤ
BY
{ (Auto THEN (InstLemma `implies-equal-div` [⌜a⌝;⌜c⌝;⌜b⌝;⌜1⌝]⋅ THEN Auto) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,c:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (a  \mdiv{}  b)  =  c  supposing  a  =  (b  *  c)


By

---

Latex:
(Auto  THEN  (InstLemma  `implies-equal-div`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index