Step
*
2
2
1
1
of Lemma
isqrt-convex
1. ∀a:ℕ. ∀b:ℕa. ((isqrt(a) - isqrt(b)) ≤ isqrt(a - b))
2. a : ℕ
3. b : ℕ
4. ¬b < a
5. a < b
6. (isqrt(b) - isqrt(a)) ≤ isqrt(b - a)
7. isqrt(a) ≤ isqrt(b)
⊢ |isqrt(a) - isqrt(b)| ≤ isqrt(|a - b|)
BY
{ (NthHypEq (-2) THEN RepeatFor 2 ((EqCD THEN Auto))) }
Latex:
Latex:
1. \mforall{}a:\mBbbN{}. \mforall{}b:\mBbbN{}a. ((isqrt(a) - isqrt(b)) \mleq{} isqrt(a - b))
2. a : \mBbbN{}
3. b : \mBbbN{}
4. \mneg{}b < a
5. a < b
6. (isqrt(b) - isqrt(a)) \mleq{} isqrt(b - a)
7. isqrt(a) \mleq{} isqrt(b)
\mvdash{} |isqrt(a) - isqrt(b)| \mleq{} isqrt(|a - b|)
By
Latex:
(NthHypEq (-2) THEN RepeatFor 2 ((EqCD THEN Auto)))
Home
Index