---

Step * of Lemma rat2real-qmul

No Annotations
∀[a,b:ℚ].  (rat2real(a * b) = (rat2real(a) * rat2real(b)))
BY
{ (Auto
   THEN (ElimRationals THENA Auto)
   THEN (RWO "mk-rational-qdiv<" 0 THENA Auto)
   THEN RepUR ``qmul mk-rational`` 0
   THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0))
   THEN RepUR ``rat2real`` 0) }

1
1. a : ℚ
2. b : ℚ
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. b = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. p1 : ℤ
10. q1 : ℤ
11. 0 < q1
12. ¬(q1 = 0 ∈ ℚ)
13. a = (p1/q1) ∈ ℚ
14. ¬↑qeq(q1;0)
⊢ (r(p1 * p))/q1 * q = ((r(p1))/q1 * (r(p))/q)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbQ{}].    (rat2real(a  *  b)  =  (rat2real(a)  *  rat2real(b)))


By

---

Latex:
(Auto
  THEN  (ElimRationals  THENA  Auto)
  THEN  (RWO  "mk-rational-qdiv<"  0  THENA  Auto)
  THEN  RepUR  ``qmul  mk-rational``  0
  THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
  THEN  RepUR  ``rat2real``  0)

---

Home Index