Step
*
1
1
2
1
1
of Lemma
isqrt-convex
1. a : ℕ@i
2. b : ℕa@i
3. isqrt(b) ≤ isqrt(a)
4. (isqrt(b) + 2) ≤ isqrt(a)
5. v : ℕ@i
6. isqrt(a - b) = v ∈ ℕ
7. (v * v) ≤ (a - b)
8. (isqrt(a) - isqrt(b)) * (isqrt(a) - isqrt(b)) < (v + 1) * (v + 1)
9. ((isqrt(a) - isqrt(b)) * (isqrt(a) - isqrt(b))) ≤ (a - b)
10. (v + 1) ≤ (isqrt(a) - isqrt(b))
⊢ (isqrt(a) - isqrt(b)) ≤ v
BY
{ TACTIC:(RWO "-1" (-3) THEN Auto) }
Latex:
Latex:
1.  a  :  \mBbbN{}@i
2.  b  :  \mBbbN{}a@i
3.  isqrt(b)  \mleq{}  isqrt(a)
4.  (isqrt(b)  +  2)  \mleq{}  isqrt(a)
5.  v  :  \mBbbN{}@i
6.  isqrt(a  -  b)  =  v
7.  (v  *  v)  \mleq{}  (a  -  b)
8.  (isqrt(a)  -  isqrt(b))  *  (isqrt(a)  -  isqrt(b))  <  (v  +  1)  *  (v  +  1)
9.  ((isqrt(a)  -  isqrt(b))  *  (isqrt(a)  -  isqrt(b)))  \mleq{}  (a  -  b)
10.  (v  +  1)  \mleq{}  (isqrt(a)  -  isqrt(b))
\mvdash{}  (isqrt(a)  -  isqrt(b))  \mleq{}  v
By
Latex:
TACTIC:(RWO  "-1"  (-3)  THEN  Auto)
Home
Index