Metamath Proof Explorer

Theorem powm2modprm

Description: If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> P e. Prime )
2 simpr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> A e. ZZ )
3 2 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> A e. ZZ )
4 m1dvdsndvds 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A - 1 ) -> -. P || A ) )
5 4 imp 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> -. P || A )
6 eqid 
 |-  ( ( A ^ ( P - 2 ) ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P )
7 6 modprminv 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 ) )
8 simpr 
 |-  ( ( ( ( A ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 ) -> ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 )
9 8 eqcomd 
 |-  ( ( ( ( A ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 ) -> 1 = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
10 7 9 syl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> 1 = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
11 1 3 5 10 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> 1 = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
12 modprm1div 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 1 <-> P || ( A - 1 ) ) )
13 12 biimpar 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( A mod P ) = 1 )
14 13 oveq1d 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( A mod P ) x. ( ( A ^ ( P - 2 ) ) mod P ) ) = ( 1 x. ( ( A ^ ( P - 2 ) ) mod P ) ) )
15 14 oveq1d 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( ( A mod P ) x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( 1 x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
16 zre 
 |-  ( A e. ZZ -> A e. RR )
17 16 ad2antlr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> A e. RR )
18 prmm2nn0 
 |-  ( P e. Prime -> ( P - 2 ) e. NN0 )
19 18 anim1ci 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A e. ZZ /\ ( P - 2 ) e. NN0 ) )
20 19 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( A e. ZZ /\ ( P - 2 ) e. NN0 ) )
21 zexpcl 
 |-  ( ( A e. ZZ /\ ( P - 2 ) e. NN0 ) -> ( A ^ ( P - 2 ) ) e. ZZ )
22 20 21 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( A ^ ( P - 2 ) ) e. ZZ )
23 prmnn 
 |-  ( P e. Prime -> P e. NN )
24 23 adantr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> P e. NN )
25 24 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> P e. NN )
26 22 25 zmodcld 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. NN0 )
27 26 nn0zd 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. ZZ )
28 23 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
29 28 adantr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> P e. RR+ )
30 29 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> P e. RR+ )
31 modmulmod 
 |-  ( ( A e. RR /\ ( ( A ^ ( P - 2 ) ) mod P ) e. ZZ /\ P e. RR+ ) -> ( ( ( A mod P ) x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
32 17 27 30 31 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( ( A mod P ) x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
33 19 21 syl 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A ^ ( P - 2 ) ) e. ZZ )
34 33 24 zmodcld 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. NN0 )
35 34 nn0cnd 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. CC )
36 35 mullidd 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( 1 x. ( ( A ^ ( P - 2 ) ) mod P ) ) = ( ( A ^ ( P - 2 ) ) mod P ) )
37 36 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( 1 x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( ( A ^ ( P - 2 ) ) mod P ) mod P ) )
38 37 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( 1 x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( ( A ^ ( P - 2 ) ) mod P ) mod P ) )
39 reexpcl 
 |-  ( ( A e. RR /\ ( P - 2 ) e. NN0 ) -> ( A ^ ( P - 2 ) ) e. RR )
40 16 18 39 syl2anr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A ^ ( P - 2 ) ) e. RR )
41 40 29 jca 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ ( P - 2 ) ) e. RR /\ P e. RR+ ) )
42 41 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( A ^ ( P - 2 ) ) e. RR /\ P e. RR+ ) )
43 modabs2 
 |-  ( ( ( A ^ ( P - 2 ) ) e. RR /\ P e. RR+ ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P ) )
44 42 43 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P ) )
45 38 44 eqtrd 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( 1 x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P ) )
46 15 32 45 3eqtr3d 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P ) )
47 11 46 eqtr2d 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ P || ( A - 1 ) ) -> ( ( A ^ ( P - 2 ) ) mod P ) = 1 )
48 47 ex 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A - 1 ) -> ( ( A ^ ( P - 2 ) ) mod P ) = 1 ) )