---

Step * 1 2 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 ∈ ℤ)
⊢ x * x^(n + 1) - 1 < y * y^(n + 1) - 1
BY
{ (InstLemma `mul_preserves_lt` [x^n;y^n;⌜x⌝]⋅ THEN Auto THEN InstLemma `mul_preserves_lt` [x;y;⌜y^n⌝]⋅ THEN Auto)⋅ }

---

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


By

---

Latex:
(InstLemma  `mul\_preserves\_lt`  [x\^{}n;y\^{}n;\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `mul\_preserves\_lt`  [x;y;\mkleeneopen{}y\^{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index