Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℙ) |
2 | | elfzoelz 10090 |
. . . . 5
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
3 | 2 | adantl 275 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ) |
4 | | prmnn 12051 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
5 | | prmz 12052 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
6 | | fzoval 10091 |
. . . . . . . 8
⊢ (𝑃 ∈ ℤ →
(1..^𝑃) = (1...(𝑃 − 1))) |
7 | 5, 6 | syl 14 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ →
(1..^𝑃) = (1...(𝑃 − 1))) |
8 | 7 | eleq2d 2240 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑁 ∈ (1..^𝑃) ↔ 𝑁 ∈ (1...(𝑃 − 1)))) |
9 | 8 | biimpa 294 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ (1...(𝑃 − 1))) |
10 | | fzm1ndvds 11803 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) |
11 | 4, 9, 10 | syl2an2r 590 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ¬ 𝑃 ∥ 𝑁) |
12 | | eqid 2170 |
. . . . . . 7
⊢ ((𝑁↑(𝑃 − 2)) mod 𝑃) = ((𝑁↑(𝑃 − 2)) mod 𝑃) |
13 | 12 | modprminv 12190 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
14 | 13 | simpld 111 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))) |
15 | 13 | simprd 113 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
16 | | 1eluzge0 9520 |
. . . . . . . . . . 11
⊢ 1 ∈
(ℤ≥‘0) |
17 | | fzss1 10006 |
. . . . . . . . . . 11
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑃 − 1)) ⊆ (0...(𝑃 − 1))) |
18 | 16, 17 | mp1i 10 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(1...(𝑃 − 1)) ⊆
(0...(𝑃 −
1))) |
19 | 18 | sseld 3146 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑠 ∈ (1...(𝑃 − 1)) → 𝑠 ∈ (0...(𝑃 − 1)))) |
20 | 19 | 3ad2ant1 1013 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (𝑠 ∈ (1...(𝑃 − 1)) → 𝑠 ∈ (0...(𝑃 − 1)))) |
21 | 20 | imdistani 443 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (1...(𝑃 − 1))) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (0...(𝑃 − 1)))) |
22 | 12 | modprminveq 12191 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1) ↔ 𝑠 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
23 | 22 | biimpa 294 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ (𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1)) → 𝑠 = ((𝑁↑(𝑃 − 2)) mod 𝑃)) |
24 | 23 | eqcomd 2176 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ (𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1)) → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠) |
25 | 24 | expr 373 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (0...(𝑃 − 1))) → (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
26 | 21, 25 | syl 14 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (1...(𝑃 − 1))) → (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
27 | 26 | ralrimiva 2543 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
28 | 14, 15, 27 | jca32 308 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) |
29 | 1, 3, 11, 28 | syl3anc 1233 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) |
30 | | oveq2 5858 |
. . . . . . 7
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (𝑁 · 𝑖) = (𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
31 | 30 | oveq1d 5865 |
. . . . . 6
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((𝑁 · 𝑖) mod 𝑃) = ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
32 | 31 | eqeq1d 2179 |
. . . . 5
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
33 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (𝑖 = 𝑠 ↔ ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
34 | 33 | imbi2d 229 |
. . . . . 6
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠) ↔ (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) |
35 | 34 | ralbidv 2470 |
. . . . 5
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠) ↔ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) |
36 | 32, 35 | anbi12d 470 |
. . . 4
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠)) ↔ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) |
37 | 36 | rspcev 2834 |
. . 3
⊢ ((((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) → ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) |
38 | 29, 37 | syl 14 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) |
39 | | oveq2 5858 |
. . . . 5
⊢ (𝑖 = 𝑠 → (𝑁 · 𝑖) = (𝑁 · 𝑠)) |
40 | 39 | oveq1d 5865 |
. . . 4
⊢ (𝑖 = 𝑠 → ((𝑁 · 𝑖) mod 𝑃) = ((𝑁 · 𝑠) mod 𝑃)) |
41 | 40 | eqeq1d 2179 |
. . 3
⊢ (𝑖 = 𝑠 → (((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ((𝑁 · 𝑠) mod 𝑃) = 1)) |
42 | 41 | reu8 2926 |
. 2
⊢
(∃!𝑖 ∈
(1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) |
43 | 38, 42 | sylibr 133 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑖 ∈ (1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1) |