---

Step * 1 1 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 : ℕ+@i
4. x : ℕ+@i
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ@i
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 : ℤ@i
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))
⊢ if v1=x then v1 else if (x) < (v1)  then x  else isqrt_newton(n;v1) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]
BY
{ TACTIC:(TACTIC:Decide ⌜x ≤ v1⌝⋅ THENA Auto) }

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 : ℕ+@i
4. x : ℕ+@i
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ@i
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 : ℤ@i
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
⊢ if v1=x then v1 else if (x) < (v1)  then x  else isqrt_newton(n;v1) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 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 : ℕ+@i
4. x : ℕ+@i
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ@i
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 : ℤ@i
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)
⊢ if v1=x then v1 else if (x) < (v1)  then x  else 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{}@i
4.  x  :  \mBbbN{}\msupplus{}@i
5.  (((x  +  1)  *  (x  +  1))  -  n)  \mleq{}  d
6.  n  <  (x  +  1)  *  (x  +  1)
7.  v  :  \mBbbZ{}@i
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{}@i
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))
\mvdash{}  if  v1=x  then  v1  else  if  (x)  <  (v1)    then  x    else  isqrt\_newton(n;v1)  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)
                                                                                                                                                          \mwedge{}  n  <  (r  +  1)
                                                                                                                                                              *  (r  +  1))]


By

---

Latex:
TACTIC:(TACTIC:Decide  \mkleeneopen{}x  \mleq{}  v1\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index