---

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


1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. ∀p:Prime. ((p | n) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
4. ¬(n = 1 ∈ ℤ)
5. factors : {m:{2...}| prime(m)}  List
6. n = Π(factors)  ∈ ℤ
⊢ ∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (Assert ∀p:{m:{2...}| prime(m)} . ((p ∈ factors) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ))) BY
         (Auto THEN BHyp 3 THEN Auto)) }

1
.....aux..... 
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. ∀p:Prime. ((p | n) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
4. ¬(n = 1 ∈ ℤ)
5. factors : {m:{2...}| prime(m)}  List
6. n = Π(factors)  ∈ ℤ
7. p : {m:{2...}| prime(m)} 
8. (p ∈ factors)
⊢ p | n

2
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. ∀p:Prime. ((p | n) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
4. ¬(n = 1 ∈ ℤ)
5. factors : {m:{2...}| prime(m)}  List
6. n = Π(factors)  ∈ ℤ
7. ∀p:{m:{2...}| prime(m)} . ((p ∈ factors) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
⊢ ∃a,b:ℤ. (n = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mneg{}(n  =  0)
3.  \mforall{}p:Prime.  ((p  |  n)  {}\mRightarrow{}  (\mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))))
4.  \mneg{}(n  =  1)
5.  factors  :  \{m:\{2...\}|  prime(m)\}    List
6.  n  =  \mPi{}(factors) 
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (n  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
(Assert  \mforall{}p:\{m:\{2...\}|  prime(m)\}  .  ((p  \mmember{}  factors)  {}\mRightarrow{}  (\mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))))  BY
              (Auto  THEN  BHyp  3  THEN  Auto))

---

Home Index