---

Step * of Lemma implies-equal-div

No Annotations
∀[a,c:ℤ]. ∀[b,d:ℤ-o].  (a ÷ b) = (c ÷ d) ∈ ℤ supposing (d * a) = (b * c) ∈ ℤ
BY
{ (Auto
   THEN (InstLemma `div_rem_sum` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (Mul ⌜d⌝ (-1)⋅ THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜c⌝;⌜d⌝]⋅ THENA Auto)
   THEN (Mul ⌜b⌝ (-1)⋅ THENA Auto)
   THEN Mul ⌜b * d⌝ 0⋅) }

1
1. a : ℤ
2. c : ℤ
3. b : ℤ-o
4. d : ℤ-o
5. (d * a) = (b * c) ∈ ℤ
6. a = (((a ÷ b) * b) + (a rem b)) ∈ ℤ
7. (d * a) = (d * (((a ÷ b) * b) + (a rem b))) ∈ ℤ
8. c = (((c ÷ d) * d) + (c rem d)) ∈ ℤ
9. (b * c) = (b * (((c ÷ d) * d) + (c rem d))) ∈ ℤ
⊢ ((b * d) * (a ÷ b)) = ((b * d) * (c ÷ d)) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Mul  \mkleeneopen{}d\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Mul  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Mul  \mkleeneopen{}b  *  d\mkleeneclose{}  0\mcdot{})

---

Home Index