---

Step * of Lemma isqrt-convex

∀a,b:ℕ.  (|isqrt(a) - isqrt(b)| ≤ isqrt(|a - b|))
BY
{ TACTIC:Assert ⌜∀a:ℕ. ∀b:ℕa.  ((isqrt(a) - isqrt(b)) ≤ isqrt(a - b))⌝⋅ }

1
.....assertion..... 
∀a:ℕ. ∀b:ℕa.  ((isqrt(a) - isqrt(b)) ≤ isqrt(a - b))

2
1. ∀a:ℕ. ∀b:ℕa.  ((isqrt(a) - isqrt(b)) ≤ isqrt(a - b))
⊢ ∀a,b:ℕ.  (|isqrt(a) - isqrt(b)| ≤ isqrt(|a - b|))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}.    (|isqrt(a)  -  isqrt(b)|  \mleq{}  isqrt(|a  -  b|))


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}a:\mBbbN{}.  \mforall{}b:\mBbbN{}a.    ((isqrt(a)  -  isqrt(b))  \mleq{}  isqrt(a  -  b))\mkleeneclose{}\mcdot{}

---

Home Index