---

Step * of Lemma exp_difference_bound

∀[n:ℕ+]. ∀[M:ℕ]. ∀[x,y:ℤ].  |x^n - y^n| ≤ ((n * M^n - 1) * |x - y|) supposing (|x| ≤ M) ∧ (|y| ≤ M)
BY
{ (Auto
   THEN (RWW "exp_difference_factor absval_mul" 0 THENA Auto)
   THEN (RWO "mul_com" 0 THENA Auto)
   THEN BLemma `mul_preserves_le`
   THEN Auto) }

1
1. n : ℕ+
2. M : ℕ
3. x : ℤ
4. y : ℤ
5. |x| ≤ M
6. |y| ≤ M
⊢ |Σ(x^n - i + 1 * y^i | i < n)| ≤ (n * M^n - 1)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[M:\mBbbN{}].  \mforall{}[x,y:\mBbbZ{}].    |x\^{}n  -  y\^{}n|  \mleq{}  ((n  *  M\^{}n  -  1)  *  |x  -  y|)  supposing  (|x|  \mleq{}  M)  \mwedge{}  (|y|  \mleq{}  M)


By

---

Latex:
(Auto
  THEN  (RWW  "exp\_difference\_factor  absval\_mul"  0  THENA  Auto)
  THEN  (RWO  "mul\_com"  0  THENA  Auto)
  THEN  BLemma  `mul\_preserves\_le`
  THEN  Auto)

---

Home Index