---

Step * of Lemma exp-convex

∀[a,b,c:ℕ]. ∀[n:ℕ+].  |a - b| ≤ c supposing |a^n - b^n| ≤ c^n
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (InductionOnNat
         THEN RWW "exp1" 0
         THEN Auto
         THEN (RWO "exp_step" (-1) THENA Auto)
         THEN (Subst' (n + 1) - 1 ~ n -1 THENA Auto))
   ) }

1
1. a : ℕ
2. b : ℕ
3. c : ℕ
4. n : ℤ@i
5. 0 < n
6. |a - b| ≤ c supposing |a^n - b^n| ≤ c^n@i
7. |(a * a^n) - b * b^n| ≤ (c * c^n)
⊢ |a - b| ≤ c

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    |a  -  b|  \mleq{}  c  supposing  |a\^{}n  -  b\^{}n|  \mleq{}  c\^{}n


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (InductionOnNat
              THEN  RWW  "exp1"  0
              THEN  Auto
              THEN  (RWO  "exp\_step"  (-1)  THENA  Auto)
              THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  -1  THENA  Auto))
  )

---

Home Index