---

Step * of Lemma qexp-greater-one

∀e:{e:ℚ| 0 < e} . ∀r:{r:ℚ| 1 + e < r} . ∀n:ℕ.  1 + (n * e) < r ↑ n supposing 1 ≤ n
BY
{ xxx(InductionOnNat THEN Auto THEN ∀h:hyp. DSet h  THEN Unhide THEN Auto)xxx }

1
1. e : ℚ
2. 0 < e
3. r : ℚ
4. 1 + e < r
5. n : ℤ
6. 0 < n
7. 1 + ((n - 1) * e) < r ↑ n - 1 supposing 1 ≤ (n - 1)
8. 1 ≤ n
⊢ 1 + (n * e) < r ↑ n

---

Latex:

---

Latex:
\mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .  \mforall{}r:\{r:\mBbbQ{}|  1  +  e  <  r\}  .  \mforall{}n:\mBbbN{}.    1  +  (n  *  e)  <  r  \muparrow{}  n  supposing  1  \mleq{}  n


By

---

Latex:
xxx(InductionOnNat  THEN  Auto  THEN  \mforall{}h:hyp.  DSet  h    THEN  Unhide  THEN  Auto)xxx

---

Home Index