Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . 3
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
2 | | 4sq.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | | 4sq.3 |
. . 3
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
4 | | 4sq.4 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
5 | | eqid 2610 |
. . 3
⊢ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} |
6 | | eqid 2610 |
. . 3
⊢ (𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ↦ ((𝑃 − 1) − 𝑣)) = (𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ↦ ((𝑃 − 1) − 𝑣)) |
7 | 1, 2, 3, 4, 5, 6 | 4sqlem12 15498 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) |
8 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ (1...(𝑃 − 1))) |
9 | | elfznn 12241 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...(𝑃 − 1)) → 𝑘 ∈ ℕ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ ℕ) |
11 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) |
12 | | abs1 13885 |
. . . . . . . . . . . 12
⊢
(abs‘1) = 1 |
13 | 12 | oveq1i 6559 |
. . . . . . . . . . 11
⊢
((abs‘1)↑2) = (1↑2) |
14 | | sq1 12820 |
. . . . . . . . . . 11
⊢
(1↑2) = 1 |
15 | 13, 14 | eqtri 2632 |
. . . . . . . . . 10
⊢
((abs‘1)↑2) = 1 |
16 | 15 | oveq2i 6560 |
. . . . . . . . 9
⊢
(((abs‘𝑢)↑2) + ((abs‘1)↑2)) =
(((abs‘𝑢)↑2) +
1) |
17 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑢 ∈ ℤ[i]) |
18 | | 1z 11284 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
19 | | zgz 15475 |
. . . . . . . . . . 11
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ[i] |
21 | 1 | 4sqlem4a 15493 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℤ[i] ∧ 1
∈ ℤ[i]) → (((abs‘𝑢)↑2) + ((abs‘1)↑2)) ∈
𝑆) |
22 | 17, 20, 21 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (((abs‘𝑢)↑2) + ((abs‘1)↑2)) ∈
𝑆) |
23 | 16, 22 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (((abs‘𝑢)↑2) + 1) ∈ 𝑆) |
24 | 11, 23 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑘 · 𝑃) ∈ 𝑆) |
25 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑖 · 𝑃) = (𝑘 · 𝑃)) |
26 | 25 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑘 · 𝑃) ∈ 𝑆)) |
27 | | 4sq.6 |
. . . . . . . 8
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
28 | 26, 27 | elrab2 3333 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑇 ↔ (𝑘 ∈ ℕ ∧ (𝑘 · 𝑃) ∈ 𝑆)) |
29 | 10, 24, 28 | sylanbrc 695 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ 𝑇) |
30 | | ne0i 3880 |
. . . . . 6
⊢ (𝑘 ∈ 𝑇 → 𝑇 ≠ ∅) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑇 ≠ ∅) |
32 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ |
33 | 27, 32 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑇 ⊆
ℕ |
34 | | 4sq.7 |
. . . . . . . . 9
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
35 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
36 | 33, 35 | sseqtri 3600 |
. . . . . . . . . 10
⊢ 𝑇 ⊆
(ℤ≥‘1) |
37 | | infssuzcl 11648 |
. . . . . . . . . 10
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
38 | 36, 31, 37 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
39 | 34, 38 | syl5eqel 2692 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ∈ 𝑇) |
40 | 33, 39 | sseldi 3566 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ∈ ℕ) |
41 | 40 | nnred 10912 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ∈ ℝ) |
42 | 10 | nnred 10912 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ ℝ) |
43 | 4 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℙ) |
44 | | prmnn 15226 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℕ) |
46 | 45 | nnred 10912 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℝ) |
47 | | infssuzle 11647 |
. . . . . . . 8
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑘 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑘) |
48 | 36, 29, 47 | sylancr 694 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → inf(𝑇, ℝ, < ) ≤ 𝑘) |
49 | 34, 48 | syl5eqbr 4618 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ≤ 𝑘) |
50 | | prmz 15227 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
51 | 43, 50 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℤ) |
52 | | elfzm11 12280 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝑃
∈ ℤ) → (𝑘
∈ (1...(𝑃 − 1))
↔ (𝑘 ∈ ℤ
∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃))) |
53 | 18, 51, 52 | sylancr 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑘 ∈ (1...(𝑃 − 1)) ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃))) |
54 | 8, 53 | mpbid 221 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃)) |
55 | 54 | simp3d 1068 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 < 𝑃) |
56 | 41, 42, 46, 49, 55 | lelttrd 10074 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 < 𝑃) |
57 | 31, 56 | jca 553 |
. . . 4
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
58 | 57 | ex 449 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) →
((((abs‘𝑢)↑2) +
1) = (𝑘 · 𝑃) → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))) |
59 | 58 | rexlimdvva 3020 |
. 2
⊢ (𝜑 → (∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃) → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))) |
60 | 7, 59 | mpd 15 |
1
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |