---

Step * 2 2 1 of Lemma four-squares

.....assertion..... 
1. p : Prime
2. ¬(p = 2 ∈ ℤ)
⊢ ∃n:ℕ+p. ∃a,b:ℤ. (((a * a) + (b * b) + 1) = (n * p) ∈ ℤ)
BY
{ ((InstLemma `Prime-isOdd` [⌜p⌝]⋅ THENA Auto) THEN (FLemma `assert-isOdd` [-1] THENA Auto) THEN D -1) }

1
1. p : Prime
2. ¬(p = 2 ∈ ℤ)
3. ↑isOdd(p)
4. k : ℤ
5. p = ((2 * k) + 1) ∈ ℤ
⊢ ∃n:ℕ+p. ∃a,b:ℤ. (((a * a) + (b * b) + 1) = (n * p) ∈ ℤ)

---

Latex:

---

Latex:
.....assertion..... 
1.  p  :  Prime
2.  \mneg{}(p  =  2)
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}p.  \mexists{}a,b:\mBbbZ{}.  (((a  *  a)  +  (b  *  b)  +  1)  =  (n  *  p))


By

---

Latex:
((InstLemma  `Prime-isOdd`  [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (FLemma  `assert-isOdd`  [-1]  THENA  Auto)  THEN  D  -1)

---

Home Index