| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elnn0 12528 | . . . 4
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) | 
| 2 |  | eleq1 2829 | . . . . . 6
⊢ (𝑗 = 1 → (𝑗 ∈ 𝑆 ↔ 1 ∈ 𝑆)) | 
| 3 |  | eleq1 2829 | . . . . . 6
⊢ (𝑗 = 𝑚 → (𝑗 ∈ 𝑆 ↔ 𝑚 ∈ 𝑆)) | 
| 4 |  | eleq1 2829 | . . . . . 6
⊢ (𝑗 = 𝑖 → (𝑗 ∈ 𝑆 ↔ 𝑖 ∈ 𝑆)) | 
| 5 |  | eleq1 2829 | . . . . . 6
⊢ (𝑗 = (𝑚 · 𝑖) → (𝑗 ∈ 𝑆 ↔ (𝑚 · 𝑖) ∈ 𝑆)) | 
| 6 |  | eleq1 2829 | . . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆)) | 
| 7 |  | abs1 15336 | . . . . . . . . . . 11
⊢
(abs‘1) = 1 | 
| 8 | 7 | oveq1i 7441 | . . . . . . . . . 10
⊢
((abs‘1)↑2) = (1↑2) | 
| 9 |  | sq1 14234 | . . . . . . . . . 10
⊢
(1↑2) = 1 | 
| 10 | 8, 9 | eqtri 2765 | . . . . . . . . 9
⊢
((abs‘1)↑2) = 1 | 
| 11 |  | abs0 15324 | . . . . . . . . . . 11
⊢
(abs‘0) = 0 | 
| 12 | 11 | oveq1i 7441 | . . . . . . . . . 10
⊢
((abs‘0)↑2) = (0↑2) | 
| 13 |  | sq0 14231 | . . . . . . . . . 10
⊢
(0↑2) = 0 | 
| 14 | 12, 13 | eqtri 2765 | . . . . . . . . 9
⊢
((abs‘0)↑2) = 0 | 
| 15 | 10, 14 | oveq12i 7443 | . . . . . . . 8
⊢
(((abs‘1)↑2) + ((abs‘0)↑2)) = (1 +
0) | 
| 16 |  | 1p0e1 12390 | . . . . . . . 8
⊢ (1 + 0) =
1 | 
| 17 | 15, 16 | eqtri 2765 | . . . . . . 7
⊢
(((abs‘1)↑2) + ((abs‘0)↑2)) = 1 | 
| 18 |  | 1z 12647 | . . . . . . . . 9
⊢ 1 ∈
ℤ | 
| 19 |  | zgz 16971 | . . . . . . . . 9
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) | 
| 20 | 18, 19 | ax-mp 5 | . . . . . . . 8
⊢ 1 ∈
ℤ[i] | 
| 21 |  | 0z 12624 | . . . . . . . . 9
⊢ 0 ∈
ℤ | 
| 22 |  | zgz 16971 | . . . . . . . . 9
⊢ (0 ∈
ℤ → 0 ∈ ℤ[i]) | 
| 23 | 21, 22 | ax-mp 5 | . . . . . . . 8
⊢ 0 ∈
ℤ[i] | 
| 24 |  | 4sq.1 | . . . . . . . . 9
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} | 
| 25 | 24 | 4sqlem4a 16989 | . . . . . . . 8
⊢ ((1
∈ ℤ[i] ∧ 0 ∈ ℤ[i]) → (((abs‘1)↑2) +
((abs‘0)↑2)) ∈ 𝑆) | 
| 26 | 20, 23, 25 | mp2an 692 | . . . . . . 7
⊢
(((abs‘1)↑2) + ((abs‘0)↑2)) ∈ 𝑆 | 
| 27 | 17, 26 | eqeltrri 2838 | . . . . . 6
⊢ 1 ∈
𝑆 | 
| 28 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑗 = 2 → (𝑗 ∈ 𝑆 ↔ 2 ∈ 𝑆)) | 
| 29 |  | eldifsn 4786 | . . . . . . . . 9
⊢ (𝑗 ∈ (ℙ ∖ {2})
↔ (𝑗 ∈ ℙ
∧ 𝑗 ≠
2)) | 
| 30 |  | oddprm 16848 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (ℙ ∖ {2})
→ ((𝑗 − 1) / 2)
∈ ℕ) | 
| 31 | 30 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((𝑗 − 1) / 2) ∈
ℕ) | 
| 32 |  | eldifi 4131 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (ℙ ∖ {2})
→ 𝑗 ∈
ℙ) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ ℙ) | 
| 34 |  | prmnn 16711 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℙ → 𝑗 ∈
ℕ) | 
| 35 |  | nncn 12274 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) | 
| 36 | 33, 34, 35 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ ℂ) | 
| 37 |  | ax-1cn 11213 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ | 
| 38 |  | subcl 11507 | . . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑗 −
1) ∈ ℂ) | 
| 39 | 36, 37, 38 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (𝑗 − 1) ∈ ℂ) | 
| 40 |  | 2cnd 12344 | . . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 2 ∈ ℂ) | 
| 41 |  | 2ne0 12370 | . . . . . . . . . . . . . 14
⊢ 2 ≠
0 | 
| 42 | 41 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 2 ≠ 0) | 
| 43 | 39, 40, 42 | divcan2d 12045 | . . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (2 · ((𝑗 − 1) / 2)) = (𝑗 − 1)) | 
| 44 | 43 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((2 · ((𝑗 − 1) / 2)) + 1) = ((𝑗 − 1) + 1)) | 
| 45 |  | npcan 11517 | . . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 −
1) + 1) = 𝑗) | 
| 46 | 36, 37, 45 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((𝑗 − 1) + 1) = 𝑗) | 
| 47 | 44, 46 | eqtr2d 2778 | . . . . . . . . . 10
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 = ((2 · ((𝑗 − 1) / 2)) + 1)) | 
| 48 | 43 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(2 · ((𝑗 − 1) / 2))) = (0...(𝑗 − 1))) | 
| 49 |  | nnm1nn0 12567 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) | 
| 50 | 33, 34, 49 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (𝑗 − 1) ∈
ℕ0) | 
| 51 |  | elnn0uz 12923 | . . . . . . . . . . . . . 14
⊢ ((𝑗 − 1) ∈
ℕ0 ↔ (𝑗 − 1) ∈
(ℤ≥‘0)) | 
| 52 | 50, 51 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (𝑗 − 1) ∈
(ℤ≥‘0)) | 
| 53 |  | eluzfz1 13571 | . . . . . . . . . . . . 13
⊢ ((𝑗 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑗 − 1))) | 
| 54 |  | fzsplit 13590 | . . . . . . . . . . . . 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 2777 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(2 · ((𝑗 − 1) / 2))) = ((0...0)
∪ ((0 + 1)...(𝑗 −
1)))) | 
| 57 |  | fz0sn 13667 | . . . . . . . . . . . . . 14
⊢ (0...0) =
{0} | 
| 58 | 14, 14 | oveq12i 7443 | . . . . . . . . . . . . . . . . 17
⊢
(((abs‘0)↑2) + ((abs‘0)↑2)) = (0 +
0) | 
| 59 |  | 00id 11436 | . . . . . . . . . . . . . . . . 17
⊢ (0 + 0) =
0 | 
| 60 | 58, 59 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢
(((abs‘0)↑2) + ((abs‘0)↑2)) = 0 | 
| 61 | 24 | 4sqlem4a 16989 | . . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℤ[i] ∧ 0 ∈ ℤ[i]) → (((abs‘0)↑2) +
((abs‘0)↑2)) ∈ 𝑆) | 
| 62 | 23, 23, 61 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢
(((abs‘0)↑2) + ((abs‘0)↑2)) ∈ 𝑆 | 
| 63 | 60, 62 | eqeltrri 2838 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
𝑆 | 
| 64 |  | snssi 4808 | . . . . . . . . . . . . . . 15
⊢ (0 ∈
𝑆 → {0} ⊆ 𝑆) | 
| 65 | 63, 64 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ {0}
⊆ 𝑆 | 
| 66 | 57, 65 | eqsstri 4030 | . . . . . . . . . . . . 13
⊢ (0...0)
⊆ 𝑆 | 
| 67 | 66 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...0) ⊆ 𝑆) | 
| 68 |  | 0p1e1 12388 | . . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 | 
| 69 | 68 | oveq1i 7441 | . . . . . . . . . . . . 13
⊢ ((0 +
1)...(𝑗 − 1)) =
(1...(𝑗 −
1)) | 
| 70 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ∀𝑚 ∈ (1...(𝑗 − 1))𝑚 ∈ 𝑆) | 
| 71 |  | dfss3 3972 | . . . . . . . . . . . . . 14
⊢
((1...(𝑗 − 1))
⊆ 𝑆 ↔
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) | 
| 72 | 70, 71 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (1...(𝑗 − 1)) ⊆ 𝑆) | 
| 73 | 69, 72 | eqsstrid 4022 | . . . . . . . . . . . 12
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((0 + 1)...(𝑗 − 1)) ⊆ 𝑆) | 
| 74 | 67, 73 | unssd 4192 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → ((0...0) ∪ ((0 + 1)...(𝑗 − 1))) ⊆ 𝑆) | 
| 75 | 56, 74 | eqsstrd 4018 | . . . . . . . . . 10
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → (0...(2 · ((𝑗 − 1) / 2))) ⊆ 𝑆) | 
| 76 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 · 𝑗) = (𝑖 · 𝑗)) | 
| 77 | 76 | eleq1d 2826 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((𝑘 · 𝑗) ∈ 𝑆 ↔ (𝑖 · 𝑗) ∈ 𝑆)) | 
| 78 | 77 | cbvrabv 3447 | . . . . . . . . . 10
⊢ {𝑘 ∈ ℕ ∣ (𝑘 · 𝑗) ∈ 𝑆} = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑗) ∈ 𝑆} | 
| 79 |  | eqid 2737 | . . . . . . . . . 10
⊢
inf({𝑘 ∈
ℕ ∣ (𝑘 ·
𝑗) ∈ 𝑆}, ℝ, < ) = inf({𝑘 ∈ ℕ ∣ (𝑘 · 𝑗) ∈ 𝑆}, ℝ, < ) | 
| 80 | 24, 31, 47, 33, 75, 78, 79 | 4sqlem18 17000 | . . . . . . . . 9
⊢ ((𝑗 ∈ (ℙ ∖ {2})
∧ ∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ 𝑆) | 
| 81 | 29, 80 | sylanbr 582 | . . . . . . . 8
⊢ (((𝑗 ∈ ℙ ∧ 𝑗 ≠ 2) ∧ ∀𝑚 ∈ (1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ 𝑆) | 
| 82 | 81 | an32s 652 | . . . . . . 7
⊢ (((𝑗 ∈ ℙ ∧
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) ∧ 𝑗 ≠ 2) → 𝑗 ∈ 𝑆) | 
| 83 | 10, 10 | oveq12i 7443 | . . . . . . . . . 10
⊢
(((abs‘1)↑2) + ((abs‘1)↑2)) = (1 +
1) | 
| 84 |  | df-2 12329 | . . . . . . . . . 10
⊢ 2 = (1 +
1) | 
| 85 | 83, 84 | eqtr4i 2768 | . . . . . . . . 9
⊢
(((abs‘1)↑2) + ((abs‘1)↑2)) = 2 | 
| 86 | 24 | 4sqlem4a 16989 | . . . . . . . . . 10
⊢ ((1
∈ ℤ[i] ∧ 1 ∈ ℤ[i]) → (((abs‘1)↑2) +
((abs‘1)↑2)) ∈ 𝑆) | 
| 87 | 20, 20, 86 | mp2an 692 | . . . . . . . . 9
⊢
(((abs‘1)↑2) + ((abs‘1)↑2)) ∈ 𝑆 | 
| 88 | 85, 87 | eqeltrri 2838 | . . . . . . . 8
⊢ 2 ∈
𝑆 | 
| 89 | 88 | a1i 11 | . . . . . . 7
⊢ ((𝑗 ∈ ℙ ∧
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 2 ∈ 𝑆) | 
| 90 | 28, 82, 89 | pm2.61ne 3027 | . . . . . 6
⊢ ((𝑗 ∈ ℙ ∧
∀𝑚 ∈
(1...(𝑗 − 1))𝑚 ∈ 𝑆) → 𝑗 ∈ 𝑆) | 
| 91 | 24 | mul4sq 16992 | . . . . . . 7
⊢ ((𝑚 ∈ 𝑆 ∧ 𝑖 ∈ 𝑆) → (𝑚 · 𝑖) ∈ 𝑆) | 
| 92 | 91 | a1i 11 | . . . . . 6
⊢ ((𝑚 ∈
(ℤ≥‘2) ∧ 𝑖 ∈ (ℤ≥‘2))
→ ((𝑚 ∈ 𝑆 ∧ 𝑖 ∈ 𝑆) → (𝑚 · 𝑖) ∈ 𝑆)) | 
| 93 | 2, 3, 4, 5, 6, 27,
90, 92 | prmind2 16722 | . . . . 5
⊢ (𝑘 ∈ ℕ → 𝑘 ∈ 𝑆) | 
| 94 |  | id 22 | . . . . . 6
⊢ (𝑘 = 0 → 𝑘 = 0) | 
| 95 | 94, 63 | eqeltrdi 2849 | . . . . 5
⊢ (𝑘 = 0 → 𝑘 ∈ 𝑆) | 
| 96 | 93, 95 | jaoi 858 | . . . 4
⊢ ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → 𝑘 ∈ 𝑆) | 
| 97 | 1, 96 | sylbi 217 | . . 3
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈ 𝑆) | 
| 98 | 97 | ssriv 3987 | . 2
⊢
ℕ0 ⊆ 𝑆 | 
| 99 | 24 | 4sqlem1 16986 | . 2
⊢ 𝑆 ⊆
ℕ0 | 
| 100 | 98, 99 | eqssi 4000 | 1
⊢
ℕ0 = 𝑆 |