---

Step * of Lemma two-squares-iff

∀x:ℕ
  (∃y,z:ℕ. (((y * y) + (z * z)) = x ∈ ℤ)
  ⇐⇒ ∃y:ℕisqrt(x) + 1. ((isqrt(x - y * y) * isqrt(x - y * y)) = (x - y * y) ∈ ℤ))
BY
{ ((TACTIC:(D 0 THENA Auto) THEN (InstLemma `isqrt-property` [⌜x⌝]⋅ THENA Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜isqrt(x)⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA Try (Complete (Auto)))) }

1
1. x : ℕ
2. v : ℕ
3. isqrt(x) = v ∈ ℕ
4. ((v * v) ≤ x) ∧ x < (v + 1) * (v + 1)
5. ∃y,z:ℕ. (((y * y) + (z * z)) = x ∈ ℤ)
⊢ ∃y:ℕv + 1. ((isqrt(x - y * y) * isqrt(x - y * y)) = (x - y * y) ∈ ℤ)

2
1. x : ℕ
2. v : ℕ
3. isqrt(x) = v ∈ ℕ
4. ((v * v) ≤ x) ∧ x < (v + 1) * (v + 1)
5. ∃y:ℕv + 1. ((isqrt(x - y * y) * isqrt(x - y * y)) = (x - y * y) ∈ ℤ)
⊢ ∃y,z:ℕ. (((y * y) + (z * z)) = x ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}
    (\mexists{}y,z:\mBbbN{}.  (((y  *  y)  +  (z  *  z))  =  x)
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:\mBbbN{}isqrt(x)  +  1.  ((isqrt(x  -  y  *  y)  *  isqrt(x  -  y  *  y))  =  (x  -  y  *  y)))


By

---

Latex:
((TACTIC:(D  0  THENA  Auto)  THEN  (InstLemma  `isqrt-property`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}isqrt(x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Try  (Complete  (Auto))))

---

Home Index