---

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

.....assertion..... 
1. p : Prime
2. r : ℕ
3. ∀c:ℕr. ∀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 * r) ∈ ℤ
7. 0 < r
8. r < p
9. ¬(r = 1 ∈ ℤ)
⊢ (∃u1:ℤ. (((2 * |u1|) ≤ r) ∧ (u1 ≡ a mod r))) ∧ (∃u2:ℤ. (((2 * |u2|) ≤ r) ∧ (u2 ≡ (-b) mod r)))
BY
{ Auto }

---

Latex:

---

Latex:
.....assertion..... 
1.  p  :  Prime
2.  r  :  \mBbbN{}
3.  \mforall{}c:\mBbbN{}r.  \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  *  r)
7.  0  <  r
8.  r  <  p
9.  \mneg{}(r  =  1)
\mvdash{}  (\mexists{}u1:\mBbbZ{}.  (((2  *  |u1|)  \mleq{}  r)  \mwedge{}  (u1  \mequiv{}  a  mod  r)))  \mwedge{}  (\mexists{}u2:\mBbbZ{}.  (((2  *  |u2|)  \mleq{}  r)  \mwedge{}  (u2  \mequiv{}  (-b)  mod  r)))


By

---

Latex:
Auto

---

Home Index