Metamath Proof Explorer

Theorem prmdiv

Description: Show an explicit expression for the modular inverse of A mod P . (Contributed by Mario Carneiro, 24-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 prmdiv.1 
 |-  R = ( ( A ^ ( P - 2 ) ) mod P )
2 nprmdvds1 
 |-  ( P e. Prime -> -. P || 1 )
3 2 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> -. P || 1 )
4 prmz 
 |-  ( P e. Prime -> P e. ZZ )
5 4 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. ZZ )
6 simp2 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> A e. ZZ )
7 phiprm 
 |-  ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
8 7 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( phi ` P ) = ( P - 1 ) )
9 prmnn 
 |-  ( P e. Prime -> P e. NN )
10 9 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. NN )
11 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
12 10 11 syl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - 1 ) e. NN0 )
13 8 12 eqeltrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( phi ` P ) e. NN0 )
14 zexpcl 
 |-  ( ( A e. ZZ /\ ( phi ` P ) e. NN0 ) -> ( A ^ ( phi ` P ) ) e. ZZ )
15 6 13 14 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( phi ` P ) ) e. ZZ )
16 1z 
 |-  1 e. ZZ
17 zsubcl 
 |-  ( ( ( A ^ ( phi ` P ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( A ^ ( phi ` P ) ) - 1 ) e. ZZ )
18 15 16 17 sylancl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) - 1 ) e. ZZ )
19 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
20 19 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. ( ZZ>= ` 2 ) )
21 uznn0sub 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 2 ) e. NN0 )
22 20 21 syl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - 2 ) e. NN0 )
23 zexpcl 
 |-  ( ( A e. ZZ /\ ( P - 2 ) e. NN0 ) -> ( A ^ ( P - 2 ) ) e. ZZ )
24 6 22 23 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 2 ) ) e. ZZ )
25 24 zred 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 2 ) ) e. RR )
26 25 10 nndivred 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 2 ) ) / P ) e. RR )
27 26 flcld 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) e. ZZ )
28 6 27 zmulcld 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) e. ZZ )
29 5 28 zmulcld 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) e. ZZ )
30 6 5 gcdcomd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A gcd P ) = ( P gcd A ) )
31 coprm 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
32 31 biimp3a 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P gcd A ) = 1 )
33 30 32 eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A gcd P ) = 1 )
34 eulerth 
 |-  ( ( P e. NN /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
35 10 6 33 34 syl3anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
36 1zzd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> 1 e. ZZ )
37 moddvds 
 |-  ( ( P e. NN /\ ( A ^ ( phi ` P ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) <-> P || ( ( A ^ ( phi ` P ) ) - 1 ) ) )
38 10 15 36 37 syl3anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) <-> P || ( ( A ^ ( phi ` P ) ) - 1 ) ) )
39 35 38 mpbid 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P || ( ( A ^ ( phi ` P ) ) - 1 ) )
40 dvdsmul1 
 |-  ( ( P e. ZZ /\ ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) e. ZZ ) -> P || ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) )
