---

Step * of Lemma rdiv-int-fractions

∀a,b:ℤ. ∀c,d:ℕ+.  ((r(a)/r(c))/(r(b)/r(d))) = (r(a * d)/r(c * b)) supposing ¬(b = 0 ∈ ℤ)
BY
{ (Intros THEN (Assert (r(b)/r(d)) ≠ r0 BY (nRMul ⌜r(d)⌝ 0⋅ THEN Auto))) }

1
1. a : ℤ
2. b : ℤ
3. c : ℕ+
4. d : ℕ+
5. [%] : ¬(b = 0 ∈ ℤ)
6. (r(b)/r(d)) ≠ r0
⊢ ((r(a)/r(c))/(r(b)/r(d))) = (r(a * d)/r(c * b))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.  \mforall{}c,d:\mBbbN{}\msupplus{}.    ((r(a)/r(c))/(r(b)/r(d)))  =  (r(a  *  d)/r(c  *  b))  supposing  \mneg{}(b  =  0)


By

---

Latex:
(Intros  THEN  (Assert  (r(b)/r(d))  \mneq{}  r0  BY  (nRMul  \mkleeneopen{}r(d)\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index