Step | Hyp | Ref
| Expression |
1 | | 2nn 11932 |
. . . 4
⊢ 2 ∈
ℕ |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℕ) |
3 | | proththd.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | 3 | nnnn0d 12179 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | 2, 4 | nnexpcld 13844 |
. 2
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
6 | | proththd.k |
. 2
⊢ (𝜑 → 𝐾 ∈ ℕ) |
7 | | proththd.l |
. 2
⊢ (𝜑 → 𝐾 < (2↑𝑁)) |
8 | | proththd.p |
. . 3
⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) |
9 | 6 | nncnd 11875 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℂ) |
10 | 5 | nncnd 11875 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) |
11 | 9, 10 | mulcomd 10883 |
. . . 4
⊢ (𝜑 → (𝐾 · (2↑𝑁)) = ((2↑𝑁) · 𝐾)) |
12 | 11 | oveq1d 7249 |
. . 3
⊢ (𝜑 → ((𝐾 · (2↑𝑁)) + 1) = (((2↑𝑁) · 𝐾) + 1)) |
13 | 8, 12 | eqtrd 2779 |
. 2
⊢ (𝜑 → 𝑃 = (((2↑𝑁) · 𝐾) + 1)) |
14 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
15 | | 2prm 16281 |
. . . . . 6
⊢ 2 ∈
ℙ |
16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈
ℙ) |
17 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ) |
18 | | prmdvdsexpb 16305 |
. . . . 5
⊢ ((𝑝 ∈ ℙ ∧ 2 ∈
ℙ ∧ 𝑁 ∈
ℕ) → (𝑝 ∥
(2↑𝑁) ↔ 𝑝 = 2)) |
19 | 14, 16, 17, 18 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) ↔ 𝑝 = 2)) |
20 | | proththd.x |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) |
21 | 3, 6, 8 | proththdlem 44783 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈
ℕ)) |
22 | 21 | simp1d 1144 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ ℕ) |
23 | 22 | nncnd 11875 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ ℂ) |
24 | | peano2cnm 11173 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℂ → (𝑃 − 1) ∈
ℂ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
26 | 25 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) ∈ ℂ) |
27 | | 2cnd 11937 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈
ℂ) |
28 | | 2ne0 11963 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ≠
0) |
30 | 26, 27, 29 | divcan1d 11638 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1)) |
31 | 30 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) = (((𝑃 − 1) / 2) ·
2)) |
32 | 31 | oveq2d 7250 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = (𝑥↑(((𝑃 − 1) / 2) ·
2))) |
33 | | zcn 12210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
34 | 33 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ) |
35 | | 2nn0 12136 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈
ℕ0) |
37 | 21 | simp3d 1146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
38 | 37 | nnnn0d 12179 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
39 | 38 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑃 − 1) / 2) ∈
ℕ0) |
40 | 34, 36, 39 | expmuld 13751 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(((𝑃 − 1) / 2) · 2)) = ((𝑥↑((𝑃 − 1) / 2))↑2)) |
41 | 32, 40 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2)) |
42 | 41 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2)) |
43 | 42 | oveq1d 7249 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃)) |
44 | 38 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 2) ∈
ℕ0) |
45 | 44 | anim1i 618 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) ∈ ℕ0
∧ 𝑥 ∈
ℤ)) |
46 | 45 | ancomd 465 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0)) |
47 | | zexpcl 13681 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝑥↑((𝑃 − 1) / 2)) ∈
ℤ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 2)) ∈
ℤ) |
49 | 48 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 2)) ∈
ℤ) |
50 | 22 | nnrpd 12655 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
51 | 50 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 𝑃 ∈
ℝ+) |
52 | 21 | simp2d 1145 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 𝑃) |
53 | 52 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 < 𝑃) |
54 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) |
55 | 49, 51, 53, 54 | modexp2m1d 44782 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃) = 1) |
56 | 43, 55 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = 1) |
57 | | oveq2 7242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 2 → ((𝑃 − 1) / 𝑝) = ((𝑃 − 1) / 2)) |
58 | 57 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 2 → (((𝑃 − 1) / 𝑝) ∈ ℕ0 ↔ ((𝑃 − 1) / 2) ∈
ℕ0)) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑃 − 1) / 𝑝) ∈ ℕ0 ↔ ((𝑃 − 1) / 2) ∈
ℕ0)) |
60 | 44, 59 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 𝑝) ∈
ℕ0) |
61 | 60 | anim2i 620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ (𝜑 ∧ 𝑝 = 2)) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈
ℕ0)) |
62 | 61 | ancoms 462 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈
ℕ0)) |
63 | | zexpcl 13681 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ0) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ) |
65 | 64 | zred 12311 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ) |
67 | | 1red 10863 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 ∈ ℝ) |
68 | 67 | renegcld 11288 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → -1 ∈
ℝ) |
69 | | oveq2 7242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 =
𝑝 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝)) |
70 | 69 | eqcoms 2747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 2 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝)) |
71 | 70 | oveq2d 7250 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 2 → (𝑥↑((𝑃 − 1) / 2)) = (𝑥↑((𝑃 − 1) / 𝑝))) |
72 | 71 | oveq1d 7249 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 2 → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃)) |
73 | 72 | eqeq1d 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 2 → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))) |
74 | 73 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))) |
75 | 74 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))) |
76 | 75 | biimpa 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃)) |
77 | | eqidd 2740 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (1 mod 𝑃) = (1 mod 𝑃)) |
78 | 66, 68, 67, 67, 51, 76, 77 | modsub12d 13532 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) = ((-1 − 1) mod 𝑃)) |
79 | 78 | oveq1d 7249 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((-1 − 1) mod 𝑃) gcd 𝑃)) |
80 | | peano2zm 12249 |
. . . . . . . . . . . . . 14
⊢ ((𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈
ℤ) |
81 | 64, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈
ℤ) |
82 | 22 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → 𝑃 ∈ ℕ) |
83 | | modgcd 16124 |
. . . . . . . . . . . . 13
⊢ ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃)) |
84 | 81, 82, 83 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃)) |
85 | 84 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃)) |
86 | | ax-1cn 10816 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
87 | | negdi2 11165 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ) → -(1 + 1) = (-1 −
1)) |
88 | 87 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ) → (-1 − 1) = -(1 +
1)) |
89 | 86, 86, 88 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (-1
− 1) = -(1 + 1) |
90 | | 1p1e2 11984 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1) =
2 |
91 | 90 | negeqi 11100 |
. . . . . . . . . . . . . . . . 17
⊢ -(1 + 1)
= -2 |
92 | 89, 91 | eqtri 2767 |
. . . . . . . . . . . . . . . 16
⊢ (-1
− 1) = -2 |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (-1 − 1) =
-2) |
94 | 93 | oveq1d 7249 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((-1 − 1) mod 𝑃) = (-2 mod 𝑃)) |
95 | 94 | oveq1d 7249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = ((-2 mod 𝑃) gcd 𝑃)) |
96 | | nnnegz 12208 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → -2 ∈ ℤ) |
97 | 2, 96 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -2 ∈
ℤ) |
98 | | modgcd 16124 |
. . . . . . . . . . . . . . 15
⊢ ((-2
∈ ℤ ∧ 𝑃
∈ ℕ) → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃)) |
99 | 97, 22, 98 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃)) |
100 | | 2z 12238 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
101 | 22 | nnzd 12310 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
102 | | neggcd 16114 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℤ ∧ 𝑃
∈ ℤ) → (-2 gcd 𝑃) = (2 gcd 𝑃)) |
103 | 100, 101,
102 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (-2 gcd 𝑃) = (2 gcd 𝑃)) |
104 | | nnz 12228 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
105 | | oddm1d2 15953 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
107 | 106 | biimprd 251 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℕ → (((𝑃 − 1) / 2) ∈ ℤ
→ ¬ 2 ∥ 𝑃)) |
108 | | nnz 12228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 − 1) / 2) ∈ ℕ
→ ((𝑃 − 1) / 2)
∈ ℤ) |
109 | 107, 108 | impel 509 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ)
→ ¬ 2 ∥ 𝑃) |
110 | | isoddgcd1 16319 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ (2 gcd
𝑃) = 1)) |
111 | 104, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℕ → (¬ 2
∥ 𝑃 ↔ (2 gcd
𝑃) = 1)) |
112 | 111 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ)
→ (¬ 2 ∥ 𝑃
↔ (2 gcd 𝑃) =
1)) |
113 | 109, 112 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ)
→ (2 gcd 𝑃) =
1) |
114 | 113 | 3adant2 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℕ ∧ 1 <
𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (2
gcd 𝑃) =
1) |
115 | 21, 114 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 gcd 𝑃) = 1) |
116 | 103, 115 | eqtrd 2779 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (-2 gcd 𝑃) = 1) |
117 | 99, 116 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = 1) |
118 | 95, 117 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1) |
119 | 118 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1) |
120 | 79, 85, 119 | 3eqtr3d 2787 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1) |
121 | 56, 120 | jca 515 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)) |
122 | 121 | ex 416 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
123 | 122 | reximdva 3203 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 = 2) → (∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
124 | 123 | ex 416 |
. . . . . 6
⊢ (𝜑 → (𝑝 = 2 → (∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))) |
125 | 20, 124 | mpid 44 |
. . . . 5
⊢ (𝜑 → (𝑝 = 2 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
126 | 125 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 = 2 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
127 | 19, 126 | sylbid 243 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
128 | 127 | ralrimiva 3108 |
. 2
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
129 | 5, 6, 7, 13, 128 | pockthg 16491 |
1
⊢ (𝜑 → 𝑃 ∈ ℙ) |