---

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

∀p:Prime. ∀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)) ∈ ℤ)))
BY
{ ((D 0 THENA Auto)
   THEN CompleteInductionOnNat
   THEN Auto
   THEN (CaseNat 1 `r'
         THENL [(Eliminate ⌜r⌝⋅ THEN InstConcl [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THEN Auto)
               ; ((Assert (∃a':ℤ. (((2 * |a'|) ≤ r) ∧ (a' ≡ a mod r)))
                         ∧ (∃b':ℤ. (((2 * |b'|) ≤ r) ∧ (b' ≡ b mod r)))
                         ∧ (∃c':ℤ. (((2 * |c'|) ≤ r) ∧ (c' ≡ c mod r)))
                         ∧ (∃d':ℤ. (((2 * |d'|) ≤ r) ∧ (d' ≡ d mod r))) BY
                         Auto)
                  THEN ExRepD
                  THEN (Assert ((a' * a') ≡ (a * a) mod r)
                              ∧ ((b' * b') ≡ (b * b) mod r)
                              ∧ ((c' * c') ≡ (c * c) mod r)
                              ∧ ((d' * d') ≡ (d * d) mod r) BY
                              EAuto 1)
                  THEN (Assert ((a' * a') + (b' * b') + (c' * c') + (d' * d')) ≡ ((a * a)
                              + (b * b)
                              + (c * c)
                              + (d * d)) mod r BY
                              (Repeat (BLemma `add_functionality_wrt_eqmod`) THEN 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. ((a' * a') + (b' * b') + (c' * c') + (d' * d')) ≡ ((a * a) + (b * b) + (c * c) + (d * d)) mod r
⊢ ∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}p:Prime.  \mforall{}r:\mBbbN{}.  \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)))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  CompleteInductionOnNat
  THEN  Auto
  THEN  (CaseNat  1  `r'
              THENL  [(Eliminate  \mkleeneopen{}r\mkleeneclose{}\mcdot{}  THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)
                          ;  ((Assert  (\mexists{}a':\mBbbZ{}.  (((2  *  |a'|)  \mleq{}  r)  \mwedge{}  (a'  \mequiv{}  a  mod  r)))
                                              \mwedge{}  (\mexists{}b':\mBbbZ{}.  (((2  *  |b'|)  \mleq{}  r)  \mwedge{}  (b'  \mequiv{}  b  mod  r)))
                                              \mwedge{}  (\mexists{}c':\mBbbZ{}.  (((2  *  |c'|)  \mleq{}  r)  \mwedge{}  (c'  \mequiv{}  c  mod  r)))
                                              \mwedge{}  (\mexists{}d':\mBbbZ{}.  (((2  *  |d'|)  \mleq{}  r)  \mwedge{}  (d'  \mequiv{}  d  mod  r)))  BY
                                              Auto)
                                THEN  ExRepD
                                THEN  (Assert  ((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)  BY
                                                        EAuto  1)
                                THEN  (Assert  ((a'  *  a')  +  (b'  *  b')  +  (c'  *  c')  +  (d'  *  d'))  \mequiv{}  ((a  *  a)
                                                        +  (b  *  b)
                                                        +  (c  *  c)
                                                        +  (d  *  d))  mod  r  BY
                                                        (Repeat  (BLemma  `add\_functionality\_wrt\_eqmod`)  THEN  Auto)))]
  ))

---

Home Index