---

Step * 2 of Lemma four-squares

.....antecedent..... 
∀p:Prime. ∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)
BY
{ ((D 0 THENA Auto) THEN CaseNat 2 `p') }

1
1. p : Prime
2. p = 2 ∈ ℤ
⊢ ∃a,b,c,d:ℤ. (2 = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

2
1. p : Prime
2. ¬(p = 2 ∈ ℤ)
⊢ ∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

---

Latex:

---

Latex:
.....antecedent..... 
\mforall{}p:Prime.  \mexists{}a,b,c,d:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  CaseNat  2  `p')

---

Home Index