---

Step * of Lemma exp-convex

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

1
1. a : ℕ
2. b : ℕ
3. c : ℕ
4. n : ℤ
5. 0 < n
6. |a - b| ≤ c supposing |a^n - b^n| ≤ c^n
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:
xxx(RepeatFor  3  ((D  0  THENA  Auto))
        THEN  xxx(InductionOnNat
                          THEN  RWW  "exp1"  0
                          THEN  Auto
                          THEN  (RWO  "exp\_step"  (-1)  THENA  Auto)
                          THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  -1  THENA  Auto))xxx
        )xxx

---

Home Index