---

Step * 1 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 < y * y^n
BY
{ EAuto 2 }

---

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  <  y  *  y\^{}n


By

---

Latex:
EAuto  2

---

Home Index