Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (𝑃 mod 4) = 1) |
2 | | simpl 486 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈
ℙ) |
3 | | 1ne2 11936 |
. . . . . . . . . . 11
⊢ 1 ≠
2 |
4 | 3 | necomi 2989 |
. . . . . . . . . 10
⊢ 2 ≠
1 |
5 | | oveq1 7189 |
. . . . . . . . . . . 12
⊢ (𝑃 = 2 → (𝑃 mod 4) = (2 mod 4)) |
6 | | 2re 11802 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
7 | | 4re 11812 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℝ |
8 | | 4pos 11835 |
. . . . . . . . . . . . . 14
⊢ 0 <
4 |
9 | 7, 8 | elrpii 12487 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ+ |
10 | | 0le2 11830 |
. . . . . . . . . . . . 13
⊢ 0 ≤
2 |
11 | | 2lt4 11903 |
. . . . . . . . . . . . 13
⊢ 2 <
4 |
12 | | modid 13367 |
. . . . . . . . . . . . 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 2790 |
. . . . . . . . . . 11
⊢ (𝑃 = 2 → (𝑃 mod 4) = 2) |
15 | 14 | neeq1d 2994 |
. . . . . . . . . 10
⊢ (𝑃 = 2 → ((𝑃 mod 4) ≠ 1 ↔ 2 ≠
1)) |
16 | 4, 15 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (𝑃 mod 4) ≠ 1) |
17 | 16 | necon2i 2969 |
. . . . . . . 8
⊢ ((𝑃 mod 4) = 1 → 𝑃 ≠ 2) |
18 | 1, 17 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ≠ 2) |
19 | | eldifsn 4685 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
20 | 2, 18, 19 | sylanbrc 586 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ (ℙ ∖
{2})) |
21 | | m1lgs 26136 |
. . . . . 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 260 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (-1
/L 𝑃) =
1) |
24 | | neg1z 12111 |
. . . . 5
⊢ -1 ∈
ℤ |
25 | | lgsqr 26099 |
. . . . 5
⊢ ((-1
∈ ℤ ∧ 𝑃
∈ (ℙ ∖ {2})) → ((-1 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ -1 ∧ ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1)))) |
26 | 24, 20, 25 | sylancr 590 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ((-1
/L 𝑃) = 1
↔ (¬ 𝑃 ∥ -1
∧ ∃𝑛 ∈
ℤ 𝑃 ∥ ((𝑛↑2) −
-1)))) |
27 | 23, 26 | mpbid 235 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (¬ 𝑃 ∥ -1 ∧ ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1))) |
28 | 27 | simprd 499 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑛 ∈ ℤ 𝑃 ∥ ((𝑛↑2) − -1)) |
29 | | simprl 771 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑛 ∈
ℤ) |
30 | | 1zzd 12106 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 1 ∈
ℤ) |
31 | | gcd1 15983 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑛 gcd 1) = 1) |
32 | 31 | ad2antrl 728 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → (𝑛 gcd 1) = 1) |
33 | | eqidd 2740 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) + 1) = ((𝑛↑2) + 1)) |
34 | | oveq1 7189 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝑥 gcd 𝑦) = (𝑛 gcd 𝑦)) |
35 | 34 | eqeq1d 2741 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑥 gcd 𝑦) = 1 ↔ (𝑛 gcd 𝑦) = 1)) |
36 | | oveq1 7189 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑥↑2) = (𝑛↑2)) |
37 | 36 | oveq1d 7197 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑥↑2) + (𝑦↑2)) = ((𝑛↑2) + (𝑦↑2))) |
38 | 37 | eqeq2d 2750 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2)))) |
39 | 35, 38 | anbi12d 634 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑛 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2))))) |
40 | | oveq2 7190 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝑛 gcd 𝑦) = (𝑛 gcd 1)) |
41 | 40 | eqeq1d 2741 |
. . . . . . 7
⊢ (𝑦 = 1 → ((𝑛 gcd 𝑦) = 1 ↔ (𝑛 gcd 1) = 1)) |
42 | | oveq1 7189 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (𝑦↑2) = (1↑2)) |
43 | | sq1 13662 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
44 | 42, 43 | eqtrdi 2790 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (𝑦↑2) = 1) |
45 | 44 | oveq2d 7198 |
. . . . . . . 8
⊢ (𝑦 = 1 → ((𝑛↑2) + (𝑦↑2)) = ((𝑛↑2) + 1)) |
46 | 45 | eqeq2d 2750 |
. . . . . . 7
⊢ (𝑦 = 1 → (((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑛↑2) + 1))) |
47 | 41, 46 | anbi12d 634 |
. . . . . 6
⊢ (𝑦 = 1 → (((𝑛 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + (𝑦↑2))) ↔ ((𝑛 gcd 1) = 1 ∧ ((𝑛↑2) + 1) = ((𝑛↑2) + 1)))) |
48 | 39, 47 | rspc2ev 3541 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ∧ 1 ∈
ℤ ∧ ((𝑛 gcd 1) =
1 ∧ ((𝑛↑2) + 1) =
((𝑛↑2) + 1))) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
49 | 29, 30, 32, 33, 48 | syl112anc 1375 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
50 | | ovex 7215 |
. . . . 5
⊢ ((𝑛↑2) + 1) ∈
V |
51 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑧 = ((𝑛↑2) + 1) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
52 | 51 | anbi2d 632 |
. . . . . 6
⊢ (𝑧 = ((𝑛↑2) + 1) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2))))) |
53 | 52 | 2rexbidv 3211 |
. . . . 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 3582 |
. . . 4
⊢ (((𝑛↑2) + 1) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝑛↑2) + 1) = ((𝑥↑2) + (𝑦↑2)))) |
56 | 49, 55 | sylibr 237 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) + 1) ∈ 𝑌) |
57 | | prmnn 16127 |
. . . 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 12181 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑛 ∈
ℂ) |
61 | 60 | sqcld 13612 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → (𝑛↑2) ∈
ℂ) |
62 | | ax-1cn 10685 |
. . . . 5
⊢ 1 ∈
ℂ |
63 | | subneg 11025 |
. . . . 5
⊢ (((𝑛↑2) ∈ ℂ ∧ 1
∈ ℂ) → ((𝑛↑2) − -1) = ((𝑛↑2) + 1)) |
64 | 61, 62, 63 | sylancl 589 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → ((𝑛↑2) − -1) = ((𝑛↑2) + 1)) |
65 | 59, 64 | breqtrd 5066 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∥ ((𝑛↑2) + 1)) |
66 | | 2sq.1 |
. . . 4
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
67 | 66, 54 | 2sqlem10 26176 |
. . 3
⊢ ((((𝑛↑2) + 1) ∈ 𝑌 ∧ 𝑃 ∈ ℕ ∧ 𝑃 ∥ ((𝑛↑2) + 1)) → 𝑃 ∈ 𝑆) |
68 | 56, 58, 65, 67 | syl3anc 1372 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑛 ∈ ℤ ∧ 𝑃 ∥ ((𝑛↑2) − -1))) → 𝑃 ∈ 𝑆) |
69 | 28, 68 | rexlimddv 3202 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) |