Metamath Proof Explorer

Theorem prmdivdiv

Description: The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 prmdiv.1 
 |-  R = ( ( A ^ ( P - 2 ) ) mod P )
2 fz1ssfz0 
 |-  ( 1 ... ( P - 1 ) ) C_ ( 0 ... ( P - 1 ) )
3 simpr 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A e. ( 1 ... ( P - 1 ) ) )
4 2 3 sseldi 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A e. ( 0 ... ( P - 1 ) ) )
5 simpl 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> P e. Prime )
6 elfznn 
 |-  ( A e. ( 1 ... ( P - 1 ) ) -> A e. NN )
7 6 adantl 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A e. NN )
8 7 nnzd 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A e. ZZ )
9 prmnn 
 |-  ( P e. Prime -> P e. NN )
10 fzm1ndvds 
 |-  ( ( P e. NN /\ A e. ( 1 ... ( P - 1 ) ) ) -> -. P || A )
11 9 10 sylan 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> -. P || A )
12 1 prmdiv 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) )
13 5 8 11 12 syl3anc 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) )
14 13 simprd 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> P || ( ( A x. R ) - 1 ) )
15 7 nncnd 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A e. CC )
16 13 simpld 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> R e. ( 1 ... ( P - 1 ) ) )
17 elfznn 
 |-  ( R e. ( 1 ... ( P - 1 ) ) -> R e. NN )
18 16 17 syl 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> R e. NN )
19 18 nncnd 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> R e. CC )
20 15 19 mulcomd 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> ( A x. R ) = ( R x. A ) )
21 20 oveq1d 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> ( ( A x. R ) - 1 ) = ( ( R x. A ) - 1 ) )
22 14 21 breqtrd 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> P || ( ( R x. A ) - 1 ) )
23 elfzelz 
 |-  ( R e. ( 1 ... ( P - 1 ) ) -> R e. ZZ )
24 16 23 syl 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> R e. ZZ )
25 fzm1ndvds 
 |-  ( ( P e. NN /\ R e. ( 1 ... ( P - 1 ) ) ) -> -. P || R )
26 9 16 25 syl2an2r 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> -. P || R )
27 eqid 
 |-  ( ( R ^ ( P - 2 ) ) mod P ) = ( ( R ^ ( P - 2 ) ) mod P )
28 27 prmdiveq 
 |-  ( ( P e. Prime /\ R e. ZZ /\ -. P || R ) -> ( ( A e. ( 0 ... ( P - 1 ) ) /\ P || ( ( R x. A ) - 1 ) ) <-> A = ( ( R ^ ( P - 2 ) ) mod P ) ) )
29 5 24 26 28 syl3anc 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> ( ( A e. ( 0 ... ( P - 1 ) ) /\ P || ( ( R x. A ) - 1 ) ) <-> A = ( ( R ^ ( P - 2 ) ) mod P ) ) )
30 4 22 29 mpbi2and 
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A = ( ( R ^ ( P - 2 ) ) mod P ) )