---

Step * 1 of Lemma square-iff-isqrt

.....equality..... 
1. x : ℕ@i
2. y : ℕ@i
3. (y * y) = x ∈ ℤ@i
⊢ isqrt(x) = y ∈ ℤ
BY
{ ((InstLemma `isqrt-property` [⌜x⌝]⋅ THEN Auto)⋅ THEN CaseNat 0 `y') }

1
1. x : ℕ@i
2. y : ℕ@i
3. (y * y) = x ∈ ℤ@i
4. (isqrt(x) * isqrt(x)) ≤ x
5. x < (isqrt(x) + 1) * (isqrt(x) + 1)
6. y = 0 ∈ ℤ
⊢ isqrt(x) = 0 ∈ ℤ

2
1. x : ℕ@i
2. y : ℕ@i
3. (y * y) = x ∈ ℤ@i
4. (isqrt(x) * isqrt(x)) ≤ x
5. x < (isqrt(x) + 1) * (isqrt(x) + 1)
6. ¬(y = 0 ∈ ℤ)
⊢ isqrt(x) = y ∈ ℤ

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  \mBbbN{}@i
2.  y  :  \mBbbN{}@i
3.  (y  *  y)  =  x@i
\mvdash{}  isqrt(x)  =  y


By

---

Latex:
((InstLemma  `isqrt-property`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}  THEN  CaseNat  0  `y')

---

Home Index