Metamath Proof Explorer

Theorem prmdiveq

Description: The modular inverse of A mod P is unique. (Contributed by Mario Carneiro, 24-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 prmdiv.1 
 |-  R = ( ( A ^ ( P - 2 ) ) mod P )
2 simpl1 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P e. Prime )
3 prmz 
 |-  ( P e. Prime -> P e. ZZ )
4 2 3 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P e. ZZ )
5 simpl2 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> A e. ZZ )
6 elfzelz 
 |-  ( S e. ( 0 ... ( P - 1 ) ) -> S e. ZZ )
7 6 ad2antrl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S e. ZZ )
8 5 7 zmulcld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A x. S ) e. ZZ )
9 1z 
 |-  1 e. ZZ
10 zsubcl 
 |-  ( ( ( A x. S ) e. ZZ /\ 1 e. ZZ ) -> ( ( A x. S ) - 1 ) e. ZZ )
11 8 9 10 sylancl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( A x. S ) - 1 ) e. ZZ )
12 1 prmdiv 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) )
13 12 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) )
14 13 simpld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> R e. ( 1 ... ( P - 1 ) ) )
15 elfzelz 
 |-  ( R e. ( 1 ... ( P - 1 ) ) -> R e. ZZ )
16 14 15 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> R e. ZZ )
17 5 16 zmulcld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A x. R ) e. ZZ )
18 zsubcl 
 |-  ( ( ( A x. R ) e. ZZ /\ 1 e. ZZ ) -> ( ( A x. R ) - 1 ) e. ZZ )
19 17 9 18 sylancl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( A x. R ) - 1 ) e. ZZ )
20 simprr 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P || ( ( A x. S ) - 1 ) )
21 13 simprd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P || ( ( A x. R ) - 1 ) )
22 4 11 19 20 21 dvds2subd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P || ( ( ( A x. S ) - 1 ) - ( ( A x. R ) - 1 ) ) )
23 8 zcnd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A x. S ) e. CC )
24 17 zcnd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A x. R ) e. CC )
25 1cnd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> 1 e. CC )
26 23 24 25 nnncan2d 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( ( A x. S ) - 1 ) - ( ( A x. R ) - 1 ) ) = ( ( A x. S ) - ( A x. R ) ) )
27 5 zcnd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> A e. CC )
28 elfznn0 
 |-  ( S e. ( 0 ... ( P - 1 ) ) -> S e. NN0 )
29 28 ad2antrl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S e. NN0 )
30 29 nn0red 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S e. RR )
31 30 recnd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S e. CC )
32 16 zcnd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> R e. CC )
33 27 31 32 subdid 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A x. ( S - R ) ) = ( ( A x. S ) - ( A x. R ) ) )
34 26 33 eqtr4d 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( ( A x. S ) - 1 ) - ( ( A x. R ) - 1 ) ) = ( A x. ( S - R ) ) )
35 22 34 breqtrd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P || ( A x. ( S - R ) ) )
36 simpl3 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> -. P || A )
37 coprm 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
38 2 5 37 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
39 36 38 mpbid 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( P gcd A ) = 1 )
40 7 16 zsubcld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( S - R ) e. ZZ )
41 coprmdvds 
 |-  ( ( P e. ZZ /\ A e. ZZ /\ ( S - R ) e. ZZ ) -> ( ( P || ( A x. ( S - R ) ) /\ ( P gcd A ) = 1 ) -> P || ( S - R ) ) )
42 4 5 40 41 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( P || ( A x. ( S - R ) ) /\ ( P gcd A ) = 1 ) -> P || ( S - R ) ) )
43 35 39 42 mp2and 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P || ( S - R ) )
44 prmnn 
 |-  ( P e. Prime -> P e. NN )
45 2 44 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P e. NN )
46 moddvds 
 |-  ( ( P e. NN /\ S e. ZZ /\ R e. ZZ ) -> ( ( S mod P ) = ( R mod P ) <-> P || ( S - R ) ) )
47 45 7 16 46 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( S mod P ) = ( R mod P ) <-> P || ( S - R ) ) )
48 43 47 mpbird 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( S mod P ) = ( R mod P ) )
49 45 nnrpd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> P e. RR+ )
50 elfzle1 
 |-  ( S e. ( 0 ... ( P - 1 ) ) -> 0 <_ S )
51 50 ad2antrl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> 0 <_ S )
52 elfzle2 
 |-  ( S e. ( 0 ... ( P - 1 ) ) -> S <_ ( P - 1 ) )
53 52 ad2antrl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S <_ ( P - 1 ) )
54 zltlem1 
 |-  ( ( S e. ZZ /\ P e. ZZ ) -> ( S < P <-> S <_ ( P - 1 ) ) )
55 7 4 54 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( S < P <-> S <_ ( P - 1 ) ) )
56 53 55 mpbird 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S < P )
57 modid 
 |-  ( ( ( S e. RR /\ P e. RR+ ) /\ ( 0 <_ S /\ S < P ) ) -> ( S mod P ) = S )
58 30 49 51 56 57 syl22anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( S mod P ) = S )
59 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
60 uznn0sub 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 2 ) e. NN0 )
61 2 59 60 3syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( P - 2 ) e. NN0 )
62 zexpcl 
 |-  ( ( A e. ZZ /\ ( P - 2 ) e. NN0 ) -> ( A ^ ( P - 2 ) ) e. ZZ )
63 5 61 62 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A ^ ( P - 2 ) ) e. ZZ )
64 63 zred 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( A ^ ( P - 2 ) ) e. RR )
65 modabs2 
 |-  ( ( ( A ^ ( P - 2 ) ) e. RR /\ P e. RR+ ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P ) )
66 64 49 65 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P ) )
67 1 oveq1i 
 |-  ( R mod P ) = ( ( ( A ^ ( P - 2 ) ) mod P ) mod P )
68 66 67 1 3eqtr4g 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> ( R mod P ) = R )
69 48 58 68 3eqtr3d 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) /\ ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) -> S = R )
70 69 ex 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) -> S = R ) )
71 fz1ssfz0 
 |-  ( 1 ... ( P - 1 ) ) C_ ( 0 ... ( P - 1 ) )
72 71 sseli 
 |-  ( R e. ( 1 ... ( P - 1 ) ) -> R e. ( 0 ... ( P - 1 ) ) )
73 eleq1 
 |-  ( S = R -> ( S e. ( 0 ... ( P - 1 ) ) <-> R e. ( 0 ... ( P - 1 ) ) ) )
74 72 73 imbitrrid 
 |-  ( S = R -> ( R e. ( 1 ... ( P - 1 ) ) -> S e. ( 0 ... ( P - 1 ) ) ) )
75 oveq2 
 |-  ( S = R -> ( A x. S ) = ( A x. R ) )
76 75 oveq1d 
 |-  ( S = R -> ( ( A x. S ) - 1 ) = ( ( A x. R ) - 1 ) )
77 76 breq2d 
 |-  ( S = R -> ( P || ( ( A x. S ) - 1 ) <-> P || ( ( A x. R ) - 1 ) ) )
78 77 biimprd 
 |-  ( S = R -> ( P || ( ( A x. R ) - 1 ) -> P || ( ( A x. S ) - 1 ) ) )
79 74 78 anim12d 
 |-  ( S = R -> ( ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) -> ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) )
80 12 79 syl5com 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( S = R -> ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) ) )
81 70 80 impbid 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) <-> S = R ) )