---

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


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 ∈ ℤ)
10. u1 : ℤ
11. (2 * |u1|) ≤ r
12. u1 ≡ a mod r
13. u2 : ℤ
14. (2 * |u2|) ≤ r
15. u2 ≡ (-b) mod r
16. ((u1 * u1) ≡ (a * a) mod r) ∧ ((u2 * u2) ≡ ((-b) * (-b)) mod r)
17. ((u1 * u1) + (u2 * u2)) ≡ ((a * a) + (b * b)) mod r
18. ((a * a) + (b * b)) ≡ 0 mod r
19. ((u1 * u1) + (u2 * u2)) ≡ 0 mod r
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (DupHyp (-1) THEN D -1 THEN Assert ⌜c ∈ ℕr⌝⋅) }

1
.....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 ∈ ℤ)
10. u1 : ℤ
11. (2 * |u1|) ≤ r
12. u1 ≡ a mod r
13. u2 : ℤ
14. (2 * |u2|) ≤ r
15. u2 ≡ (-b) mod r
16. ((u1 * u1) ≡ (a * a) mod r) ∧ ((u2 * u2) ≡ ((-b) * (-b)) mod r)
17. ((u1 * u1) + (u2 * u2)) ≡ ((a * a) + (b * b)) mod r
18. ((a * a) + (b * b)) ≡ 0 mod r
19. ((u1 * u1) + (u2 * u2)) ≡ 0 mod r
20. c : ℤ
21. (((u1 * u1) + (u2 * u2)) - 0) = (r * c) ∈ ℤ
⊢ c ∈ ℕr

2
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 ∈ ℤ)
10. u1 : ℤ
11. (2 * |u1|) ≤ r
12. u1 ≡ a mod r
13. u2 : ℤ
14. (2 * |u2|) ≤ r
15. u2 ≡ (-b) mod r
16. ((u1 * u1) ≡ (a * a) mod r) ∧ ((u2 * u2) ≡ ((-b) * (-b)) mod r)
17. ((u1 * u1) + (u2 * u2)) ≡ ((a * a) + (b * b)) mod r
18. ((a * a) + (b * b)) ≡ 0 mod r
19. ((u1 * u1) + (u2 * u2)) ≡ 0 mod r
20. c : ℤ
21. (((u1 * u1) + (u2 * u2)) - 0) = (r * c) ∈ ℤ
22. c ∈ ℕr
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:

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)
10.  u1  :  \mBbbZ{}
11.  (2  *  |u1|)  \mleq{}  r
12.  u1  \mequiv{}  a  mod  r
13.  u2  :  \mBbbZ{}
14.  (2  *  |u2|)  \mleq{}  r
15.  u2  \mequiv{}  (-b)  mod  r
16.  ((u1  *  u1)  \mequiv{}  (a  *  a)  mod  r)  \mwedge{}  ((u2  *  u2)  \mequiv{}  ((-b)  *  (-b))  mod  r)
17.  ((u1  *  u1)  +  (u2  *  u2))  \mequiv{}  ((a  *  a)  +  (b  *  b))  mod  r
18.  ((a  *  a)  +  (b  *  b))  \mequiv{}  0  mod  r
19.  ((u1  *  u1)  +  (u2  *  u2))  \mequiv{}  0  mod  r
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
(DupHyp  (-1)  THEN  D  -1  THEN  Assert  \mkleeneopen{}c  \mmember{}  \mBbbN{}r\mkleeneclose{}\mcdot{})

---

Home Index