---

Step * 1 of Lemma rnexp-rless


1. x : ℝ
2. y : ℝ
3. r0 ≤ x
4. x < y
⊢ ∀n:ℕ+. (x^n < y^n)
BY
{ ((InductionOnNat THEN Auto)
   THEN RWO "rnexp_unroll" 0
   THEN Auto
   THEN AutoSplit
   THEN Thin (-3)
   THEN (Subst' (n + 1) - 1 ~ n 0 THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. r0 ≤ x
4. x < y
5. n : ℤ
6. 0 < n
7. x^n < y^n
⊢ (x^n * x) < (y^n * y)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  r0  \mleq{}  x
4.  x  <  y
\mvdash{}  \mforall{}n:\mBbbN{}\msupplus{}.  (x\^{}n  <  y\^{}n)


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  RWO  "rnexp\_unroll"  0
  THEN  Auto
  THEN  AutoSplit
  THEN  Thin  (-3)
  THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto))

---

Home Index