---

Step * 1 2 of Lemma small-reciprocal-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
{ xxx((InstLemma `div_rem_sum` [⌜q⌝;⌜p⌝]⋅ THENA Auto)
      THEN (InstLemma `rem_bounds_1` [⌜q⌝;⌜p⌝]⋅ THENA Auto)
      THEN (InstLemma `div_bounds_1` [⌜q⌝;⌜p⌝]⋅ THENA Auto)
      THEN With ⌜(q ÷ p) + 1⌝ (D 0)⋅
      THEN Auto)xxx }

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)
⊢ (1/(q ÷ p) + 1) < (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)  <  (p/q)


By

---

Latex:
xxx((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  With  \mkleeneopen{}(q  \mdiv{}  p)  +  1\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto)xxx

---

Home Index