| 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 2736 | . . 3
⊢ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} | 
| 6 |  | eqid 2736 | . . 3
⊢ (𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ↦ ((𝑃 − 1) − 𝑣)) = (𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ↦ ((𝑃 − 1) − 𝑣)) | 
| 7 | 1, 2, 3, 4, 5, 6 | 4sqlem12 16995 | . 2
⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) | 
| 8 |  | simplrl 776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ (1...(𝑃 − 1))) | 
| 9 |  | elfznn 13594 | . . . . . . . 8
⊢ (𝑘 ∈ (1...(𝑃 − 1)) → 𝑘 ∈ ℕ) | 
| 10 | 8, 9 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ ℕ) | 
| 11 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) | 
| 12 |  | abs1 15337 | . . . . . . . . . . . 12
⊢
(abs‘1) = 1 | 
| 13 | 12 | oveq1i 7442 | . . . . . . . . . . 11
⊢
((abs‘1)↑2) = (1↑2) | 
| 14 |  | sq1 14235 | . . . . . . . . . . 11
⊢
(1↑2) = 1 | 
| 15 | 13, 14 | eqtri 2764 | . . . . . . . . . 10
⊢
((abs‘1)↑2) = 1 | 
| 16 | 15 | oveq2i 7443 | . . . . . . . . 9
⊢
(((abs‘𝑢)↑2) + ((abs‘1)↑2)) =
(((abs‘𝑢)↑2) +
1) | 
| 17 |  | simplrr 777 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑢 ∈ ℤ[i]) | 
| 18 |  | 1z 12649 | . . . . . . . . . . 11
⊢ 1 ∈
ℤ | 
| 19 |  | zgz 16972 | . . . . . . . . . . 11
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) | 
| 20 | 18, 19 | ax-mp 5 | . . . . . . . . . 10
⊢ 1 ∈
ℤ[i] | 
| 21 | 1 | 4sqlem4a 16990 | . . . . . . . . . 10
⊢ ((𝑢 ∈ ℤ[i] ∧ 1
∈ ℤ[i]) → (((abs‘𝑢)↑2) + ((abs‘1)↑2)) ∈
𝑆) | 
| 22 | 17, 20, 21 | sylancl 586 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (((abs‘𝑢)↑2) + ((abs‘1)↑2)) ∈
𝑆) | 
| 23 | 16, 22 | eqeltrrid 2845 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (((abs‘𝑢)↑2) + 1) ∈ 𝑆) | 
| 24 | 11, 23 | eqeltrrd 2841 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑘 · 𝑃) ∈ 𝑆) | 
| 25 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑖 · 𝑃) = (𝑘 · 𝑃)) | 
| 26 | 25 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑖 = 𝑘 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑘 · 𝑃) ∈ 𝑆)) | 
| 27 |  | 4sq.6 | . . . . . . . 8
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} | 
| 28 | 26, 27 | elrab2 3694 | . . . . . . 7
⊢ (𝑘 ∈ 𝑇 ↔ (𝑘 ∈ ℕ ∧ (𝑘 · 𝑃) ∈ 𝑆)) | 
| 29 | 10, 24, 28 | sylanbrc 583 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ 𝑇) | 
| 30 | 29 | ne0d 4341 | . . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑇 ≠ ∅) | 
| 31 | 27 | ssrab3 4081 | . . . . . . . 8
⊢ 𝑇 ⊆
ℕ | 
| 32 |  | 4sq.7 | . . . . . . . . 9
⊢ 𝑀 = inf(𝑇, ℝ, < ) | 
| 33 |  | nnuz 12922 | . . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) | 
| 34 | 31, 33 | sseqtri 4031 | . . . . . . . . . 10
⊢ 𝑇 ⊆
(ℤ≥‘1) | 
| 35 |  | infssuzcl 12975 | . . . . . . . . . 10
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) | 
| 36 | 34, 30, 35 | sylancr 587 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → inf(𝑇, ℝ, < ) ∈ 𝑇) | 
| 37 | 32, 36 | eqeltrid 2844 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ∈ 𝑇) | 
| 38 | 31, 37 | sselid 3980 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ∈ ℕ) | 
| 39 | 38 | nnred 12282 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ∈ ℝ) | 
| 40 | 10 | nnred 12282 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 ∈ ℝ) | 
| 41 | 4 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℙ) | 
| 42 |  | prmnn 16712 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 43 | 41, 42 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℕ) | 
| 44 | 43 | nnred 12282 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℝ) | 
| 45 |  | infssuzle 12974 | . . . . . . . 8
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑘 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑘) | 
| 46 | 34, 29, 45 | sylancr 587 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → inf(𝑇, ℝ, < ) ≤ 𝑘) | 
| 47 | 32, 46 | eqbrtrid 5177 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 ≤ 𝑘) | 
| 48 |  | prmz 16713 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 49 | 41, 48 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑃 ∈ ℤ) | 
| 50 |  | elfzm11 13636 | . . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝑃
∈ ℤ) → (𝑘
∈ (1...(𝑃 − 1))
↔ (𝑘 ∈ ℤ
∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃))) | 
| 51 | 18, 49, 50 | sylancr 587 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑘 ∈ (1...(𝑃 − 1)) ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃))) | 
| 52 | 8, 51 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑃)) | 
| 53 | 52 | simp3d 1144 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑘 < 𝑃) | 
| 54 | 39, 40, 44, 47, 53 | lelttrd 11420 | . . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → 𝑀 < 𝑃) | 
| 55 | 30, 54 | jca 511 | . . . 4
⊢ (((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) ∧ (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) | 
| 56 | 55 | ex 412 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝑃 − 1)) ∧ 𝑢 ∈ ℤ[i])) →
((((abs‘𝑢)↑2) +
1) = (𝑘 · 𝑃) → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))) | 
| 57 | 56 | rexlimdvva 3212 | . 2
⊢ (𝜑 → (∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃) → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))) | 
| 58 | 7, 57 | mpd 15 | 1
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |