| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pockthi.d | . 2
⊢ 𝐷 ∈ ℕ | 
| 2 |  | pockthi.p | . . . . . 6
⊢ 𝑃 ∈ ℙ | 
| 3 |  | prmnn 16712 | . . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 4 | 2, 3 | ax-mp 5 | . . . . 5
⊢ 𝑃 ∈ ℕ | 
| 5 |  | pockthi.e | . . . . . 6
⊢ 𝐸 ∈ ℕ | 
| 6 | 5 | nnnn0i 12536 | . . . . 5
⊢ 𝐸 ∈
ℕ0 | 
| 7 |  | nnexpcl 14116 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐸 ∈ ℕ0)
→ (𝑃↑𝐸) ∈
ℕ) | 
| 8 | 4, 6, 7 | mp2an 692 | . . . 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 12277 | . . . . . . . 8
⊢ 𝐷 ∈ ℂ | 
| 16 | 8 | nncni 12277 | . . . . . . . 8
⊢ (𝑃↑𝐸) ∈ ℂ | 
| 17 | 15, 16 | mulcomi 11270 | . . . . . . 7
⊢ (𝐷 · (𝑃↑𝐸)) = ((𝑃↑𝐸) · 𝐷) | 
| 18 | 14, 17 | eqtri 2764 | . . . . . 6
⊢ 𝑀 = ((𝑃↑𝐸) · 𝐷) | 
| 19 | 18 | oveq1i 7442 | . . . . 5
⊢ (𝑀 + 1) = (((𝑃↑𝐸) · 𝐷) + 1) | 
| 20 | 13, 19 | eqtri 2764 | . . . 4
⊢ 𝑁 = (((𝑃↑𝐸) · 𝐷) + 1) | 
| 21 | 20 | a1i 11 | . . 3
⊢ (𝐷 ∈ ℕ → 𝑁 = (((𝑃↑𝐸) · 𝐷) + 1)) | 
| 22 |  | prmdvdsexpb 16754 | . . . . . . 7
⊢ ((𝑥 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝐸 ∈ ℕ) → (𝑥 ∥ (𝑃↑𝐸) ↔ 𝑥 = 𝑃)) | 
| 23 | 2, 5, 22 | mp3an23 1454 | . . . . . 6
⊢ (𝑥 ∈ ℙ → (𝑥 ∥ (𝑃↑𝐸) ↔ 𝑥 = 𝑃)) | 
| 24 |  | pockthi.m | . . . . . . . . . . . . 13
⊢ 𝑀 = (𝐺 · 𝑃) | 
| 25 |  | pockthi.g | . . . . . . . . . . . . . 14
⊢ 𝐺 ∈ ℕ | 
| 26 | 25, 4 | nnmulcli 12292 | . . . . . . . . . . . . 13
⊢ (𝐺 · 𝑃) ∈ ℕ | 
| 27 | 24, 26 | eqeltri 2836 | . . . . . . . . . . . 12
⊢ 𝑀 ∈ ℕ | 
| 28 | 27 | nncni 12277 | . . . . . . . . . . 11
⊢ 𝑀 ∈ ℂ | 
| 29 |  | ax-1cn 11214 | . . . . . . . . . . 11
⊢ 1 ∈
ℂ | 
| 30 | 28, 29, 13 | mvrraddi 11526 | . . . . . . . . . 10
⊢ (𝑁 − 1) = 𝑀 | 
| 31 | 30 | oveq2i 7443 | . . . . . . . . 9
⊢ (𝐴↑(𝑁 − 1)) = (𝐴↑𝑀) | 
| 32 | 31 | oveq1i 7442 | . . . . . . . 8
⊢ ((𝐴↑(𝑁 − 1)) mod 𝑁) = ((𝐴↑𝑀) mod 𝑁) | 
| 33 |  | pockthi.mod | . . . . . . . . 9
⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁) | 
| 34 |  | peano2nn 12279 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℕ) | 
| 35 | 27, 34 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (𝑀 + 1) ∈
ℕ | 
| 36 | 13, 35 | eqeltri 2836 | . . . . . . . . . . 11
⊢ 𝑁 ∈ ℕ | 
| 37 | 36 | nnrei 12276 | . . . . . . . . . 10
⊢ 𝑁 ∈ ℝ | 
| 38 | 27 | nngt0i 12306 | . . . . . . . . . . . 12
⊢ 0 <
𝑀 | 
| 39 | 27 | nnrei 12276 | . . . . . . . . . . . . 13
⊢ 𝑀 ∈ ℝ | 
| 40 |  | 1re 11262 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ | 
| 41 |  | ltaddpos2 11755 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 1 ∈
ℝ) → (0 < 𝑀
↔ 1 < (𝑀 +
1))) | 
| 42 | 39, 40, 41 | mp2an 692 | . . . . . . . . . . . 12
⊢ (0 <
𝑀 ↔ 1 < (𝑀 + 1)) | 
| 43 | 38, 42 | mpbi 230 | . . . . . . . . . . 11
⊢ 1 <
(𝑀 + 1) | 
| 44 | 43, 13 | breqtrri 5169 | . . . . . . . . . 10
⊢ 1 <
𝑁 | 
| 45 |  | 1mod 13944 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) | 
| 46 | 37, 44, 45 | mp2an 692 | . . . . . . . . 9
⊢ (1 mod
𝑁) = 1 | 
| 47 | 33, 46 | eqtri 2764 | . . . . . . . 8
⊢ ((𝐴↑𝑀) mod 𝑁) = 1 | 
| 48 | 32, 47 | eqtri 2764 | . . . . . . 7
⊢ ((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 | 
| 49 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑃 → ((𝑁 − 1) / 𝑥) = ((𝑁 − 1) / 𝑃)) | 
| 50 | 25 | nncni 12277 | . . . . . . . . . . . . . . 15
⊢ 𝐺 ∈ ℂ | 
| 51 | 4 | nncni 12277 | . . . . . . . . . . . . . . 15
⊢ 𝑃 ∈ ℂ | 
| 52 | 50, 51 | mulcomi 11270 | . . . . . . . . . . . . . 14
⊢ (𝐺 · 𝑃) = (𝑃 · 𝐺) | 
| 53 | 30, 24, 52 | 3eqtrri 2769 | . . . . . . . . . . . . 13
⊢ (𝑃 · 𝐺) = (𝑁 − 1) | 
| 54 | 36 | nncni 12277 | . . . . . . . . . . . . . . 15
⊢ 𝑁 ∈ ℂ | 
| 55 | 54, 29 | subcli 11586 | . . . . . . . . . . . . . 14
⊢ (𝑁 − 1) ∈
ℂ | 
| 56 | 4 | nnne0i 12307 | . . . . . . . . . . . . . 14
⊢ 𝑃 ≠ 0 | 
| 57 | 55, 51, 50, 56 | divmuli 12022 | . . . . . . . . . . . . 13
⊢ (((𝑁 − 1) / 𝑃) = 𝐺 ↔ (𝑃 · 𝐺) = (𝑁 − 1)) | 
| 58 | 53, 57 | mpbir 231 | . . . . . . . . . . . 12
⊢ ((𝑁 − 1) / 𝑃) = 𝐺 | 
| 59 | 49, 58 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑃 → ((𝑁 − 1) / 𝑥) = 𝐺) | 
| 60 | 59 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑥 = 𝑃 → (𝐴↑((𝑁 − 1) / 𝑥)) = (𝐴↑𝐺)) | 
| 61 | 60 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑥 = 𝑃 → ((𝐴↑((𝑁 − 1) / 𝑥)) − 1) = ((𝐴↑𝐺) − 1)) | 
| 62 | 61 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑥 = 𝑃 → (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = (((𝐴↑𝐺) − 1) gcd 𝑁)) | 
| 63 |  | pockthi.gcd | . . . . . . . 8
⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1 | 
| 64 | 62, 63 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑥 = 𝑃 → (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1) | 
| 65 |  | pockthi.a | . . . . . . . . 9
⊢ 𝐴 ∈ ℕ | 
| 66 | 65 | nnzi 12643 | . . . . . . . 8
⊢ 𝐴 ∈ ℤ | 
| 67 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑦↑(𝑁 − 1)) = (𝐴↑(𝑁 − 1))) | 
| 68 | 67 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝑦↑(𝑁 − 1)) mod 𝑁) = ((𝐴↑(𝑁 − 1)) mod 𝑁)) | 
| 69 | 68 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ↔ ((𝐴↑(𝑁 − 1)) mod 𝑁) = 1)) | 
| 70 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑦↑((𝑁 − 1) / 𝑥)) = (𝐴↑((𝑁 − 1) / 𝑥))) | 
| 71 | 70 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → ((𝑦↑((𝑁 − 1) / 𝑥)) − 1) = ((𝐴↑((𝑁 − 1) / 𝑥)) − 1)) | 
| 72 | 71 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁)) | 
| 73 | 72 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑦 = 𝐴 → ((((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1 ↔ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) | 
| 74 | 69, 73 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1) ↔ (((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1))) | 
| 75 | 74 | rspcev 3621 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) | 
| 76 | 66, 75 | mpan 690 | . . . . . . 7
⊢ ((((𝐴↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝐴↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) | 
| 77 | 48, 64, 76 | sylancr 587 | . . . . . 6
⊢ (𝑥 = 𝑃 → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) | 
| 78 | 23, 77 | biimtrdi 253 | . . . . 5
⊢ (𝑥 ∈ ℙ → (𝑥 ∥ (𝑃↑𝐸) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1))) | 
| 79 | 78 | rgen 3062 | . . . 4
⊢
∀𝑥 ∈
ℙ (𝑥 ∥ (𝑃↑𝐸) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1)) | 
| 80 | 79 | a1i 11 | . . 3
⊢ (𝐷 ∈ ℕ →
∀𝑥 ∈ ℙ
(𝑥 ∥ (𝑃↑𝐸) → ∃𝑦 ∈ ℤ (((𝑦↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑦↑((𝑁 − 1) / 𝑥)) − 1) gcd 𝑁) = 1))) | 
| 81 | 9, 10, 12, 21, 80 | pockthg 16945 | . 2
⊢ (𝐷 ∈ ℕ → 𝑁 ∈
ℙ) | 
| 82 | 1, 81 | ax-mp 5 | 1
⊢ 𝑁 ∈ ℙ |