---

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

---

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
8.  x  =  0
\mvdash{}  0  *  0\^{}(n  +  1)  -  1  <  y  *  y\^{}(n  +  1)  -  1


By

---

Latex:
(RW  IntNormC  0  THENA  Auto)

---

Home Index