---

Step * 1 1 1 1 1 of Lemma isqrt_newton_wf

.....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. (v ÷ 2) = v1 ∈ ℤ
15. (v - v rem 2) = (2 * v1) ∈ ℤ
16. 0 ≤ (v rem 2)
17. v rem 2 < 2
18. (v rem 2) ≤ 1
19. (x * (v rem 2)) ≤ (x * 1)
20. ((v * x) + ((-1) * x * (v rem 2))) = (2 * v1 * x) ∈ ℤ
21. (x * 0) ≤ (x * (v rem 2))
22. x ≤ v1
⊢ x ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]
BY
{ xxx(MemTypeCD THEN Auto)xxx }

1
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. (v ÷ 2) = v1 ∈ ℤ
15. (v - v rem 2) = (2 * v1) ∈ ℤ
16. 0 ≤ (v rem 2)
17. v rem 2 < 2
18. (v rem 2) ≤ 1
19. (x * (v rem 2)) ≤ (x * 1)
20. ((v * x) + ((-1) * x * (v rem 2))) = (2 * v1 * x) ∈ ℤ
21. (x * 0) ≤ (x * (v rem 2))
22. x ≤ v1
⊢ (x * x) ≤ n

---

Latex:

---

Latex:
.....assertion..... 
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.  (v  \mdiv{}  2)  =  v1
15.  (v  -  v  rem  2)  =  (2  *  v1)
16.  0  \mleq{}  (v  rem  2)
17.  v  rem  2  <  2
18.  (v  rem  2)  \mleq{}  1
19.  (x  *  (v  rem  2))  \mleq{}  (x  *  1)
20.  ((v  *  x)  +  ((-1)  *  x  *  (v  rem  2)))  =  (2  *  v1  *  x)
21.  (x  *  0)  \mleq{}  (x  *  (v  rem  2))
22.  x  \mleq{}  v1
\mvdash{}  x  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]


By

---

Latex:
xxx(MemTypeCD  THEN  Auto)xxx

---

Home Index