---

Step * 1 1 2 2 1 1 1 of Lemma qlog-exists


1. q : ℚ
2. 0 ≤ q
3. q < 1
4. n : ℕ
5. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
6. e : ℚ
7. 0 < e
8. e ≤ 1
9. e ≤ q
10. n1 : ℤ
11. ¬n1 < n
12. 0 ≤ n1
13. n2 : ℚ
14. n2 = q ↑ n1 ∈ ℚ
15. e ≤ n2
16. n2 * n2 < e
17. ¬(n1 = 1 ∈ ℤ)
18. ¬(n1 = 0 ∈ ℤ)
19. 0 < n2
20. q ↑ n1 - n * q ↑ n < q ↑ n1 - n * e
⊢ n1 < n
BY
{ (RWO "qexp-add<" (-1) THENA Auto') }

1
1. q : ℚ
2. 0 ≤ q
3. q < 1
4. n : ℕ
5. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
6. e : ℚ
7. 0 < e
8. e ≤ 1
9. e ≤ q
10. n1 : ℤ
11. ¬n1 < n
12. 0 ≤ n1
13. n2 : ℚ
14. n2 = q ↑ n1 ∈ ℚ
15. e ≤ n2
16. n2 * n2 < e
17. ¬(n1 = 1 ∈ ℤ)
18. ¬(n1 = 0 ∈ ℤ)
19. 0 < n2
20. q ↑ (n1 - n) + n < q ↑ n1 - n * e
⊢ n1 < n

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  0  \mleq{}  q
3.  q  <  1
4.  n  :  \mBbbN{}
5.  \mforall{}[m:\mBbbN{}n].  \mforall{}e:\{e:\mBbbQ{}|  0  <  e  \mwedge{}  (e  \mleq{}  1)  \mwedge{}  q  \muparrow{}  m  <  e\}  .  \{n:\mBbbN{}\msupplus{}|  (e  \mleq{}  q  \muparrow{}  n  -  1)  \mwedge{}  q  \muparrow{}  n  <  e\} 
6.  e  :  \mBbbQ{}
7.  0  <  e
8.  e  \mleq{}  1
9.  e  \mleq{}  q
10.  n1  :  \mBbbZ{}
11.  \mneg{}n1  <  n
12.  0  \mleq{}  n1
13.  n2  :  \mBbbQ{}
14.  n2  =  q  \muparrow{}  n1
15.  e  \mleq{}  n2
16.  n2  *  n2  <  e
17.  \mneg{}(n1  =  1)
18.  \mneg{}(n1  =  0)
19.  0  <  n2
20.  q  \muparrow{}  n1  -  n  *  q  \muparrow{}  n  <  q  \muparrow{}  n1  -  n  *  e
\mvdash{}  n1  <  n


By

---

Latex:
(RWO  "qexp-add<"  (-1)  THENA  Auto')

---

Home Index