| Step | Hyp | Ref
| Expression |
| 1 | | 4sq.4 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 2 | | prmnn 16711 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 4 | 3 | nncnd 12282 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 5 | 4 | mullidd 11279 |
. 2
⊢ (𝜑 → (1 · 𝑃) = 𝑃) |
| 6 | | 4sq.7 |
. . . . . . . . . . . 12
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
| 7 | | 4sq.6 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
| 8 | 7 | ssrab3 4082 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ⊆
ℕ |
| 9 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 10 | 8, 9 | sseqtri 4032 |
. . . . . . . . . . . . 13
⊢ 𝑇 ⊆
(ℤ≥‘1) |
| 11 | | 4sq.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
| 12 | | 4sq.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 13 | | 4sq.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
| 14 | | 4sq.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) |
| 15 | 11, 12, 13, 1, 14, 7, 6 | 4sqlem13 16995 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
| 16 | 15 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ≠ ∅) |
| 17 | | infssuzcl 12974 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
| 18 | 10, 16, 17 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
| 19 | 6, 18 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
| 20 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (𝑖 · 𝑃) = (𝑀 · 𝑃)) |
| 21 | 20 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑀 · 𝑃) ∈ 𝑆)) |
| 22 | 21, 7 | elrab2 3695 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ ℕ ∧ (𝑀 · 𝑃) ∈ 𝑆)) |
| 23 | 19, 22 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ (𝑀 · 𝑃) ∈ 𝑆)) |
| 24 | 23 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) ∈ 𝑆) |
| 25 | 11 | 4sqlem2 16987 |
. . . . . . . . 9
⊢ ((𝑀 · 𝑃) ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 26 | 24, 25 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
→ ∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ ∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 28 | | simp1l 1198 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝜑) |
| 29 | 28, 12 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑁 ∈ ℕ) |
| 30 | 28, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑃 = ((2 · 𝑁) + 1)) |
| 31 | 28, 1 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑃 ∈ ℙ) |
| 32 | 28, 14 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → (0...(2 · 𝑁)) ⊆ 𝑆) |
| 33 | | simp1r 1199 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑀 ∈
(ℤ≥‘2)) |
| 34 | | simp2ll 1241 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑎 ∈ ℤ) |
| 35 | | simp2lr 1242 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑏 ∈ ℤ) |
| 36 | | simp2rl 1243 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑐 ∈ ℤ) |
| 37 | | simp2rr 1244 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑑 ∈ ℤ) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 39 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 40 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 42 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(((((((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2) + ((((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2)) + (((((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2) + ((((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2))) / 𝑀) = (((((((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2) + ((((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2)) + (((((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2) + ((((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))↑2))) / 𝑀) |
| 43 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 44 | 11, 29, 30, 31, 32, 7, 6, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43 | 4sqlem17 16999 |
. . . . . . . . . . . 12
⊢ ¬
((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 45 | 44 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → ¬ 𝑀 ∈
(ℤ≥‘2)) |
| 46 | 45 | 3expia 1122 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ)))
→ ((𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
| 47 | 46 | anassrs 467 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ (𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ))
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
→ ((𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
| 48 | 47 | rexlimdvva 3213 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ (𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ))
→ (∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
| 49 | 48 | rexlimdvva 3213 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
→ (∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ ∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
| 50 | 27, 49 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
→ ¬ 𝑀 ∈
(ℤ≥‘2)) |
| 51 | 50 | pm2.01da 799 |
. . . . 5
⊢ (𝜑 → ¬ 𝑀 ∈
(ℤ≥‘2)) |
| 52 | 23 | simpld 494 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 53 | | elnn1uz2 12967 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ ↔ (𝑀 = 1 ∨ 𝑀 ∈
(ℤ≥‘2))) |
| 54 | 52, 53 | sylib 218 |
. . . . . 6
⊢ (𝜑 → (𝑀 = 1 ∨ 𝑀 ∈
(ℤ≥‘2))) |
| 55 | 54 | ord 865 |
. . . . 5
⊢ (𝜑 → (¬ 𝑀 = 1 → 𝑀 ∈
(ℤ≥‘2))) |
| 56 | 51, 55 | mt3d 148 |
. . . 4
⊢ (𝜑 → 𝑀 = 1) |
| 57 | 56, 19 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → 1 ∈ 𝑇) |
| 58 | | oveq1 7438 |
. . . . . 6
⊢ (𝑖 = 1 → (𝑖 · 𝑃) = (1 · 𝑃)) |
| 59 | 58 | eleq1d 2826 |
. . . . 5
⊢ (𝑖 = 1 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (1 · 𝑃) ∈ 𝑆)) |
| 60 | 59, 7 | elrab2 3695 |
. . . 4
⊢ (1 ∈
𝑇 ↔ (1 ∈ ℕ
∧ (1 · 𝑃) ∈
𝑆)) |
| 61 | 60 | simprbi 496 |
. . 3
⊢ (1 ∈
𝑇 → (1 · 𝑃) ∈ 𝑆) |
| 62 | 57, 61 | syl 17 |
. 2
⊢ (𝜑 → (1 · 𝑃) ∈ 𝑆) |
| 63 | 5, 62 | eqeltrrd 2842 |
1
⊢ (𝜑 → 𝑃 ∈ 𝑆) |