---

Step * 1 of Lemma exp_preserves_le


1. n : ℤ
2. n ≠ 0
3. 0 < n
4. ∀[x,y:ℕ].  x^n - 1 ≤ y^n - 1 supposing x ≤ y
5. x : ℕ
6. y : ℕ
7. x ≤ y
⊢ (x * x^n - 1) ≤ (y * y^n - 1)
BY
{ ((Assert x^n - 1 ≤ y^n - 1 BY
          Auto)
   THEN InstLemma `mul_preserves_le` [x^n - 1;y^n - 1;⌜x⌝]⋅
   THEN Auto
   THEN InstLemma `mul_preserves_le` [x;y;⌜y^n - 1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  x\^{}n  -  1  \mleq{}  y\^{}n  -  1  BY
                Auto)
  THEN  InstLemma  `mul\_preserves\_le`  [x\^{}n  -  1;y\^{}n  -  1;\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `mul\_preserves\_le`  [x;y;\mkleeneopen{}y\^{}n  -  1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index