Step
*
of Lemma
exp-convex2
∀[a,b:ℤ]. ∀[c:ℕ]. ∀[n:ℕ+].  |a - b| ≤ c supposing (|a^n - b^n| ≤ c^n) ∧ (0 ≤ a 
⇐⇒ 0 ≤ b)
BY
{ 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:
Auto
Home
Index