---

Step * 1 of Lemma rdiv-int-fractions


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))
BY
{ (Assert r(c * b) ≠ r0 BY
         Auto) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  c  :  \mBbbN{}\msupplus{}
4.  d  :  \mBbbN{}\msupplus{}
5.  [\%]  :  \mneg{}(b  =  0)
6.  (r(b)/r(d))  \mneq{}  r0
\mvdash{}  ((r(a)/r(c))/(r(b)/r(d)))  =  (r(a  *  d)/r(c  *  b))


By

---

Latex:
(Assert  r(c  *  b)  \mneq{}  r0  BY
              Auto)

---

Home Index