---

Step * 1 2 1 2 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
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ ((Assert ((u1 * u1) ≡ (a * a) mod r) ∧ ((u2 * u2) ≡ ((-b) * (-b)) mod r) BY
          EAuto 1)
   THEN (Assert ((u1 * u1) + (u2 * u2)) ≡ ((a * a) + ((-b) * (-b))) mod r BY
               EAuto 1)
   THEN (Assert ((a * a) + (b * b)) ≡ 0 mod r BY
               (D 0 With ⌜p⌝  THEN Auto))
   THEN (Subst' (-b) * (-b) ~ b * b -2 THENA Auto)
   THEN (Assert ((u1 * u1) + (u2 * u2)) ≡ 0 mod r BY
               (RWO "-1" (-2) 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
⊢ ∃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
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
((Assert  ((u1  *  u1)  \mequiv{}  (a  *  a)  mod  r)  \mwedge{}  ((u2  *  u2)  \mequiv{}  ((-b)  *  (-b))  mod  r)  BY
                EAuto  1)
  THEN  (Assert  ((u1  *  u1)  +  (u2  *  u2))  \mequiv{}  ((a  *  a)  +  ((-b)  *  (-b)))  mod  r  BY
                          EAuto  1)
  THEN  (Assert  ((a  *  a)  +  (b  *  b))  \mequiv{}  0  mod  r  BY
                          (D  0  With  \mkleeneopen{}p\mkleeneclose{}    THEN  Auto))
  THEN  (Subst'  (-b)  *  (-b)  \msim{}  b  *  b  -2  THENA  Auto)
  THEN  (Assert  ((u1  *  u1)  +  (u2  *  u2))  \mequiv{}  0  mod  r  BY
                          (RWO  "-1"  (-2)  THEN  Auto)))

---

Home Index