---

Step * 1 of Lemma rleq-rat2real


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))
BY
{ ((RWO "int-rdiv-req" 0 THENA Auto) THEN RWO "rleq-int-fractions" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  q1  :  \mBbbQ{}
2.  q2  :  \mBbbQ{}
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  q2  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  p1  :  \mBbbZ{}
10.  q3  :  \mBbbZ{}
11.  0  <  q3
12.  \mneg{}(q3  =  0)
13.  q1  =  (p1/q3)
14.  \mneg{}\muparrow{}qeq(q3;0)
\mvdash{}  uiff((r(p1))/q3  \mleq{}  (r(p))/q;(p1  *  q)  \mleq{}  (q3  *  p))


By

---

Latex:
((RWO  "int-rdiv-req"  0  THENA  Auto)  THEN  RWO  "rleq-int-fractions"  0  THEN  Auto)

---

Home Index