| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑃 ∈ ℙ) | 
| 2 |  | elfzoelz 13700 | . . . . 5
⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ) | 
| 3 | 2 | adantl 481 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ) | 
| 4 |  | prmnn 16712 | . . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 5 |  | prmz 16713 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 6 |  | fzoval 13701 | . . . . . . . 8
⊢ (𝑃 ∈ ℤ →
(1..^𝑃) = (1...(𝑃 − 1))) | 
| 7 | 5, 6 | syl 17 | . . . . . . 7
⊢ (𝑃 ∈ ℙ →
(1..^𝑃) = (1...(𝑃 − 1))) | 
| 8 | 7 | eleq2d 2826 | . . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑁 ∈ (1..^𝑃) ↔ 𝑁 ∈ (1...(𝑃 − 1)))) | 
| 9 | 8 | biimpa 476 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → 𝑁 ∈ (1...(𝑃 − 1))) | 
| 10 |  | fzm1ndvds 16360 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑁) | 
| 11 | 4, 9, 10 | syl2an2r 685 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ¬ 𝑃 ∥ 𝑁) | 
| 12 |  | eqid 2736 | . . . . . . 7
⊢ ((𝑁↑(𝑃 − 2)) mod 𝑃) = ((𝑁↑(𝑃 − 2)) mod 𝑃) | 
| 13 | 12 | modprminv 16838 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) | 
| 14 | 13 | simpld 494 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))) | 
| 15 | 13 | simprd 495 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) | 
| 16 |  | 1eluzge0 12935 | . . . . . . . . . . 11
⊢ 1 ∈
(ℤ≥‘0) | 
| 17 |  | fzss1 13604 | . . . . . . . . . . 11
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑃 − 1)) ⊆ (0...(𝑃 − 1))) | 
| 18 | 16, 17 | mp1i 13 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(1...(𝑃 − 1)) ⊆
(0...(𝑃 −
1))) | 
| 19 | 18 | sseld 3981 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑠 ∈ (1...(𝑃 − 1)) → 𝑠 ∈ (0...(𝑃 − 1)))) | 
| 20 | 19 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (𝑠 ∈ (1...(𝑃 − 1)) → 𝑠 ∈ (0...(𝑃 − 1)))) | 
| 21 | 20 | imdistani 568 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (1...(𝑃 − 1))) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (0...(𝑃 − 1)))) | 
| 22 | 12 | modprminveq 16839 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ((𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1) ↔ 𝑠 = ((𝑁↑(𝑃 − 2)) mod 𝑃))) | 
| 23 | 22 | biimpa 476 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ (𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1)) → 𝑠 = ((𝑁↑(𝑃 − 2)) mod 𝑃)) | 
| 24 | 23 | eqcomd 2742 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ (𝑠 ∈ (0...(𝑃 − 1)) ∧ ((𝑁 · 𝑠) mod 𝑃) = 1)) → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠) | 
| 25 | 24 | expr 456 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (0...(𝑃 − 1))) → (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) | 
| 26 | 21, 25 | syl 17 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) ∧ 𝑠 ∈ (1...(𝑃 − 1))) → (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) | 
| 27 | 26 | ralrimiva 3145 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) | 
| 28 | 14, 15, 27 | jca32 515 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑁) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) | 
| 29 | 1, 3, 11, 28 | syl3anc 1372 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (((𝑁↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) | 
| 30 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (𝑁 · 𝑖) = (𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃))) | 
| 31 | 30 | oveq1d 7447 | . . . . . 6
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((𝑁 · 𝑖) mod 𝑃) = ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) | 
| 32 | 31 | eqeq1d 2738 | . . . . 5
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) | 
| 33 |  | eqeq1 2740 | . . . . . . 7
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (𝑖 = 𝑠 ↔ ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)) | 
| 34 | 33 | imbi2d 340 | . . . . . 6
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠) ↔ (((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) | 
| 35 | 34 | ralbidv 3177 | . . . . 5
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → (∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠) ↔ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠))) | 
| 36 | 32, 35 | anbi12d 632 | . . . 4
⊢ (𝑖 = ((𝑁↑(𝑃 − 2)) mod 𝑃) → ((((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠)) ↔ (((𝑁 · ((𝑁↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → ((𝑁↑(𝑃 − 2)) mod 𝑃) = 𝑠)))) | 
| 37 | 36 | rspcev 3621 | . . 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 17 | . 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) | 
| 39 |  | oveq2 7440 | . . . . 5
⊢ (𝑖 = 𝑠 → (𝑁 · 𝑖) = (𝑁 · 𝑠)) | 
| 40 | 39 | oveq1d 7447 | . . . 4
⊢ (𝑖 = 𝑠 → ((𝑁 · 𝑖) mod 𝑃) = ((𝑁 · 𝑠) mod 𝑃)) | 
| 41 | 40 | eqeq1d 2738 | . . 3
⊢ (𝑖 = 𝑠 → (((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ((𝑁 · 𝑠) mod 𝑃) = 1)) | 
| 42 | 41 | reu8 3738 | . 2
⊢
(∃!𝑖 ∈
(1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1 ↔ ∃𝑖 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑖) mod 𝑃) = 1 ∧ ∀𝑠 ∈ (1...(𝑃 − 1))(((𝑁 · 𝑠) mod 𝑃) = 1 → 𝑖 = 𝑠))) | 
| 43 | 38, 42 | sylibr 234 | 1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑖 ∈ (1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1) |