---

Step * of Lemma rpower-greater-one

∀x,q:ℝ.  ((r0 < x) ⇒ ((r1 + x) < q) ⇒ (∀n:ℕ. (r1 + (r(n) * x)) < q^n supposing 1 < n))
BY
{ ((InductionOnNat THEN Auto)
   THEN (Assert r0 ≤ r1 BY
               Auto)
   THEN (Assert r0 ≤ (r1 + x) BY
               (nRAdd ⌜x⌝ (-1)⋅ THEN Auto))
   THEN CaseNat 2 `n') }

1
1. x : ℝ
2. q : ℝ
3. r0 < x
4. (r1 + x) < q
5. n : ℤ
6. [%3] : 0 < n
7. (r1 + (r(n - 1) * x)) < q^n - 1 supposing 1 < n - 1
8. 1 < n
9. r0 ≤ r1
10. r0 ≤ (r1 + x)
11. n = 2 ∈ ℤ
⊢ (r1 + (r(2) * x)) < q^2

2
1. x : ℝ
2. q : ℝ
3. r0 < x
4. (r1 + x) < q
5. n : ℤ
6. [%3] : 0 < n
7. (r1 + (r(n - 1) * x)) < q^n - 1 supposing 1 < n - 1
8. 1 < n
9. r0 ≤ r1
10. r0 ≤ (r1 + x)
11. ¬(n = 2 ∈ ℤ)
⊢ (r1 + (r(n) * x)) < q^n

---

Latex:

---

Latex:
\mforall{}x,q:\mBbbR{}.    ((r0  <  x)  {}\mRightarrow{}  ((r1  +  x)  <  q)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (r1  +  (r(n)  *  x))  <  q\^{}n  supposing  1  <  n))


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  (Assert  r0  \mleq{}  r1  BY
                          Auto)
  THEN  (Assert  r0  \mleq{}  (r1  +  x)  BY
                          (nRAdd  \mkleeneopen{}x\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  CaseNat  2  `n')

---

Home Index