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 ) )