Step | Hyp | Ref
| Expression |
1 | | prmuz2 15246 |
. . 3
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
(ℤ≥‘2)) |
2 | | eqid 2610 |
. . . 4
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
3 | | eleq2 2677 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑁 − 1) ∈ 𝑧 ↔ (𝑁 − 1) ∈ 𝑥)) |
4 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (𝑛↑(𝑁 − 2)) = (𝑦↑(𝑁 − 2))) |
5 | 4 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑛 = 𝑦 → ((𝑛↑(𝑁 − 2)) mod 𝑁) = ((𝑦↑(𝑁 − 2)) mod 𝑁)) |
6 | 5 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑛 = 𝑦 → (((𝑛↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧 ↔ ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧)) |
7 | 6 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝑧 ((𝑛↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑧 ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧) |
8 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧 ↔ ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑥)) |
9 | 8 | raleqbi1dv 3123 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ 𝑧 ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑥)) |
10 | 7, 9 | syl5bb 271 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (∀𝑛 ∈ 𝑧 ((𝑛↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑥)) |
11 | 3, 10 | anbi12d 743 |
. . . . 5
⊢ (𝑧 = 𝑥 → (((𝑁 − 1) ∈ 𝑧 ∧ ∀𝑛 ∈ 𝑧 ((𝑛↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧) ↔ ((𝑁 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑥))) |
12 | 11 | cbvrabv 3172 |
. . . 4
⊢ {𝑧 ∈ 𝒫 (1...(𝑁 − 1)) ∣ ((𝑁 − 1) ∈ 𝑧 ∧ ∀𝑛 ∈ 𝑧 ((𝑛↑(𝑁 − 2)) mod 𝑁) ∈ 𝑧)} = {𝑥 ∈ 𝒫 (1...(𝑁 − 1)) ∣ ((𝑁 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑁 − 2)) mod 𝑁) ∈ 𝑥)} |
13 | 2, 12 | wilthlem3 24596 |
. . 3
⊢ (𝑁 ∈ ℙ → 𝑁 ∥ ((!‘(𝑁 − 1)) +
1)) |
14 | 1, 13 | jca 553 |
. 2
⊢ (𝑁 ∈ ℙ → (𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1))) |
15 | | simpl 472 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) → 𝑁 ∈
(ℤ≥‘2)) |
16 | | elfzuz 12209 |
. . . . . . . . 9
⊢ (𝑛 ∈ (2...(𝑁 − 1)) → 𝑛 ∈
(ℤ≥‘2)) |
17 | 16 | adantl 481 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑛 ∈
(ℤ≥‘2)) |
18 | | eluz2nn 11602 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘2) → 𝑛 ∈ ℕ) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑛 ∈ ℕ) |
20 | | elfzuz3 12210 |
. . . . . . . 8
⊢ (𝑛 ∈ (2...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
22 | | dvdsfac 14886 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑛)) → 𝑛 ∥ (!‘(𝑁 − 1))) |
23 | 19, 21, 22 | syl2anc 691 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑛 ∥ (!‘(𝑁 − 1))) |
24 | | eluz2nn 11602 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
25 | 24 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
26 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
27 | | faccl 12932 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈
ℕ0 → (!‘(𝑁 − 1)) ∈
ℕ) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → (!‘(𝑁 − 1)) ∈
ℕ) |
29 | 28 | nnzd 11357 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → (!‘(𝑁 − 1)) ∈
ℤ) |
30 | | eluz2b2 11637 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘2) ↔ (𝑛 ∈ ℕ ∧ 1 < 𝑛)) |
31 | 30 | simprbi 479 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘2) → 1 < 𝑛) |
32 | 17, 31 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 1 < 𝑛) |
33 | | ndvdsp1 14973 |
. . . . . . 7
⊢
(((!‘(𝑁
− 1)) ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 1 < 𝑛) → (𝑛 ∥ (!‘(𝑁 − 1)) → ¬ 𝑛 ∥ ((!‘(𝑁 − 1)) + 1))) |
34 | 29, 19, 32, 33 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → (𝑛 ∥ (!‘(𝑁 − 1)) → ¬ 𝑛 ∥ ((!‘(𝑁 − 1)) + 1))) |
35 | 23, 34 | mpd 15 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → ¬ 𝑛 ∥ ((!‘(𝑁 − 1)) +
1)) |
36 | | simplr 788 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) |
37 | 19 | nnzd 11357 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑛 ∈ ℤ) |
38 | 25 | nnzd 11357 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
39 | 29 | peano2zd 11361 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → ((!‘(𝑁 − 1)) + 1) ∈
ℤ) |
40 | | dvdstr 14856 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧
((!‘(𝑁 − 1)) +
1) ∈ ℤ) → ((𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) → 𝑛 ∥ ((!‘(𝑁 − 1)) + 1))) |
41 | 37, 38, 39, 40 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → ((𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) → 𝑛 ∥ ((!‘(𝑁 − 1)) + 1))) |
42 | 36, 41 | mpan2d 706 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → (𝑛 ∥ 𝑁 → 𝑛 ∥ ((!‘(𝑁 − 1)) + 1))) |
43 | 35, 42 | mtod 188 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) ∧ 𝑛 ∈ (2...(𝑁 − 1))) → ¬ 𝑛 ∥ 𝑁) |
44 | 43 | ralrimiva 2949 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) → ∀𝑛 ∈ (2...(𝑁 − 1)) ¬ 𝑛 ∥ 𝑁) |
45 | | isprm3 15234 |
. . 3
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈
(ℤ≥‘2) ∧ ∀𝑛 ∈ (2...(𝑁 − 1)) ¬ 𝑛 ∥ 𝑁)) |
46 | 15, 44, 45 | sylanbrc 695 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)) → 𝑁 ∈ ℙ) |
47 | 14, 46 | impbii 198 |
1
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1))) |