---

Step * 1 2 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
⊢ ∃m:ℕ+. ((1/m) ≤ (p/q))
BY
{ xxxxxxCaseNat 1 `p'xxxxxx }

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. p = 1 ∈ ℤ
⊢ ∃m:ℕ+. ((1/m) ≤ (1/q))

2
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. ¬(p = 1 ∈ ℤ)
⊢ ∃m:ℕ+. ((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
\mvdash{}  \mexists{}m:\mBbbN{}\msupplus{}.  ((1/m)  \mleq{}  (p/q))


By

---

Latex:
xxxxxxCaseNat  1  `p'xxxxxx

---

Home Index