Metamath Proof Explorer

Theorem modprminveq

Description: The modular inverse of A mod P is unique. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Hypothesis modprminv.1 
|- R = ( ( A ^ ( P - 2 ) ) mod P )
Assertion modprminveq 
|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ ( ( A x. S ) mod P ) = 1 ) <-> S = R ) )

Proof

Step Hyp Ref Expression
1 modprminv.1 
 |-  R = ( ( A ^ ( P - 2 ) ) mod P )
2 elfzelz 
 |-  ( S e. ( 0 ... ( P - 1 ) ) -> S e. ZZ )
3 zmulcl 
 |-  ( ( A e. ZZ /\ S e. ZZ ) -> ( A x. S ) e. ZZ )
4 2 3 sylan2 
 |-  ( ( A e. ZZ /\ S e. ( 0 ... ( P - 1 ) ) ) -> ( A x. S ) e. ZZ )
5 modprm1div 
 |-  ( ( P e. Prime /\ ( A x. S ) e. ZZ ) -> ( ( ( A x. S ) mod P ) = 1 <-> P || ( ( A x. S ) - 1 ) ) )
6 4 5 sylan2 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ S e. ( 0 ... ( P - 1 ) ) ) ) -> ( ( ( A x. S ) mod P ) = 1 <-> P || ( ( A x. S ) - 1 ) ) )
7 6 expr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( S e. ( 0 ... ( P - 1 ) ) -> ( ( ( A x. S ) mod P ) = 1 <-> P || ( ( A x. S ) - 1 ) ) ) )
8 7 3adant3 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( S e. ( 0 ... ( P - 1 ) ) -> ( ( ( A x. S ) mod P ) = 1 <-> P || ( ( A x. S ) - 1 ) ) ) )
9 8 pm5.32d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ ( ( A x. S ) mod P ) = 1 ) <-> ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) )
10 1 prmdiveq 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) <-> S = R ) )
11 9 10 bitrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ ( ( A x. S ) mod P ) = 1 ) <-> S = R ) )