---

Step * 1 1 1 1 1 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. a - b < (v + 1) * (v + 1)
9. (isqrt(a) * isqrt(a)) ≤ a
10. (isqrt(b) * isqrt(b)) ≤ b
11. ((isqrt(b) * isqrt(b)) ≤ b) ∧ b < (isqrt(b) + 1) * (isqrt(b) + 1)
⊢ b ≤ ((isqrt(b) + 2) * isqrt(b))
BY
{ TACTIC:(D -1 THEN (RW IntNormC (-1) THENA Auto) THEN (RW IntNormC (0) THENA Auto)) }

1
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. a - b < (v + 1) * (v + 1)
9. (isqrt(a) * isqrt(a)) ≤ a
10. (isqrt(b) * isqrt(b)) ≤ b
11. (isqrt(b) * isqrt(b)) ≤ b
12. b < 1 + (2 * isqrt(b)) + (isqrt(b) * isqrt(b))
⊢ b ≤ ((2 * isqrt(b)) + (isqrt(b) * isqrt(b)))

---

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.  a  -  b  <  (v  +  1)  *  (v  +  1)
9.  (isqrt(a)  *  isqrt(a))  \mleq{}  a
10.  (isqrt(b)  *  isqrt(b))  \mleq{}  b
11.  ((isqrt(b)  *  isqrt(b))  \mleq{}  b)  \mwedge{}  b  <  (isqrt(b)  +  1)  *  (isqrt(b)  +  1)
\mvdash{}  b  \mleq{}  ((isqrt(b)  +  2)  *  isqrt(b))


By

---

Latex:
TACTIC:(D  -1  THEN  (RW  IntNormC  (-1)  THENA  Auto)  THEN  (RW  IntNormC  (0)  THENA  Auto))

---

Home Index