---

Step * 1 1 of Lemma rdiv-int-fractions


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))
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN GenConclTerms Auto [⌜(r(b)/r(d))⌝;⌜r(c * b)⌝]⋅) }

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

---

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
7.  r(c  *  b)  \mneq{}  r0
\mvdash{}  ((r(a)/r(c))/(r(b)/r(d)))  =  (r(a  *  d)/r(c  *  b))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  GenConclTerms  Auto  [\mkleeneopen{}(r(b)/r(d))\mkleeneclose{};\mkleeneopen{}r(c  *  b)\mkleeneclose{}]\mcdot{})

---

Home Index