Step | Hyp | Ref
| Expression |
1 | | pockthi.d |
. 2
⊢ 𝐷 ∈ ℕ |
2 | | pockthi.p |
. . . . . 6
⊢ 𝑃 ∈ ℙ |
3 | | prmnn 15767 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ 𝑃 ∈ ℕ |
5 | | pockthi.e |
. . . . . 6
⊢ 𝐸 ∈ ℕ |
6 | 5 | nnnn0i 11634 |
. . . . 5
⊢ 𝐸 ∈
ℕ0 |
7 | | nnexpcl 13174 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐸 ∈ ℕ0)
→ (𝑃↑𝐸) ∈
ℕ) |
8 | 4, 6, 7 | mp2an 683 |
. . . 4
⊢ (𝑃↑𝐸) ∈ ℕ |
9 | 8 | a1i 11 |
. . 3
⊢ (𝐷 ∈ ℕ → (𝑃↑𝐸) ∈ ℕ) |
10 | | id 22 |
. . 3
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℕ) |
11 | | pockthi.gt |
. . . 4
⊢ 𝐷 < (𝑃↑𝐸) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝐷 ∈ ℕ → 𝐷 < (𝑃↑𝐸)) |
13 | | pockthi.n |
. . . . 5
⊢ 𝑁 = (𝑀 + 1) |
14 | | pockthi.fac |
. . . . . . 7
⊢ 𝑀 = (𝐷 · (𝑃↑𝐸)) |
15 | 1 | nncni 11368 |
. . . . . . . 8
⊢ 𝐷 ∈ ℂ |
16 | 8 | nncni 11368 |
. . . . . . . 8
⊢ (𝑃↑𝐸) ∈ ℂ |
17 | 15, 16 | mulcomi 10372 |
. . . . . . 7
⊢ (𝐷 · (𝑃↑𝐸)) = ((𝑃↑𝐸) · 𝐷) |
18 | 14, 17 | eqtri 2849 |
. . . . . 6
⊢ 𝑀 = ((𝑃↑𝐸) · 𝐷) |
19 | 18 | oveq1i 6920 |
. . . . 5
⊢ (𝑀 + 1) = (((𝑃↑𝐸) · 𝐷) + 1) |
20 | 13, 19 | eqtri 2849 |
. . . 4
⊢ 𝑁 = (((𝑃↑𝐸) · 𝐷) + 1) |
21 | 20 | a1i 11 |
. . 3
⊢ (𝐷 ∈ ℕ → 𝑁 = (((𝑃↑𝐸) · 𝐷) + 1)) |
22 | | prmdvdsexpb 15806 |
. . . . . . 7
⊢ ((𝑥 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝐸 ∈ ℕ) → (𝑥 ∥ (𝑃↑𝐸) ↔ 𝑥 = 𝑃)) |
23 | 2, 5, 22 | mp3an23 1581 |
. . . . . 6
⊢ (𝑥 ∈ ℙ → (𝑥 ∥ (𝑃↑𝐸) ↔ 𝑥 = 𝑃)) |
24 | 13 | eqcomi 2834 |
. . . . . . . . . . 11
⊢ (𝑀 + 1) = 𝑁 |
25 | | pockthi.m |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = (𝐺 · 𝑃) |
26 | | pockthi.g |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 ∈ ℕ |
27 | 26, 4 | nnmulcli 11384 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 · 𝑃) ∈ ℕ |
28 | 25, 27 | eqeltri 2902 |
. . . . . . . . . . . . . . 15
⊢ 𝑀 ∈ ℕ |
29 | | peano2nn 11371 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℕ) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑀 + 1) ∈
ℕ |
31 | 13, 30 | eqeltri 2902 |
. . . . . . . . . . . . 13
⊢ 𝑁 ∈ ℕ |
32 | 31 | nncni 11368 |
. . . . . . . . . . . 12
⊢ 𝑁 ∈ ℂ |
33 | | ax-1cn 10317 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
34 | 28 | nncni 11368 |
. . . . . . . . . . . 12
⊢ 𝑀 ∈ ℂ |
35 | 32, 33, 34 | subadd2i 10697 |
. . . . . . . . . . 11
⊢ ((𝑁 − 1) = 𝑀 ↔ (𝑀 + 1) = 𝑁) |
36 | 24, 35 | mpbir 223 |
. . . . . . . . . 10
⊢ (𝑁 − 1) = 𝑀 |
37 | 36 | oveq2i 6921 |
. . . . . . . . 9
⊢ (𝐴↑(𝑁 − 1)) = (𝐴↑𝑀) |
38 | 37 | oveq1i 6920 |
. . . . . . . 8
⊢ ((𝐴↑(𝑁 − 1)) mod 𝑁) = ((𝐴↑𝑀) mod 𝑁) |
39 | | pockthi.mod |
. . . . . . . . 9
⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁) |
40 | 31 | nnrei 11367 |
. . . . . . . . . 10
⊢ 𝑁 ∈ ℝ |
41 | 28 | nngt0i 11397 |
. . . . . . . . . . . 12
⊢ 0 <
𝑀 |
42 | 28 | nnrei 11367 |
. . . . . . . . . . . . 13
⊢ 𝑀 ∈ ℝ |
43 | | 1re 10363 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
44 | | ltaddpos2 10850 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 1 ∈
ℝ) → (0 < 𝑀
↔ 1 < (𝑀 +
1))) |
45 | 42, 43, 44 | mp2an 683 |
. . . . . . . . . . . 12
⊢ (0 <
𝑀 ↔ 1 < (𝑀 + 1)) |
46 | 41, 45 | mpbi 222 |
. . . . . . . . . . 11
⊢ 1 <
(𝑀 + 1) |
47 | 46, 13 | breqtrri 4902 |
. . . . . . . . . 10
⊢ 1 <
𝑁 |
48 | | 1mod 13004 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) |
49 | 40, 47, 48 | mp2an 683 |
. . . . . . . . 9
⊢ (1 mod
𝑁) = 1 |
50 | 39, 49 | eqtri 2849 |
. . . . . . . 8
⊢ ((𝐴↑𝑀) mod 𝑁) = 1 |
51 | 38, 50 | eqtri 2849 |
. . . . . . 7
⊢ ((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 |
52 | | oveq2 6918 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑃 → ((𝑁 − 1) / 𝑥) = ((𝑁 − 1) / 𝑃)) |
53 | 26 | nncni 11368 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ∈ ℂ |
54 | 4 | nncni 11368 |
. . . . . . . . . . . . . . 15
⊢ 𝑃 ∈ ℂ |
55 | 53, 54 | mulcomi 10372 |
. . . . . . . . . . . . . 14
⊢ (𝐺 · 𝑃) = (𝑃 · 𝐺) |
56 | 36, 25, 55 | 3eqtrri 2854 |
. . . . . . . . . . . . 13
⊢ (𝑃 · 𝐺) = (𝑁 − 1) |
57 | 32, 33 | subcli 10685 |
. . . . . . . . . . . . . 14
⊢ (𝑁 − 1) ∈
ℂ |
58 | 4 | nnne0i 11398 |
. . . . . . . . . . . . . 14
⊢ 𝑃 ≠ 0 |
59 | 57, 54, 53, 58 | divmuli 11112 |
. . . . . . . . . . . . 13
⊢ (((𝑁 − 1) / 𝑃) = 𝐺 ↔ (𝑃 · 𝐺) = (𝑁 − 1)) |
60 | 56, 59 | mpbir 223 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) / 𝑃) = 𝐺 |
61 | 52, 60 | syl6eq 2877 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑃 → ((𝑁 − 1) / 𝑥) = 𝐺) |
62 | 61 | oveq2d 6926 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑃 → (𝐴↑((𝑁 − 1) / 𝑥)) = (𝐴↑𝐺)) |
63 | 62 | oveq1d 6925 |
. . . . . . . . 9
⊢ (𝑥 = 𝑃 → ((𝐴↑((𝑁 − 1) / 𝑥)) − 1) = ((𝐴↑𝐺) − 1)) |
64 | 63 | oveq1d 6925 |
. . . . . . . 8
⊢ (𝑥 = 𝑃 → (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = (((𝐴↑𝐺) − 1) gcd 𝑁)) |
65 | | pockthi.gcd |
. . . . . . . 8
⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1 |
66 | 64, 65 | syl6eq 2877 |
. . . . . . 7
⊢ (𝑥 = 𝑃 → (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1) |
67 | | pockthi.a |
. . . . . . . . 9
⊢ 𝐴 ∈ ℕ |
68 | 67 | nnzi 11736 |
. . . . . . . 8
⊢ 𝐴 ∈ ℤ |
69 | | oveq1 6917 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑦↑(𝑁 − 1)) = (𝐴↑(𝑁 − 1))) |
70 | 69 | oveq1d 6925 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝑦↑(𝑁 − 1)) mod 𝑁) = ((𝐴↑(𝑁 − 1)) mod 𝑁)) |
71 | 70 | eqeq1d 2827 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ↔ ((𝐴↑(𝑁 − 1)) mod 𝑁) = 1)) |
72 | | oveq1 6917 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑦↑((𝑁 − 1) / 𝑥)) = (𝐴↑((𝑁 − 1) / 𝑥))) |
73 | 72 | oveq1d 6925 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → ((𝑦↑((𝑁 − 1) / 𝑥)) − 1) = ((𝐴↑((𝑁 − 1) / 𝑥)) − 1)) |
74 | 73 | oveq1d 6925 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁)) |
75 | 74 | eqeq1d 2827 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → ((((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1 ↔ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) |
76 | 71, 75 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1) ↔ (((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1))) |
77 | 76 | rspcev 3526 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) |
78 | 68, 77 | mpan 681 |
. . . . . . 7
⊢ ((((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) |
79 | 51, 66, 78 | sylancr 581 |
. . . . . 6
⊢ (𝑥 = 𝑃 → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) |
80 | 23, 79 | syl6bi 245 |
. . . . 5
⊢ (𝑥 ∈ ℙ → (𝑥 ∥ (𝑃↑𝐸) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1))) |
81 | 80 | rgen 3131 |
. . . 4
⊢
∀𝑥 ∈
ℙ (𝑥 ∥ (𝑃↑𝐸) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) |
82 | 81 | a1i 11 |
. . 3
⊢ (𝐷 ∈ ℕ →
∀𝑥 ∈ ℙ
(𝑥 ∥ (𝑃↑𝐸) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1))) |
83 | 9, 10, 12, 21, 82 | pockthg 15988 |
. 2
⊢ (𝐷 ∈ ℕ → 𝑁 ∈
ℙ) |
84 | 1, 83 | ax-mp 5 |
1
⊢ 𝑁 ∈ ℙ |