---

Step * 1 2 1 2 1 1 2 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
20. c : ℤ
21. (((u1 * u1) + (u2 * u2)) - 0) = (r * c) ∈ ℤ
22. c ∈ ℕr
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (Assert ((u1 * a) + (u2 * (-b))) ≡ 0 mod r BY
         ((Assert ((u1 * a) ≡ (a * a) mod r) ∧ ((u2 * (-b)) ≡ ((-b) * (-b)) mod r) BY
                 (D 0 THEN BLemma `multiply_functionality_wrt_eqmod` THEN EAuto 1))
          THEN (Assert ((u1 * a) + (u2 * (-b))) ≡ ((a * a) + ((-b) * (-b))) mod r BY
                      EAuto 1)
          THEN (Subst' (-b) * (-b) ~ b * b -1 THENA Auto)
          THEN RWO "-7" (-1)
          THEN Auto)) }

1
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
23. ((u1 * a) + (u2 * (-b))) ≡ 0 mod 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
20.  c  :  \mBbbZ{}
21.  (((u1  *  u1)  +  (u2  *  u2))  -  0)  =  (r  *  c)
22.  c  \mmember{}  \mBbbN{}r
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
(Assert  ((u1  *  a)  +  (u2  *  (-b)))  \mequiv{}  0  mod  r  BY
              ((Assert  ((u1  *  a)  \mequiv{}  (a  *  a)  mod  r)  \mwedge{}  ((u2  *  (-b))  \mequiv{}  ((-b)  *  (-b))  mod  r)  BY
                              (D  0  THEN  BLemma  `multiply\_functionality\_wrt\_eqmod`  THEN  EAuto  1))
                THEN  (Assert  ((u1  *  a)  +  (u2  *  (-b)))  \mequiv{}  ((a  *  a)  +  ((-b)  *  (-b)))  mod  r  BY
                                        EAuto  1)
                THEN  (Subst'  (-b)  *  (-b)  \msim{}  b  *  b  -1  THENA  Auto)
                THEN  RWO  "-7"  (-1)
                THEN  Auto))

---

Home Index