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