Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℙ) |
2 | | elfzoelz 12470 |
. . . . 5
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) |
3 | 2 | adantl 482 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ) |
4 | | prmnn 15388 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ) |
6 | | prmz 15389 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
7 | | fzoval 12471 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℤ →
(1..^𝑃) = (1...(𝑃 − 1))) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ →
(1..^𝑃) = (1...(𝑃 − 1))) |
9 | 8 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (𝑁 ∈ (1..^𝑃) ↔ 𝑁 ∈ (1...(𝑃 − 1)))) |
10 | 9 | biimpa 501 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ (1...(𝑃 − 1))) |
11 | 5, 10 | jca 554 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1)))) |
12 | | fzm1ndvds 15044 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ¬ 𝑃 ∥ 𝑁) |
14 | | eqid 2622 |
. . . . . . 7
⊢ ((𝑁↑(𝑃 − 2)) mod 𝑃) = ((𝑁↑(𝑃 − 2)) mod 𝑃) |
15 | 14 | modprminv 15504 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
16 | 15 | simpld 475 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))) |
17 | 15 | simprd 479 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
18 | | 1eluzge0 11732 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℤ≥‘0) |
19 | | fzss1 12380 |
. . . . . . . . . . . 12
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑃 − 1)) ⊆ (0...(𝑃 − 1))) |
20 | 18, 19 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ →
(1...(𝑃 − 1)) ⊆
(0...(𝑃 −
1))) |
21 | 20 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (𝑠 ∈ (1...(𝑃 − 1)) → 𝑠 ∈ (0...(𝑃 − 1)))) |
22 | 21 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (𝑠 ∈ (1...(𝑃 − 1)) → 𝑠 ∈ (0...(𝑃 − 1)))) |
23 | 22 | imdistani 726 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (1...(𝑃 − 1))) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (0...(𝑃 − 1)))) |
24 | 14 | modprminveq 15505 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1) ↔ 𝑠 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
25 | 24 | biimpa 501 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ (𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1)) → 𝑠 = ((𝑁↑(𝑃 − 2)) mod 𝑃)) |
26 | 25 | eqcomd 2628 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ (𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1)) → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠) |
27 | 26 | expr 643 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (0...(𝑃 − 1))) → (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
28 | 23, 27 | syl 17 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (1...(𝑃 − 1))) → (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
29 | 28 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
30 | 17, 29 | jca 554 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) |
31 | 16, 30 | jca 554 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) |
32 | 1, 3, 13, 31 | syl3anc 1326 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) |
33 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (𝑁 · 𝑖) = (𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃))) |
34 | 33 | oveq1d 6665 |
. . . . . 6
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((𝑁 · 𝑖) mod 𝑃) = ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
35 | 34 | eqeq1d 2624 |
. . . . 5
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
36 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (𝑖 = 𝑠 ↔ ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) |
37 | 36 | imbi2d 330 |
. . . . . 6
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠) ↔ (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) |
38 | 37 | ralbidv 2986 |
. . . . 5
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠) ↔ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) |
39 | 35, 38 | anbi12d 747 |
. . . 4
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠)) ↔ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) |
40 | 39 | rspcev 3309 |
. . 3
⊢ ((((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) → ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) |
41 | 32, 40 | syl 17 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) |
42 | | oveq2 6658 |
. . . . 5
⊢ (𝑖 = 𝑠 → (𝑁 · 𝑖) = (𝑁 · 𝑠)) |
43 | 42 | oveq1d 6665 |
. . . 4
⊢ (𝑖 = 𝑠 → ((𝑁 · 𝑖) mod 𝑃) = ((𝑁 · 𝑠) mod 𝑃)) |
44 | 43 | eqeq1d 2624 |
. . 3
⊢ (𝑖 = 𝑠 → (((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ((𝑁 · 𝑠) mod 𝑃) = 1)) |
45 | 44 | reu8 3402 |
. 2
⊢
(∃!𝑖 ∈
(1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) |
46 | 41, 45 | sylibr 224 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑖 ∈ (1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1) |