---

Step * 1 1 1 2 1 of Lemma isqrt_newton_wf


1. d : ℕ
2. ∀d:ℕd. ∀n,x:ℕ+.
     (((((x + 1) * (x + 1)) - n) ≤ d)
     ⇒ n < (x + 1) * (x + 1)
     ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))
3. n : ℕ+
4. x : ℕ+
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ
8. (x + (n ÷ x)) = v ∈ ℤ
9. ((n - n rem x) + (x * x)) = (v * x) ∈ ℤ
10. 0 ≤ (n rem x)
11. n rem x < x
12. 0 ≤ (n ÷ x)
13. v1 : ℤ
14. ¬x < v1
15. v1 ≠ x
16. (v ÷ 2) = v1 ∈ ℤ
17. (v - v rem 2) = (2 * v1) ∈ ℤ
18. 0 ≤ (v rem 2)
19. v rem 2 < 2
20. (v rem 2) ≤ 1
21. (x * (v rem 2)) ≤ (x * 1)
22. ((v * x) + ((-1) * x * (v rem 2))) = (2 * v1 * x) ∈ ℤ
23. (x * 0) ≤ (x * (v rem 2))
24. ¬(x ≤ v1)
⊢ isqrt_newton(n;v1) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]
BY
{ xxxAssert ⌜n < (v1 + 1) * (v1 + 1)⌝⋅xxx }

1
.....assertion..... 
1. d : ℕ
2. ∀d:ℕd. ∀n,x:ℕ+.
     (((((x + 1) * (x + 1)) - n) ≤ d)
     ⇒ n < (x + 1) * (x + 1)
     ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))
3. n : ℕ+
4. x : ℕ+
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ
8. (x + (n ÷ x)) = v ∈ ℤ
9. ((n - n rem x) + (x * x)) = (v * x) ∈ ℤ
10. 0 ≤ (n rem x)
11. n rem x < x
12. 0 ≤ (n ÷ x)
13. v1 : ℤ
14. ¬x < v1
15. v1 ≠ x
16. (v ÷ 2) = v1 ∈ ℤ
17. (v - v rem 2) = (2 * v1) ∈ ℤ
18. 0 ≤ (v rem 2)
19. v rem 2 < 2
20. (v rem 2) ≤ 1
21. (x * (v rem 2)) ≤ (x * 1)
22. ((v * x) + ((-1) * x * (v rem 2))) = (2 * v1 * x) ∈ ℤ
23. (x * 0) ≤ (x * (v rem 2))
24. ¬(x ≤ v1)
⊢ n < (v1 + 1) * (v1 + 1)

2
1. d : ℕ
2. ∀d:ℕd. ∀n,x:ℕ+.
     (((((x + 1) * (x + 1)) - n) ≤ d)
     ⇒ n < (x + 1) * (x + 1)
     ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))
3. n : ℕ+
4. x : ℕ+
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ
8. (x + (n ÷ x)) = v ∈ ℤ
9. ((n - n rem x) + (x * x)) = (v * x) ∈ ℤ
10. 0 ≤ (n rem x)
11. n rem x < x
12. 0 ≤ (n ÷ x)
13. v1 : ℤ
14. ¬x < v1
15. v1 ≠ x
16. (v ÷ 2) = v1 ∈ ℤ
17. (v - v rem 2) = (2 * v1) ∈ ℤ
18. 0 ≤ (v rem 2)
19. v rem 2 < 2
20. (v rem 2) ≤ 1
21. (x * (v rem 2)) ≤ (x * 1)
22. ((v * x) + ((-1) * x * (v rem 2))) = (2 * v1 * x) ∈ ℤ
23. (x * 0) ≤ (x * (v rem 2))
24. ¬(x ≤ v1)
25. n < (v1 + 1) * (v1 + 1)
⊢ isqrt_newton(n;v1) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d.  \mforall{}n,x:\mBbbN{}\msupplus{}.
          (((((x  +  1)  *  (x  +  1))  -  n)  \mleq{}  d)
          {}\mRightarrow{}  n  <  (x  +  1)  *  (x  +  1)
          {}\mRightarrow{}  (isqrt\_newton(n;x)  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]))
3.  n  :  \mBbbN{}\msupplus{}
4.  x  :  \mBbbN{}\msupplus{}
5.  (((x  +  1)  *  (x  +  1))  -  n)  \mleq{}  d
6.  n  <  (x  +  1)  *  (x  +  1)
7.  v  :  \mBbbZ{}
8.  (x  +  (n  \mdiv{}  x))  =  v
9.  ((n  -  n  rem  x)  +  (x  *  x))  =  (v  *  x)
10.  0  \mleq{}  (n  rem  x)
11.  n  rem  x  <  x
12.  0  \mleq{}  (n  \mdiv{}  x)
13.  v1  :  \mBbbZ{}
14.  \mneg{}x  <  v1
15.  v1  \mneq{}  x
16.  (v  \mdiv{}  2)  =  v1
17.  (v  -  v  rem  2)  =  (2  *  v1)
18.  0  \mleq{}  (v  rem  2)
19.  v  rem  2  <  2
20.  (v  rem  2)  \mleq{}  1
21.  (x  *  (v  rem  2))  \mleq{}  (x  *  1)
22.  ((v  *  x)  +  ((-1)  *  x  *  (v  rem  2)))  =  (2  *  v1  *  x)
23.  (x  *  0)  \mleq{}  (x  *  (v  rem  2))
24.  \mneg{}(x  \mleq{}  v1)
\mvdash{}  isqrt\_newton(n;v1)  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]


By

---

Latex:
xxxAssert  \mkleeneopen{}n  <  (v1  +  1)  *  (v1  +  1)\mkleeneclose{}\mcdot{}xxx

---

Home Index