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 sselid
 |-  ( ( 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 16 elfzelzd
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> R e. ZZ )
24 fzm1ndvds
 |-  ( ( P e. NN /\ R e. ( 1 ... ( P - 1 ) ) ) -> -. P || R )
25 9 16 24 syl2an2r
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> -. P || R )
26 eqid
 |-  ( ( R ^ ( P - 2 ) ) mod P ) = ( ( R ^ ( P - 2 ) ) mod P )
27 26 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 ) ) )
28 5 23 25 27 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 ) ) )
29 4 22 28 mpbi2and
 |-  ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A = ( ( R ^ ( P - 2 ) ) mod P ) )