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 
|- ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E! i e. ( 1 ... ( P - 1 ) ) ( ( N x. i ) mod P ) = 1 )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> P e. Prime )
2 elfzoelz 
 |-  ( N e. ( 1 ..^ P ) -> N e. ZZ )
3 2 adantl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> N e. ZZ )
4 prmnn 
 |-  ( P e. Prime -> P e. NN )
5 prmz 
 |-  ( P e. Prime -> P e. ZZ )
6 fzoval 
 |-  ( P e. ZZ -> ( 1 ..^ P ) = ( 1 ... ( P - 1 ) ) )
7 5 6 syl 
 |-  ( P e. Prime -> ( 1 ..^ P ) = ( 1 ... ( P - 1 ) ) )
8 7 eleq2d 
 |-  ( P e. Prime -> ( N e. ( 1 ..^ P ) <-> N e. ( 1 ... ( P - 1 ) ) ) )
9 8 biimpa 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> N e. ( 1 ... ( P - 1 ) ) )
10 fzm1ndvds 
 |-  ( ( P e. NN /\ N e. ( 1 ... ( P - 1 ) ) ) -> -. P || N )
11 4 9 10 syl2an2r 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> -. P || N )
12 eqid 
 |-  ( ( N ^ ( P - 2 ) ) mod P ) = ( ( N ^ ( P - 2 ) ) mod P )
13 12 modprminv 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( ( ( N ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 ) )
14 13 simpld 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( ( N ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) )
15 13 simprd 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 )
16 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
17 fzss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... ( P - 1 ) ) C_ ( 0 ... ( P - 1 ) ) )
18 16 17 mp1i 
 |-  ( P e. Prime -> ( 1 ... ( P - 1 ) ) C_ ( 0 ... ( P - 1 ) ) )
19 18 sseld 
 |-  ( P e. Prime -> ( s e. ( 1 ... ( P - 1 ) ) -> s e. ( 0 ... ( P - 1 ) ) ) )
20 19 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( s e. ( 1 ... ( P - 1 ) ) -> s e. ( 0 ... ( P - 1 ) ) ) )
21 20 imdistani 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) /\ s e. ( 1 ... ( P - 1 ) ) ) -> ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) /\ s e. ( 0 ... ( P - 1 ) ) ) )
22 12 modprminveq 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( ( s e. ( 0 ... ( P - 1 ) ) /\ ( ( N x. s ) mod P ) = 1 ) <-> s = ( ( N ^ ( P - 2 ) ) mod P ) ) )
23 22 biimpa 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) /\ ( s e. ( 0 ... ( P - 1 ) ) /\ ( ( N x. s ) mod P ) = 1 ) ) -> s = ( ( N ^ ( P - 2 ) ) mod P ) )
24 23 eqcomd 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) /\ ( s e. ( 0 ... ( P - 1 ) ) /\ ( ( N x. s ) mod P ) = 1 ) ) -> ( ( N ^ ( P - 2 ) ) mod P ) = s )
25 24 expr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) /\ s e. ( 0 ... ( P - 1 ) ) ) -> ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) )
26 21 25 syl 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) /\ s e. ( 1 ... ( P - 1 ) ) ) -> ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) )
27 26 ralrimiva 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) )
28 14 15 27 jca32 
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( ( ( N ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) ) ) )
29 1 3 11 28 syl3anc 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( ( N ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) ) ) )
30 oveq2 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( N x. i ) = ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) )
31 30 oveq1d 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( ( N x. i ) mod P ) = ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) )
32 31 eqeq1d 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( ( ( N x. i ) mod P ) = 1 <-> ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 ) )
33 eqeq1 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( i = s <-> ( ( N ^ ( P - 2 ) ) mod P ) = s ) )
34 33 imbi2d 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( ( ( ( N x. s ) mod P ) = 1 -> i = s ) <-> ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) ) )
35 34 ralbidv 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> i = s ) <-> A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) ) )
36 32 35 anbi12d 
 |-  ( i = ( ( N ^ ( P - 2 ) ) mod P ) -> ( ( ( ( N x. i ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> i = s ) ) <-> ( ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) ) ) )
37 36 rspcev 
 |-  ( ( ( ( N ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( ( N x. ( ( N ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> ( ( N ^ ( P - 2 ) ) mod P ) = s ) ) ) -> E. i e. ( 1 ... ( P - 1 ) ) ( ( ( N x. i ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> i = s ) ) )
38 29 37 syl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. i e. ( 1 ... ( P - 1 ) ) ( ( ( N x. i ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> i = s ) ) )
39 oveq2 
 |-  ( i = s -> ( N x. i ) = ( N x. s ) )
40 39 oveq1d 
 |-  ( i = s -> ( ( N x. i ) mod P ) = ( ( N x. s ) mod P ) )
41 40 eqeq1d 
 |-  ( i = s -> ( ( ( N x. i ) mod P ) = 1 <-> ( ( N x. s ) mod P ) = 1 ) )
42 41 reu8 
 |-  ( E! i e. ( 1 ... ( P - 1 ) ) ( ( N x. i ) mod P ) = 1 <-> E. i e. ( 1 ... ( P - 1 ) ) ( ( ( N x. i ) mod P ) = 1 /\ A. s e. ( 1 ... ( P - 1 ) ) ( ( ( N x. s ) mod P ) = 1 -> i = s ) ) )
43 38 42 sylibr 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E! i e. ( 1 ... ( P - 1 ) ) ( ( N x. i ) mod P ) = 1 )