Step | Hyp | Ref
| Expression |
1 | | 4sq.4 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) |
2 | | prmnn 15388 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℕ) |
4 | 3 | nncnd 11036 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℂ) |
5 | 4 | mulid2d 10058 |
. 2
⊢ (𝜑 → (1 · 𝑃) = 𝑃) |
6 | | 4sq.7 |
. . . . . . . . . . . 12
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
7 | | 4sq.6 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
8 | | ssrab2 3687 |
. . . . . . . . . . . . . . 15
⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ |
9 | 7, 8 | eqsstri 3635 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ⊆
ℕ |
10 | | nnuz 11723 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
11 | 9, 10 | sseqtri 3637 |
. . . . . . . . . . . . 13
⊢ 𝑇 ⊆
(ℤ≥‘1) |
12 | | 4sq.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
13 | | 4sq.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℕ) |
14 | | 4sq.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
15 | | 4sq.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) |
16 | 12, 13, 14, 1, 15, 7, 6 | 4sqlem13 15661 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
17 | 16 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ≠ ∅) |
18 | | infssuzcl 11772 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
19 | 11, 17, 18 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
20 | 6, 19 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
21 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (𝑖 · 𝑃) = (𝑀 · 𝑃)) |
22 | 21 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑀 · 𝑃) ∈ 𝑆)) |
23 | 22, 7 | elrab2 3366 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ ℕ ∧ (𝑀 · 𝑃) ∈ 𝑆)) |
24 | 20, 23 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ (𝑀 · 𝑃) ∈ 𝑆)) |
25 | 24 | simprd 479 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) ∈ 𝑆) |
26 | 12 | 4sqlem2 15653 |
. . . . . . . . 9
⊢ ((𝑀 · 𝑃) ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
27 | 25, 26 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
→ ∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ ∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
29 | | simp1l 1085 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝜑) |
30 | 29, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑁 ∈ ℕ) |
31 | 29, 14 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑃 = ((2 · 𝑁) + 1)) |
32 | 29, 1 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑃 ∈ ℙ) |
33 | 29, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → (0...(2 · 𝑁)) ⊆ 𝑆) |
34 | | simp1r 1086 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑀 ∈
(ℤ≥‘2)) |
35 | | simp2ll 1128 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑎 ∈ ℤ) |
36 | | simp2lr 1129 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑏 ∈ ℤ) |
37 | | simp2rl 1130 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑐 ∈ ℤ) |
38 | | simp2rr 1131 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → 𝑑 ∈ ℤ) |
39 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑎 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
40 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑏 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
41 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑐 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
42 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑑 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
43 | | eqid 2622 |
. . . . . . . . . . . . 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))) / 𝑀) |
44 | | simp3 1063 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
45 | 12, 30, 31, 32, 33, 7, 6, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44 | 4sqlem17 15665 |
. . . . . . . . . . . 12
⊢ ¬
((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
46 | 45 | pm2.21i 116 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
∧ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) → ¬ 𝑀 ∈
(ℤ≥‘2)) |
47 | 46 | 3expia 1267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ ((𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ)
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ)))
→ ((𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
48 | 47 | anassrs 680 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ (𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ))
∧ (𝑐 ∈ ℤ
∧ 𝑑 ∈ ℤ))
→ ((𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
49 | 48 | rexlimdvva 3038 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
∧ (𝑎 ∈ ℤ
∧ 𝑏 ∈ ℤ))
→ (∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
50 | 49 | rexlimdvva 3038 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
→ (∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ ∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ (𝑀 · 𝑃) = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ¬ 𝑀 ∈
(ℤ≥‘2))) |
51 | 28, 50 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (ℤ≥‘2))
→ ¬ 𝑀 ∈
(ℤ≥‘2)) |
52 | 51 | pm2.01da 458 |
. . . . 5
⊢ (𝜑 → ¬ 𝑀 ∈
(ℤ≥‘2)) |
53 | 24 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
54 | | elnn1uz2 11765 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ ↔ (𝑀 = 1 ∨ 𝑀 ∈
(ℤ≥‘2))) |
55 | 53, 54 | sylib 208 |
. . . . . 6
⊢ (𝜑 → (𝑀 = 1 ∨ 𝑀 ∈
(ℤ≥‘2))) |
56 | 55 | ord 392 |
. . . . 5
⊢ (𝜑 → (¬ 𝑀 = 1 → 𝑀 ∈
(ℤ≥‘2))) |
57 | 52, 56 | mt3d 140 |
. . . 4
⊢ (𝜑 → 𝑀 = 1) |
58 | 57, 20 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → 1 ∈ 𝑇) |
59 | | oveq1 6657 |
. . . . . 6
⊢ (𝑖 = 1 → (𝑖 · 𝑃) = (1 · 𝑃)) |
60 | 59 | eleq1d 2686 |
. . . . 5
⊢ (𝑖 = 1 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (1 · 𝑃) ∈ 𝑆)) |
61 | 60, 7 | elrab2 3366 |
. . . 4
⊢ (1 ∈
𝑇 ↔ (1 ∈ ℕ
∧ (1 · 𝑃) ∈
𝑆)) |
62 | 61 | simprbi 480 |
. . 3
⊢ (1 ∈
𝑇 → (1 · 𝑃) ∈ 𝑆) |
63 | 58, 62 | syl 17 |
. 2
⊢ (𝜑 → (1 · 𝑃) ∈ 𝑆) |
64 | 5, 63 | eqeltrrd 2702 |
1
⊢ (𝜑 → 𝑃 ∈ 𝑆) |