This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reumodprminv

Description: For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018)

Ref Expression
Assertion reumodprminv ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃! 𝑖 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → 𝑃 ∈ ℙ )
2 elfzoelz ⊢ ( 𝑁 ∈ ( 1 ..^ 𝑃 ) → 𝑁 ∈ ℤ )
3 2 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → 𝑁 ∈ ℤ )
4 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
5 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
6 fzoval ⊢ ( 𝑃 ∈ ℤ → ( 1 ..^ 𝑃 ) = ( 1 ... ( 𝑃 − 1 ) ) )
7 5 6 syl ⊢ ( 𝑃 ∈ ℙ → ( 1 ..^ 𝑃 ) = ( 1 ... ( 𝑃 − 1 ) ) )
8 7 eleq2d ⊢ ( 𝑃 ∈ ℙ → ( 𝑁 ∈ ( 1 ..^ 𝑃 ) ↔ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) )
9 8 biimpa ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
10 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑁 )
11 4 9 10 syl2an2r ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ¬ 𝑃 ∥ 𝑁 )
12 eqid ⊢ ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
13 12 modprminv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ( ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ) )
14 13 simpld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
15 13 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 )
16 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
17 fzss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 0 ... ( 𝑃 − 1 ) ) )
18 16 17 mp1i ⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 0 ... ( 𝑃 − 1 ) ) )
19 18 sseld ⊢ ( 𝑃 ∈ ℙ → ( 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ( 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
21 20 imdistani ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) ∧ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) ∧ 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
22 12 modprminveq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ( ( 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 ) ↔ 𝑠 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
23 22 biimpa ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) ∧ ( 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 ) ) → 𝑠 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
24 23 eqcomd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) ∧ ( 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 ) ) → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 )
25 24 expr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) ∧ 𝑠 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) → ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) )
26 21 25 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) ∧ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) )
27 26 ralrimiva ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) )
28 14 15 27 jca32 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑁 ) → ( ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ∧ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) ) ) )
29 1 3 11 28 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ∧ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) ) ) )
30 oveq2 ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( 𝑁 · 𝑖 ) = ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
31 30 oveq1d ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
32 31 eqeq1d ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 ↔ ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ) )
33 eqeq1 ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( 𝑖 = 𝑠 ↔ ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) )
34 33 imbi2d ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → 𝑖 = 𝑠 ) ↔ ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) ) )
35 34 ralbidv ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → 𝑖 = 𝑠 ) ↔ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) ) )
36 32 35 anbi12d ⊢ ( 𝑖 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 ∧ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → 𝑖 = 𝑠 ) ) ↔ ( ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ∧ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑠 ) ) ) )
37 36 rspcev ⊢ ( ( ( ( 𝑁 ↑ ( 𝑃 − 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 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑖 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 ∧ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → 𝑖 = 𝑠 ) ) )
39 oveq2 ⊢ ( 𝑖 = 𝑠 → ( 𝑁 · 𝑖 ) = ( 𝑁 · 𝑠 ) )
40 39 oveq1d ⊢ ( 𝑖 = 𝑠 → ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = ( ( 𝑁 · 𝑠 ) mod 𝑃 ) )
41 40 eqeq1d ⊢ ( 𝑖 = 𝑠 → ( ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 ↔ ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 ) )
42 41 reu8 ⊢ ( ∃! 𝑖 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 ↔ ∃ 𝑖 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 ∧ ∀ 𝑠 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( ( 𝑁 · 𝑠 ) mod 𝑃 ) = 1 → 𝑖 = 𝑠 ) ) )
43 38 42 sylibr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃! 𝑖 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑁 · 𝑖 ) mod 𝑃 ) = 1 )