Step | Hyp | Ref
| Expression |
1 | | elnn0 11294 |
. . . 4
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) |
2 | | eleq1 2689 |
. . . . . 6
⊢ (𝑗 = 1 → (𝑗 ∈ 𝑆 ↔ 1 ∈ 𝑆)) |
3 | | eleq1 2689 |
. . . . . 6
⊢ (𝑗 = 𝑚 → (𝑗 ∈ 𝑆 ↔ 𝑚 ∈ 𝑆)) |
4 | | eleq1 2689 |
. . . . . 6
⊢ (𝑗 = 𝑖 → (𝑗 ∈ 𝑆 ↔ 𝑖 ∈ 𝑆)) |
5 | | eleq1 2689 |
. . . . . 6
⊢ (𝑗 = (𝑚 · 𝑖) → (𝑗 ∈ 𝑆 ↔ (𝑚 · 𝑖) ∈ 𝑆)) |
6 | | eleq1 2689 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆)) |
7 | | abs1 14037 |
. . . . . . . . . . 11
⊢
(abs‘1) = 1 |
8 | 7 | oveq1i 6660 |
. . . . . . . . . 10
⊢
((abs‘1)↑2) = (1↑2) |
9 | | sq1 12958 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
10 | 8, 9 | eqtri 2644 |
. . . . . . . . 9
⊢
((abs‘1)↑2) = 1 |
11 | | abs0 14025 |
. . . . . . . . . . 11
⊢
(abs‘0) = 0 |
12 | 11 | oveq1i 6660 |
. . . . . . . . . 10
⊢
((abs‘0)↑2) = (0↑2) |
13 | | sq0 12955 |
. . . . . . . . . 10
⊢
(0↑2) = 0 |
14 | 12, 13 | eqtri 2644 |
. . . . . . . . 9
⊢
((abs‘0)↑2) = 0 |
15 | 10, 14 | oveq12i 6662 |
. . . . . . . 8
⊢
(((abs‘1)↑2) + ((abs‘0)↑2)) = (1 +
0) |
16 | | 1p0e1 11133 |
. . . . . . . 8
⊢ (1 + 0) =
1 |
17 | 15, 16 | eqtri 2644 |
. . . . . . 7
⊢
(((abs‘1)↑2) + ((abs‘0)↑2)) = 1 |
18 | | 1z 11407 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
19 | | zgz 15637 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . 8
⊢ 1 ∈
ℤ[i] |
21 | | 0z 11388 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
22 | | zgz 15637 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → 0 ∈ ℤ[i]) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ∈
ℤ[i] |
24 | | 4sq.1 |
. . . . . . . . 9
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
25 | 24 | 4sqlem4a 15655 |
. . . . . . . 8
⊢ ((1
∈ ℤ[i] ∧ 0 ∈ ℤ[i]) → (((abs‘1)↑2) +
((abs‘0)↑2)) ∈ 𝑆) |
26 | 20, 23, 25 | mp2an 708 |
. . . . . . 7
⊢
(((abs‘1)↑2) + ((abs‘0)↑2)) ∈ 𝑆 |
27 | 17, 26 | eqeltrri 2698 |
. . . . . 6
⊢ 1 ∈
𝑆 |
28 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑗 = 2 → (𝑗 ∈ 𝑆 ↔ 2 ∈ 𝑆)) |
29 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝑗 ∈ (ℙ ∖ {2})
↔ (𝑗 ∈ ℙ
∧ 𝑗 ≠
2)) |
30 | | oddprm 15515 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (ℙ ∖ {2})
→ ((𝑗 − 1) / 2)
∈ ℕ) |
31 | 30 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((𝑗 − 1) / 2) ∈
ℕ) |
32 | | eldifi 3732 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (ℙ ∖ {2})
→ 𝑗 ∈
ℙ) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ ℙ) |
34 | | prmnn 15388 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℙ → 𝑗 ∈
ℕ) |
35 | | nncn 11028 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ ℂ) |
37 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
38 | | subcl 10280 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑗 −
1) ∈ ℂ) |
39 | 36, 37, 38 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (𝑗 − 1) ∈ ℂ) |
40 | | 2cnd 11093 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 2 ∈ ℂ) |
41 | | 2ne0 11113 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 2 ≠ 0) |
43 | 39, 40, 42 | divcan2d 10803 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (2 · ((𝑗 − 1) / 2)) = (𝑗 − 1)) |
44 | 43 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((2 · ((𝑗 − 1) / 2)) + 1) = ((𝑗 − 1) + 1)) |
45 | | npcan 10290 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 −
1) + 1) = 𝑗) |
46 | 36, 37, 45 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((𝑗 − 1) + 1) = 𝑗) |
47 | 44, 46 | eqtr2d 2657 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 = ((2 · ((𝑗 − 1) / 2)) + 1)) |
48 | 43 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(2 · ((𝑗 − 1) / 2))) = (0...(𝑗 − 1))) |
49 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
50 | 33, 34, 49 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (𝑗 − 1) ∈
ℕ0) |
51 | | elnn0uz 11725 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 − 1) ∈
ℕ0 ↔ (𝑗 − 1) ∈
(ℤ≥‘0)) |
52 | 50, 51 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (𝑗 − 1) ∈
(ℤ≥‘0)) |
53 | | eluzfz1 12348 |
. . . . . . . . . . . . 13
⊢ ((𝑗 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑗 − 1))) |
54 | | fzsplit 12367 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(0...(𝑗 − 1)) →
(0...(𝑗 − 1)) =
((0...0) ∪ ((0 + 1)...(𝑗 − 1)))) |
55 | 52, 53, 54 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(𝑗 − 1)) = ((0...0) ∪ ((0 +
1)...(𝑗 −
1)))) |
56 | 48, 55 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(2 · ((𝑗 − 1) / 2))) = ((0...0)
∪ ((0 + 1)...(𝑗 −
1)))) |
57 | | fzsn 12383 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℤ → (0...0) = {0}) |
58 | 21, 57 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (0...0) =
{0} |
59 | 14, 14 | oveq12i 6662 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘0)↑2) + ((abs‘0)↑2)) = (0 +
0) |
60 | | 00id 10211 |
. . . . . . . . . . . . . . . . 17
⊢ (0 + 0) =
0 |
61 | 59, 60 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
⊢
(((abs‘0)↑2) + ((abs‘0)↑2)) = 0 |
62 | 24 | 4sqlem4a 15655 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℤ[i] ∧ 0 ∈ ℤ[i]) → (((abs‘0)↑2) +
((abs‘0)↑2)) ∈ 𝑆) |
63 | 23, 23, 62 | mp2an 708 |
. . . . . . . . . . . . . . . 16
⊢
(((abs‘0)↑2) + ((abs‘0)↑2)) ∈ 𝑆 |
64 | 61, 63 | eqeltrri 2698 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
𝑆 |
65 | | snssi 4339 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
𝑆 → {0} ⊆ 𝑆) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ {0}
⊆ 𝑆 |
67 | 58, 66 | eqsstri 3635 |
. . . . . . . . . . . . 13
⊢ (0...0)
⊆ 𝑆 |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...0) ⊆ 𝑆) |
69 | | 0p1e1 11132 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
70 | 69 | oveq1i 6660 |
. . . . . . . . . . . . 13
⊢ ((0 +
1)...(𝑗 − 1)) =
(1...(𝑗 −
1)) |
71 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ∀𝑚 ∈ (1...(𝑗 − 1))𝑚 ∈ 𝑆) |
72 | | dfss3 3592 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑗 − 1))
⊆ 𝑆 ↔
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) |
73 | 71, 72 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (1...(𝑗 − 1)) ⊆ 𝑆) |
74 | 70, 73 | syl5eqss 3649 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((0 + 1)...(𝑗 − 1)) ⊆ 𝑆) |
75 | 68, 74 | unssd 3789 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((0...0) ∪ ((0 + 1)...(𝑗 − 1))) ⊆ 𝑆) |
76 | 56, 75 | eqsstrd 3639 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(2 · ((𝑗 − 1) / 2))) ⊆ 𝑆) |
77 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 · 𝑗) = (𝑖 · 𝑗)) |
78 | 77 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((𝑘 · 𝑗) ∈ 𝑆 ↔ (𝑖 · 𝑗) ∈ 𝑆)) |
79 | 78 | cbvrabv 3199 |
. . . . . . . . . 10
⊢ {𝑘 ∈ ℕ ∣ (𝑘 · 𝑗) ∈ 𝑆} = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑗) ∈ 𝑆} |
80 | | eqid 2622 |
. . . . . . . . . 10
⊢
inf({𝑘 ∈
ℕ ∣ (𝑘 ·
𝑗) ∈ 𝑆}, ℝ, < ) = inf({𝑘 ∈ ℕ ∣ (𝑘 · 𝑗) ∈ 𝑆}, ℝ, < ) |
81 | 24, 31, 47, 33, 76, 79, 80 | 4sqlem18 15666 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ 𝑆) |
82 | 29, 81 | sylanbr 490 |
. . . . . . . 8
⊢ (((𝑗 ∈ ℙ ∧ 𝑗 ≠ 2) ∧ ∀𝑚 ∈ (1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ 𝑆) |
83 | 82 | an32s 846 |
. . . . . . 7
⊢ (((𝑗 ∈ ℙ ∧
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) ∧ 𝑗 ≠ 2) → 𝑗 ∈ 𝑆) |
84 | 10, 10 | oveq12i 6662 |
. . . . . . . . . 10
⊢
(((abs‘1)↑2) + ((abs‘1)↑2)) = (1 +
1) |
85 | | df-2 11079 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
86 | 84, 85 | eqtr4i 2647 |
. . . . . . . . 9
⊢
(((abs‘1)↑2) + ((abs‘1)↑2)) = 2 |
87 | 24 | 4sqlem4a 15655 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ[i] ∧ 1 ∈ ℤ[i]) → (((abs‘1)↑2) +
((abs‘1)↑2)) ∈ 𝑆) |
88 | 20, 20, 87 | mp2an 708 |
. . . . . . . . 9
⊢
(((abs‘1)↑2) + ((abs‘1)↑2)) ∈ 𝑆 |
89 | 86, 88 | eqeltrri 2698 |
. . . . . . . 8
⊢ 2 ∈
𝑆 |
90 | 89 | a1i 11 |
. . . . . . 7
⊢ ((𝑗 ∈ ℙ ∧
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 2 ∈ 𝑆) |
91 | 28, 83, 90 | pm2.61ne 2879 |
. . . . . 6
⊢ ((𝑗 ∈ ℙ ∧
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ 𝑆) |
92 | 24 | mul4sq 15658 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝑆 ∧ 𝑖 ∈ 𝑆) → (𝑚 · 𝑖) ∈ 𝑆) |
93 | 92 | a1i 11 |
. . . . . 6
⊢ ((𝑚 ∈
(ℤ≥‘2) ∧ 𝑖 ∈ (ℤ≥‘2))
→ ((𝑚 ∈ 𝑆 ∧ 𝑖 ∈ 𝑆) → (𝑚 · 𝑖) ∈ 𝑆)) |
94 | 2, 3, 4, 5, 6, 27,
91, 93 | prmind2 15398 |
. . . . 5
⊢ (𝑘 ∈ ℕ → 𝑘 ∈ 𝑆) |
95 | | id 22 |
. . . . . 6
⊢ (𝑘 = 0 → 𝑘 = 0) |
96 | 95, 64 | syl6eqel 2709 |
. . . . 5
⊢ (𝑘 = 0 → 𝑘 ∈ 𝑆) |
97 | 94, 96 | jaoi 394 |
. . . 4
⊢ ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → 𝑘 ∈ 𝑆) |
98 | 1, 97 | sylbi 207 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈ 𝑆) |
99 | 98 | ssriv 3607 |
. 2
⊢
ℕ0 ⊆ 𝑆 |
100 | 24 | 4sqlem1 15652 |
. 2
⊢ 𝑆 ⊆
ℕ0 |
101 | 99, 100 | eqssi 3619 |
1
⊢
ℕ0 = 𝑆 |