---

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

∀p:Prime. ∀c:ℕ. ∀a,b:ℤ.
  (((((a * a) + (b * b)) = (p * c) ∈ ℤ) ∧ 0 < c ∧ c < p) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
BY
{ ((D 0 THENA Auto) THEN CompleteInductionOnNat THEN Auto) }

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
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}p:Prime.  \mforall{}c:\mBbbN{}.  \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)))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  CompleteInductionOnNat  THEN  Auto)

---

Home Index