| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (𝑃 mod 4) = 1) |
| 2 | | simpl 482 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈
ℙ) |
| 3 | | 1ne2 12474 |
. . . . . . . . . . 11
⊢ 1 ≠
2 |
| 4 | 3 | necomi 2995 |
. . . . . . . . . 10
⊢ 2 ≠
1 |
| 5 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑃 = 2 → (𝑃 mod 4) = (2 mod 4)) |
| 6 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 7 | | 4re 12350 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℝ |
| 8 | | 4pos 12373 |
. . . . . . . . . . . . . 14
⊢ 0 <
4 |
| 9 | 7, 8 | elrpii 13037 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ+ |
| 10 | | 0le2 12368 |
. . . . . . . . . . . . 13
⊢ 0 ≤
2 |
| 11 | | 2lt4 12441 |
. . . . . . . . . . . . 13
⊢ 2 <
4 |
| 12 | | modid 13936 |
. . . . . . . . . . . . 13
⊢ (((2
∈ ℝ ∧ 4 ∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 <
4)) → (2 mod 4) = 2) |
| 13 | 6, 9, 10, 11, 12 | mp4an 693 |
. . . . . . . . . . . 12
⊢ (2 mod 4)
= 2 |
| 14 | 5, 13 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑃 = 2 → (𝑃 mod 4) = 2) |
| 15 | 14 | neeq1d 3000 |
. . . . . . . . . 10
⊢ (𝑃 = 2 → ((𝑃 mod 4) ≠ 1 ↔ 2 ≠
1)) |
| 16 | 4, 15 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (𝑃 mod 4) ≠ 1) |
| 17 | 16 | necon2i 2975 |
. . . . . . . 8
⊢ ((𝑃 mod 4) = 1 → 𝑃 ≠ 2) |
| 18 | 1, 17 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ≠ 2) |
| 19 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
| 20 | 2, 18, 19 | sylanbrc 583 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ (ℙ ∖
{2})) |
| 21 | | m1lgs 27432 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1)) |
| 22 | 20, 21 | syl 17 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ((-1
/L 𝑃) = 1
↔ (𝑃 mod 4) =
1)) |
| 23 | 1, 22 | mpbird 257 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (-1
/L 𝑃) =
1) |
| 24 | | neg1z 12653 |
. . . . 5
⊢ -1 ∈
ℤ |
| 25 | | lgsqr 27395 |
. . . . 5
⊢ ((-1
∈ ℤ ∧ 𝑃
∈ (ℙ ∖ {2})) → ((-1 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ -1 ∧ ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1)))) |
| 26 | 24, 20, 25 | sylancr 587 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ((-1
/L 𝑃) = 1
↔ (¬ 𝑃 ∥ -1
∧ ∃𝑛 ∈
ℤ 𝑃 ∥ ((𝑛↑2) −
-1)))) |
| 27 | 23, 26 | mpbid 232 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (¬ 𝑃 ∥ -1 ∧ ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1))) |
| 28 | 27 | simprd 495 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1)) |
| 29 | | simprl 771 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑛 ∈
ℤ) |
| 30 | | 1zzd 12648 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 1 ∈
ℤ) |
| 31 | | gcd1 16565 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑛 gcd 1) = 1) |
| 32 | 31 | ad2antrl 728 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → (𝑛 gcd 1) = 1) |
| 33 | | eqidd 2738 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) + 1) = ((𝑛↑2) + 1)) |
| 34 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝑥 gcd 𝑦) = (𝑛 gcd 𝑦)) |
| 35 | 34 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑥 gcd 𝑦) = 1 ↔ (𝑛 gcd 𝑦) = 1)) |
| 36 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑥↑2) = (𝑛↑2)) |
| 37 | 36 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑥↑2) + (𝑦↑2)) = ((𝑛↑2) + (𝑦↑2))) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2)))) |
| 39 | 35, 38 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑛 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2))))) |
| 40 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝑛 gcd 𝑦) = (𝑛 gcd 1)) |
| 41 | 40 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑦 = 1 → ((𝑛 gcd 𝑦) = 1 ↔ (𝑛 gcd 1) = 1)) |
| 42 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (𝑦↑2) = (1↑2)) |
| 43 | | sq1 14234 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
| 44 | 42, 43 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (𝑦↑2) = 1) |
| 45 | 44 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑦 = 1 → ((𝑛↑2) + (𝑦↑2)) = ((𝑛↑2) + 1)) |
| 46 | 45 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 1 → (((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑛↑2) + 1))) |
| 47 | 41, 46 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 1 → (((𝑛 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2))) ↔ ((𝑛 gcd 1) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + 1)))) |
| 48 | 39, 47 | rspc2ev 3635 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℤ ∧ ((𝑛 gcd 1) =
1 ∧ ((𝑛↑2) + 1) =
((𝑛↑2) + 1))) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
| 49 | 29, 30, 32, 33, 48 | syl112anc 1376 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
| 50 | | ovex 7464 |
. . . . 5
⊢ ((𝑛↑2) + 1) ∈
V |
| 51 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑧 = ((𝑛↑2) + 1) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
| 52 | 51 | anbi2d 630 |
. . . . . 6
⊢ (𝑧 = ((𝑛↑2) + 1) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))))) |
| 53 | 52 | 2rexbidv 3222 |
. . . . 5
⊢ (𝑧 = ((𝑛↑2) + 1) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))))) |
| 54 | | 2sqlem7.2 |
. . . . 5
⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} |
| 55 | 50, 53, 54 | elab2 3682 |
. . . 4
⊢ (((𝑛↑2) + 1) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
| 56 | 49, 55 | sylibr 234 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) + 1) ∈ 𝑌) |
| 57 | | prmnn 16711 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 58 | 57 | ad2antrr 726 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∈
ℕ) |
| 59 | | simprr 773 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∥ ((𝑛↑2) − -1)) |
| 60 | 29 | zcnd 12723 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑛 ∈
ℂ) |
| 61 | 60 | sqcld 14184 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → (𝑛↑2) ∈
ℂ) |
| 62 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 63 | | subneg 11558 |
. . . . 5
⊢ (((𝑛↑2) ∈ ℂ ∧ 1
∈ ℂ) → ((𝑛↑2) − -1) = ((𝑛↑2) + 1)) |
| 64 | 61, 62, 63 | sylancl 586 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) − -1) = ((𝑛↑2) + 1)) |
| 65 | 59, 64 | breqtrd 5169 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∥ ((𝑛↑2) + 1)) |
| 66 | | 2sq.1 |
. . . 4
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
| 67 | 66, 54 | 2sqlem10 27472 |
. . 3
⊢ ((((𝑛↑2) + 1) ∈ 𝑌 ∧ 𝑃 ∈ ℕ ∧ 𝑃 ∥ ((𝑛↑2) + 1)) → 𝑃 ∈ 𝑆) |
| 68 | 56, 58, 65, 67 | syl3anc 1373 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∈ 𝑆) |
| 69 | 28, 68 | rexlimddv 3161 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) |