---

Step * of Lemma rat2real-qadd

∀[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 ``qadd 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 * q) + (p * q1)))/q1 * q = ((r(p1))/q1 + (r(p))/q)

---

Latex:

---

Latex:
\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  ``qadd  mk-rational``  0
  THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
  THEN  RepUR  ``rat2real``  0)

---

Home Index