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

Metamath Proof Explorer

Theorem modprminv

Description: Show an explicit expression for the modular inverse of A mod P . This is an application of prmdiv . (Contributed by Alexander van der Vekens, 15-May-2018)

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

Proof

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