---

Step * of Lemma rleq-rat2real

∀[q1,q2:ℚ].  uiff(rat2real(q1) ≤ rat2real(q2);q1 ≤ q2)
BY
{ ((UnivCD THENA Auto)
   THEN (ElimRationals THENA Auto)
   THEN (RWO "mk-rational-qdiv<" 0 THENA Auto)
   THEN (RWO "qle-mk-rational" 0 THENA Auto)
   THEN RepUR ``mk-rational rat2real`` 0) }

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

---

Latex:

---

Latex:
\mforall{}[q1,q2:\mBbbQ{}].    uiff(rat2real(q1)  \mleq{}  rat2real(q2);q1  \mleq{}  q2)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (ElimRationals  THENA  Auto)
  THEN  (RWO  "mk-rational-qdiv<"  0  THENA  Auto)
  THEN  (RWO  "qle-mk-rational"  0  THENA  Auto)
  THEN  RepUR  ``mk-rational  rat2real``  0)

---

Home Index