---

Step * of Lemma exp-convex2

∀[a,b:ℤ]. ∀[c:ℕ]. ∀[n:ℕ+].  |a - b| ≤ c supposing (|a^n - b^n| ≤ c^n) ∧ (0 ≤ a ⇐⇒ 0 ≤ b)
BY
{ TACTIC:Auto }

1
1. a : ℤ
2. b : ℤ
3. c : ℕ
4. n : ℕ+
5. |a^n - b^n| ≤ c^n
6. (0 ≤ a) ⇒ (0 ≤ b)
7. (0 ≤ a) ⇐ 0 ≤ b
⊢ |a - b| ≤ c

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[c:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    |a  -  b|  \mleq{}  c  supposing  (|a\^{}n  -  b\^{}n|  \mleq{}  c\^{}n)  \mwedge{}  (0  \mleq{}  a  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  b)


By

---

Latex:
TACTIC:Auto

---

Home Index