---

Step * of Lemma implies-sum-of-two-squares

∀n:ℕ. ((∃x:ℤ-o. ∃w,y:ℤ. ((n * x * x) = ((w * w) + (y * y)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)))
BY
{ Assert ⌜∀n,x:ℕ.
            (0 < x ⇒ (∃w,y:ℤ. ((n * x * x) = ((w * w) + (y * y)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)))⌝⋅ }

1
.....assertion..... 
∀n,x:ℕ.  (0 < x ⇒ (∃w,y:ℤ. ((n * x * x) = ((w * w) + (y * y)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)))

2
1. ∀n,x:ℕ.  (0 < x ⇒ (∃w,y:ℤ. ((n * x * x) = ((w * w) + (y * y)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)))
⊢ ∀n:ℕ. ((∃x:ℤ-o. ∃w,y:ℤ. ((n * x * x) = ((w * w) + (y * y)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  ((\mexists{}x:\mBbbZ{}\msupminus{}\msupzero{}.  \mexists{}w,y:\mBbbZ{}.  ((n  *  x  *  x)  =  ((w  *  w)  +  (y  *  y))))  {}\mRightarrow{}  (\mexists{}a,b:\mBbbZ{}.  (n  =  ((a  *  a)  +  (b  *  b)))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n,x:\mBbbN{}.
                    (0  <  x
                    {}\mRightarrow{}  (\mexists{}w,y:\mBbbZ{}.  ((n  *  x  *  x)  =  ((w  *  w)  +  (y  *  y))))
                    {}\mRightarrow{}  (\mexists{}a,b:\mBbbZ{}.  (n  =  ((a  *  a)  +  (b  *  b)))))\mkleeneclose{}\mcdot{}

---

Home Index