---

Step * 1 1 1 of Lemma prime-sum-of-four-squares


1. p : Prime
2. r : ℕ
3. ∀r:ℕr. ∀a,b,c,d:ℤ.
     (((((a * a) + (b * b) + (c * c) + (d * d)) = (p * r) ∈ ℤ) ∧ 0 < r ∧ r < p)
     ⇒ (∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)))
4. a : ℤ
5. b : ℤ
6. c : ℤ
7. d : ℤ
8. ((a * a) + (b * b) + (c * c) + (d * d)) = (p * r) ∈ ℤ
9. 0 < r
10. r < p
11. ¬(r = 1 ∈ ℤ)
12. a' : ℤ
13. (2 * |a'|) ≤ r
14. a' ≡ a mod r
15. b' : ℤ
16. (2 * |b'|) ≤ r
17. b' ≡ b mod r
18. c' : ℤ
19. (2 * |c'|) ≤ r
20. c' ≡ c mod r
21. d' : ℤ
22. (2 * |d'|) ≤ r
23. d' ≡ d mod r
24. ((a' * a') ≡ (a * a) mod r)
∧ ((b' * b') ≡ (b * b) mod r)
∧ ((c' * c') ≡ (c * c) mod r)
∧ ((d' * d') ≡ (d * d) mod r)
25. c1 : ℤ
26. (((a' * a') + (b' * b') + (c' * c') + (d' * d')) - 0) = (r * c1) ∈ ℤ
⊢ ∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)
BY
{ (Subst' ((a' * a') + (b' * b') + (c' * c') + (d' * d')) - 0 ~ (a' * a') + (b' * b') + (c' * c') + (d' * d') -1
   THENA Auto
   ) }

1
1. p : Prime
2. r : ℕ
3. ∀r:ℕr. ∀a,b,c,d:ℤ.
     (((((a * a) + (b * b) + (c * c) + (d * d)) = (p * r) ∈ ℤ) ∧ 0 < r ∧ r < p)
     ⇒ (∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)))
4. a : ℤ
5. b : ℤ
6. c : ℤ
7. d : ℤ
8. ((a * a) + (b * b) + (c * c) + (d * d)) = (p * r) ∈ ℤ
9. 0 < r
10. r < p
11. ¬(r = 1 ∈ ℤ)
12. a' : ℤ
13. (2 * |a'|) ≤ r
14. a' ≡ a mod r
15. b' : ℤ
16. (2 * |b'|) ≤ r
17. b' ≡ b mod r
18. c' : ℤ
19. (2 * |c'|) ≤ r
20. c' ≡ c mod r
21. d' : ℤ
22. (2 * |d'|) ≤ r
23. d' ≡ d mod r
24. ((a' * a') ≡ (a * a) mod r)
∧ ((b' * b') ≡ (b * b) mod r)
∧ ((c' * c') ≡ (c * c) mod r)
∧ ((d' * d') ≡ (d * d) mod r)
25. c1 : ℤ
26. ((a' * a') + (b' * b') + (c' * c') + (d' * d')) = (r * c1) ∈ ℤ
⊢ ∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

---

Latex:

---

Latex:

1.  p  :  Prime
2.  r  :  \mBbbN{}
3.  \mforall{}r:\mBbbN{}r.  \mforall{}a,b,c,d:\mBbbZ{}.
          (((((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d))  =  (p  *  r))  \mwedge{}  0  <  r  \mwedge{}  r  <  p)
          {}\mRightarrow{}  (\mexists{}a,b,c,d:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d)))))
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  c  :  \mBbbZ{}
7.  d  :  \mBbbZ{}
8.  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d))  =  (p  *  r)
9.  0  <  r
10.  r  <  p
11.  \mneg{}(r  =  1)
12.  a'  :  \mBbbZ{}
13.  (2  *  |a'|)  \mleq{}  r
14.  a'  \mequiv{}  a  mod  r
15.  b'  :  \mBbbZ{}
16.  (2  *  |b'|)  \mleq{}  r
17.  b'  \mequiv{}  b  mod  r
18.  c'  :  \mBbbZ{}
19.  (2  *  |c'|)  \mleq{}  r
20.  c'  \mequiv{}  c  mod  r
21.  d'  :  \mBbbZ{}
22.  (2  *  |d'|)  \mleq{}  r
23.  d'  \mequiv{}  d  mod  r
24.  ((a'  *  a')  \mequiv{}  (a  *  a)  mod  r)
\mwedge{}  ((b'  *  b')  \mequiv{}  (b  *  b)  mod  r)
\mwedge{}  ((c'  *  c')  \mequiv{}  (c  *  c)  mod  r)
\mwedge{}  ((d'  *  d')  \mequiv{}  (d  *  d)  mod  r)
25.  c1  :  \mBbbZ{}
26.  (((a'  *  a')  +  (b'  *  b')  +  (c'  *  c')  +  (d'  *  d'))  -  0)  =  (r  *  c1)
\mvdash{}  \mexists{}a,b,c,d:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d)))


By

---

Latex:
(Subst'  ((a'  *  a')  +  (b'  *  b')  +  (c'  *  c')  +  (d'  *  d'))  -  0  \msim{}  (a'  *  a')
  +  (b'  *  b')
  +  (c'  *  c')
  +  (d'  *  d')  -1
  THENA  Auto
  )

---

Home Index