---

Step * of Lemma exp_preserves_lt

∀[n:ℕ+]. ∀[x,y:ℕ].  x^n < y^n supposing x < y
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN RWO "exp1 exp_step" 0
   THEN Auto
   THEN (Assert x^n < y^n BY
               (BackThruSomeHyp THEN Auto))) }

1
1. n : ℤ@i
2. 0 < n
3. ∀[x,y:ℕ].  x^n < y^n supposing x < y@i
4. x : ℕ
5. y : ℕ
6. x < y
7. x^n < y^n
⊢ x * x^(n + 1) - 1 < y * y^(n + 1) - 1

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x,y:\mBbbN{}].    x\^{}n  <  y\^{}n  supposing  x  <  y


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "exp1  exp\_step"  0
  THEN  Auto
  THEN  (Assert  x\^{}n  <  y\^{}n  BY
                          (BackThruSomeHyp  THEN  Auto)))

---

Home Index