---

Step * 1 of Lemma exp_preserves_lt


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
BY
{ CaseNat 0 `x' }

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
8. x = 0 ∈ ℤ
⊢ 0 * 0^(n + 1) - 1 < y * y^(n + 1) - 1

2
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
8. ¬(x = 0 ∈ ℤ)
⊢ x * x^(n + 1) - 1 < y * y^(n + 1) - 1

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  0  <  n
3.  \mforall{}[x,y:\mBbbN{}].    x\^{}n  <  y\^{}n  supposing  x  <  y@i
4.  x  :  \mBbbN{}
5.  y  :  \mBbbN{}
6.  x  <  y
7.  x\^{}n  <  y\^{}n
\mvdash{}  x  *  x\^{}(n  +  1)  -  1  <  y  *  y\^{}(n  +  1)  -  1


By

---

Latex:
CaseNat  0  `x'

---

Home Index