---

Step * 1 of Lemma prime-sum-of-two-squares-lemma


1. p : Prime
2. c : ℕ
3. ∀c:ℕc. ∀a,b:ℤ.  (((((a * a) + (b * b)) = (p * c) ∈ ℤ) ∧ 0 < c ∧ c < p) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
4. a : ℤ
5. b : ℤ
6. ((a * a) + (b * b)) = (p * c) ∈ ℤ
7. 0 < c
8. c < p
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ CaseNat 1 `c' }

1
1. p : Prime
2. c : ℕ
3. ∀c:ℕc. ∀a,b:ℤ.  (((((a * a) + (b * b)) = (p * c) ∈ ℤ) ∧ 0 < c ∧ c < p) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
4. a : ℤ
5. b : ℤ
6. ((a * a) + (b * b)) = (p * c) ∈ ℤ
7. 0 < c
8. c < p
9. c = 1 ∈ ℤ
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

2
1. p : Prime
2. c : ℕ
3. ∀c:ℕc. ∀a,b:ℤ.  (((((a * a) + (b * b)) = (p * c) ∈ ℤ) ∧ 0 < c ∧ c < p) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
4. a : ℤ
5. b : ℤ
6. ((a * a) + (b * b)) = (p * c) ∈ ℤ
7. 0 < c
8. c < p
9. ¬(c = 1 ∈ ℤ)
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:

1.  p  :  Prime
2.  c  :  \mBbbN{}
3.  \mforall{}c:\mBbbN{}c.  \mforall{}a,b:\mBbbZ{}.
          (((((a  *  a)  +  (b  *  b))  =  (p  *  c))  \mwedge{}  0  <  c  \mwedge{}  c  <  p)  {}\mRightarrow{}  (\mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))))
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  ((a  *  a)  +  (b  *  b))  =  (p  *  c)
7.  0  <  c
8.  c  <  p
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
CaseNat  1  `c'

---

Home Index