Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (𝑃 mod 4) = 1) |
2 | | simpl 483 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈
ℙ) |
3 | | 1ne2 12181 |
. . . . . . . . . . 11
⊢ 1 ≠
2 |
4 | 3 | necomi 2998 |
. . . . . . . . . 10
⊢ 2 ≠
1 |
5 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑃 = 2 → (𝑃 mod 4) = (2 mod 4)) |
6 | | 2re 12047 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
7 | | 4re 12057 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℝ |
8 | | 4pos 12080 |
. . . . . . . . . . . . . 14
⊢ 0 <
4 |
9 | 7, 8 | elrpii 12733 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ+ |
10 | | 0le2 12075 |
. . . . . . . . . . . . 13
⊢ 0 ≤
2 |
11 | | 2lt4 12148 |
. . . . . . . . . . . . 13
⊢ 2 <
4 |
12 | | modid 13616 |
. . . . . . . . . . . . 13
⊢ (((2
∈ ℝ ∧ 4 ∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 <
4)) → (2 mod 4) = 2) |
13 | 6, 9, 10, 11, 12 | mp4an 690 |
. . . . . . . . . . . 12
⊢ (2 mod 4)
= 2 |
14 | 5, 13 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑃 = 2 → (𝑃 mod 4) = 2) |
15 | 14 | neeq1d 3003 |
. . . . . . . . . 10
⊢ (𝑃 = 2 → ((𝑃 mod 4) ≠ 1 ↔ 2 ≠
1)) |
16 | 4, 15 | mpbiri 257 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (𝑃 mod 4) ≠ 1) |
17 | 16 | necon2i 2978 |
. . . . . . . 8
⊢ ((𝑃 mod 4) = 1 → 𝑃 ≠ 2) |
18 | 1, 17 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ≠ 2) |
19 | | eldifsn 4720 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
20 | 2, 18, 19 | sylanbrc 583 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ (ℙ ∖
{2})) |
21 | | m1lgs 26536 |
. . . . . 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 256 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (-1
/L 𝑃) =
1) |
24 | | neg1z 12356 |
. . . . 5
⊢ -1 ∈
ℤ |
25 | | lgsqr 26499 |
. . . . 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 231 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (¬ 𝑃 ∥ -1 ∧ ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1))) |
28 | 27 | simprd 496 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1)) |
29 | | simprl 768 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑛 ∈
ℤ) |
30 | | 1zzd 12351 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 1 ∈
ℤ) |
31 | | gcd1 16235 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑛 gcd 1) = 1) |
32 | 31 | ad2antrl 725 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → (𝑛 gcd 1) = 1) |
33 | | eqidd 2739 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) + 1) = ((𝑛↑2) + 1)) |
34 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝑥 gcd 𝑦) = (𝑛 gcd 𝑦)) |
35 | 34 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑥 gcd 𝑦) = 1 ↔ (𝑛 gcd 𝑦) = 1)) |
36 | | oveq1 7282 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑥↑2) = (𝑛↑2)) |
37 | 36 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑥↑2) + (𝑦↑2)) = ((𝑛↑2) + (𝑦↑2))) |
38 | 37 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2)))) |
39 | 35, 38 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑛 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2))))) |
40 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝑛 gcd 𝑦) = (𝑛 gcd 1)) |
41 | 40 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑦 = 1 → ((𝑛 gcd 𝑦) = 1 ↔ (𝑛 gcd 1) = 1)) |
42 | | oveq1 7282 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (𝑦↑2) = (1↑2)) |
43 | | sq1 13912 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
44 | 42, 43 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (𝑦↑2) = 1) |
45 | 44 | oveq2d 7291 |
. . . . . . . 8
⊢ (𝑦 = 1 → ((𝑛↑2) + (𝑦↑2)) = ((𝑛↑2) + 1)) |
46 | 45 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 = 1 → (((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑛↑2) + 1))) |
47 | 41, 46 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = 1 → (((𝑛 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2))) ↔ ((𝑛 gcd 1) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + 1)))) |
48 | 39, 47 | rspc2ev 3572 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℤ ∧ ((𝑛 gcd 1) =
1 ∧ ((𝑛↑2) + 1) =
((𝑛↑2) + 1))) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
49 | 29, 30, 32, 33, 48 | syl112anc 1373 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
50 | | ovex 7308 |
. . . . 5
⊢ ((𝑛↑2) + 1) ∈
V |
51 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑧 = ((𝑛↑2) + 1) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
52 | 51 | anbi2d 629 |
. . . . . 6
⊢ (𝑧 = ((𝑛↑2) + 1) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))))) |
53 | 52 | 2rexbidv 3229 |
. . . . 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 3613 |
. . . 4
⊢ (((𝑛↑2) + 1) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
56 | 49, 55 | sylibr 233 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) + 1) ∈ 𝑌) |
57 | | prmnn 16379 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
58 | 57 | ad2antrr 723 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∈
ℕ) |
59 | | simprr 770 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∥ ((𝑛↑2) − -1)) |
60 | 29 | zcnd 12427 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑛 ∈
ℂ) |
61 | 60 | sqcld 13862 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → (𝑛↑2) ∈
ℂ) |
62 | | ax-1cn 10929 |
. . . . 5
⊢ 1 ∈
ℂ |
63 | | subneg 11270 |
. . . . 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 5100 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∥ ((𝑛↑2) + 1)) |
66 | | 2sq.1 |
. . . 4
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
67 | 66, 54 | 2sqlem10 26576 |
. . 3
⊢ ((((𝑛↑2) + 1) ∈ 𝑌 ∧ 𝑃 ∈ ℕ ∧ 𝑃 ∥ ((𝑛↑2) + 1)) → 𝑃 ∈ 𝑆) |
68 | 56, 58, 65, 67 | syl3anc 1370 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∈ 𝑆) |
69 | 28, 68 | rexlimddv 3220 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) |