---

Step * 1 2 2 1 1 2 1 of Lemma reciprocal-qle-proof


1. e : ℚ
2. 0 < e
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. e = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. 0 < p
10. q = (((q ÷ p) * p) + (q rem p)) ∈ ℤ
11. 0 ≤ (q rem p)
12. q rem p < p
13. 0 ≤ (q ÷ p)
14. m : ℕ+
15. ((q ÷ p) + 1) = m ∈ ℕ+
16. q < m * p
⊢ (1/m) ≤ (p/q)
BY
{ (QMul ⌜m⌝ 0⋅ THEN Auto) }

1
1. e : ℚ
2. 0 < e
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. e = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. 0 < p
10. q = (((q ÷ p) * p) + (q rem p)) ∈ ℤ
11. 0 ≤ (q rem p)
12. q rem p < p
13. 0 ≤ (q ÷ p)
14. m : ℕ+
15. ((q ÷ p) + 1) = m ∈ ℕ+
16. q < m * p
⊢ 1 ≤ (m * (p/q))

---

Latex:

---

Latex:

1.  e  :  \mBbbQ{}
2.  0  <  e
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  e  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  0  <  p
10.  q  =  (((q  \mdiv{}  p)  *  p)  +  (q  rem  p))
11.  0  \mleq{}  (q  rem  p)
12.  q  rem  p  <  p
13.  0  \mleq{}  (q  \mdiv{}  p)
14.  m  :  \mBbbN{}\msupplus{}
15.  ((q  \mdiv{}  p)  +  1)  =  m
16.  q  <  m  *  p
\mvdash{}  (1/m)  \mleq{}  (p/q)


By

---

Latex:
(QMul  \mkleeneopen{}m\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index