41 5 28 40 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P || ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) )
42 5 18 29 39 41 dvds2subd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P || ( ( ( A ^ ( phi ` P ) ) - 1 ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
43 6 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> A e. CC )
44 24 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 2 ) ) e. CC )
45 5 27 zmulcld 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) e. ZZ )
46 45 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) e. CC )
47 43 44 46 subdid 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A x. ( ( A ^ ( P - 2 ) ) - ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) = ( ( A x. ( A ^ ( P - 2 ) ) ) - ( A x. ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
48 10 nnrpd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. RR+ )
49 modval 
 |-  ( ( ( A ^ ( P - 2 ) ) e. RR /\ P e. RR+ ) -> ( ( A ^ ( P - 2 ) ) mod P ) = ( ( A ^ ( P - 2 ) ) - ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) )
50 25 48 49 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 2 ) ) mod P ) = ( ( A ^ ( P - 2 ) ) - ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) )
51 1 50 eqtrid 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> R = ( ( A ^ ( P - 2 ) ) - ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) )
52 51 oveq2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A x. R ) = ( A x. ( ( A ^ ( P - 2 ) ) - ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
53 2m1e1 
 |-  ( 2 - 1 ) = 1
54 53 oveq2i 
 |-  ( P - ( 2 - 1 ) ) = ( P - 1 )
55 8 54 eqtr4di 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( phi ` P ) = ( P - ( 2 - 1 ) ) )
56 10 nncnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. CC )
57 2cnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> 2 e. CC )
58 1cnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> 1 e. CC )
59 56 57 58 subsubd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - ( 2 - 1 ) ) = ( ( P - 2 ) + 1 ) )
60 55 59 eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( phi ` P ) = ( ( P - 2 ) + 1 ) )
61 60 oveq2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( phi ` P ) ) = ( A ^ ( ( P - 2 ) + 1 ) ) )
62 43 22 expp1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( ( P - 2 ) + 1 ) ) = ( ( A ^ ( P - 2 ) ) x. A ) )
63 44 43 mulcomd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 2 ) ) x. A ) = ( A x. ( A ^ ( P - 2 ) ) ) )
64 61 62 63 3eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( phi ` P ) ) = ( A x. ( A ^ ( P - 2 ) ) ) )
65 27 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) e. CC )
66 56 43 65 mul12d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) = ( A x. ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) )
67 64 66 oveq12d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) = ( ( A x. ( A ^ ( P - 2 ) ) ) - ( A x. ( P x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
68 47 52 67 3eqtr4d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A x. R ) = ( ( A ^ ( phi ` P ) ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
69 68 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A x. R ) - 1 ) = ( ( ( A ^ ( phi ` P ) ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) - 1 ) )
70 15 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( phi ` P ) ) e. CC )
71 29 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) e. CC )
72 70 71 58 sub32d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( A ^ ( phi ` P ) ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) - 1 ) = ( ( ( A ^ ( phi ` P ) ) - 1 ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
73 69 72 eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A x. R ) - 1 ) = ( ( ( A ^ ( phi ` P ) ) - 1 ) - ( P x. ( A x. ( |_ ` ( ( A ^ ( P - 2 ) ) / P ) ) ) ) ) )
74 42 73 breqtrrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P || ( ( A x. R ) - 1 ) )
75 oveq2 
 |-  ( R = 0 -> ( A x. R ) = ( A x. 0 ) )
76 75 oveq1d 
 |-  ( R = 0 -> ( ( A x. R ) - 1 ) = ( ( A x. 0 ) - 1 ) )
77 76 breq2d 
 |-  ( R = 0 -> ( P || ( ( A x. R ) - 1 ) <-> P || ( ( A x. 0 ) - 1 ) ) )
78 74 77 syl5ibcom 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R = 0 -> P || ( ( A x. 0 ) - 1 ) ) )
79 43 mul01d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A x. 0 ) = 0 )
80 79 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A x. 0 ) - 1 ) = ( 0 - 1 ) )
81 df-neg 
 |-  -u 1 = ( 0 - 1 )
82 80 81 eqtr4di 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A x. 0 ) - 1 ) = -u 1 )
83 82 breq2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P || ( ( A x. 0 ) - 1 ) <-> P || -u 1 ) )
84 dvdsnegb 
 |-  ( ( P e. ZZ /\ 1 e. ZZ ) -> ( P || 1 <-> P || -u 1 ) )
85 5 16 84 sylancl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P || 1 <-> P || -u 1 ) )
86 83 85 bitr4d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P || ( ( A x. 0 ) - 1 ) <-> P || 1 ) )
87 78 86 sylibd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R = 0 -> P || 1 ) )
88 3 87 mtod 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> -. R = 0 )
89 zmodfz 
 |-  ( ( ( A ^ ( P - 2 ) ) e. ZZ /\ P e. NN ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. ( 0 ... ( P - 1 ) ) )
90 24 10 89 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. ( 0 ... ( P - 1 ) ) )
91 1 90 eqeltrid 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> R e. ( 0 ... ( P - 1 ) ) )
92 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
93 12 92 eleqtrdi 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
94 elfzp12 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( R e. ( 0 ... ( P - 1 ) ) <-> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) ) )
95 93 94 syl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R e. ( 0 ... ( P - 1 ) ) <-> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) ) )
96 91 95 mpbid 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) )
97 96 ord 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( -. R = 0 -> R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) )
98 88 97 mpd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> R e. ( ( 0 + 1 ) ... ( P - 1 ) ) )
99 1e0p1 
 |-  1 = ( 0 + 1 )
100 99 oveq1i 
 |-  ( 1 ... ( P - 1 ) ) = ( ( 0 + 1 ) ... ( P - 1 ) )
101 98 100 eleqtrrdi 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> R e. ( 1 ... ( P - 1 ) ) )
102 101 74 jca 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) )