Metamath Proof Explorer

Theorem lgslem1

Description: When a is coprime to the prime p , a ^ ( ( p - 1 ) / 2 ) is equivalent mod p to 1 or -u 1 , and so adding 1 makes it equivalent to 0 or 2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgslem1 
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
2 1 3ad2ant2 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P e. Prime )
3 prmnn 
 |-  ( P e. Prime -> P e. NN )
4 2 3 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P e. NN )
5 simp1 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> A e. ZZ )
6 prmz 
 |-  ( P e. Prime -> P e. ZZ )
7 2 6 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P e. ZZ )
8 5 7 gcdcomd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A gcd P ) = ( P gcd A ) )
9 simp3 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> -. P || A )
10 coprm 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
11 2 5 10 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
12 9 11 mpbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P gcd A ) = 1 )
13 8 12 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A gcd P ) = 1 )
14 eulerth 
 |-  ( ( P e. NN /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
15 4 5 13 14 syl3anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
16 phiprm 
 |-  ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
17 2 16 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( phi ` P ) = ( P - 1 ) )
18 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
19 4 18 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P - 1 ) e. NN0 )
20 17 19 eqeltrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( phi ` P ) e. NN0 )
21 zexpcl 
 |-  ( ( A e. ZZ /\ ( phi ` P ) e. NN0 ) -> ( A ^ ( phi ` P ) ) e. ZZ )
22 5 20 21 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A ^ ( phi ` P ) ) e. ZZ )
23 1zzd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 1 e. ZZ )
24 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 ) ) )
25 4 22 23 24 syl3anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) <-> P || ( ( A ^ ( phi ` P ) ) - 1 ) ) )
26 15 25 mpbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P || ( ( A ^ ( phi ` P ) ) - 1 ) )
27 19 nn0cnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P - 1 ) e. CC )
28 2cnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 e. CC )
29 2ne0 
 |-  2 =/= 0
30 29 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 =/= 0 )
31 27 28 30 divcan1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( P - 1 ) / 2 ) x. 2 ) = ( P - 1 ) )
32 17 31 eqtr4d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( phi ` P ) = ( ( ( P - 1 ) / 2 ) x. 2 ) )
33 32 oveq2d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A ^ ( phi ` P ) ) = ( A ^ ( ( ( P - 1 ) / 2 ) x. 2 ) ) )
34 5 zcnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> A e. CC )
35 2nn0 
 |-  2 e. NN0
36 35 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 e. NN0 )
37 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
38 37 3ad2ant2 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( P - 1 ) / 2 ) e. NN )
39 38 nnnn0d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( P - 1 ) / 2 ) e. NN0 )
40 34 36 39 expmuld 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A ^ ( ( ( P - 1 ) / 2 ) x. 2 ) ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) )
41 33 40 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A ^ ( phi ` P ) ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) )
42 41 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) - 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) - 1 ) )
43 sq1 
 |-  ( 1 ^ 2 ) = 1
44 43 oveq2i 
 |-  ( ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) - ( 1 ^ 2 ) ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) - 1 )
45 42 44 eqtr4di 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) - 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) - ( 1 ^ 2 ) ) )
46 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
47 5 39 46 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
48 47 zcnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. CC )
49 ax-1cn 
 |-  1 e. CC
50 subsq 
 |-  ( ( ( A ^ ( ( P - 1 ) / 2 ) ) e. CC /\ 1 e. CC ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) - ( 1 ^ 2 ) ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) x. ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
51 48 49 50 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) - ( 1 ^ 2 ) ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) x. ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
52 45 51 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) - 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) x. ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
53 26 52 breqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P || ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) x. ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
54 47 peano2zd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. ZZ )
55 peano2zm 
 |-  ( ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ -> ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) e. ZZ )
56 47 55 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) e. ZZ )
57 euclemma 
 |-  ( ( P e. Prime /\ ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. ZZ /\ ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) e. ZZ ) -> ( P || ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) x. ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) <-> ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) \/ P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) ) )
58 2 54 56 57 syl3anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P || ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) x. ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) <-> ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) \/ P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) ) )
59 53 58 mpbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) \/ P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
60 dvdsval3 
 |-  ( ( P e. NN /\ ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. ZZ ) -> ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) <-> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 ) )
61 4 54 60 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) <-> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 ) )
62 2z 
 |-  2 e. ZZ
63 62 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 e. ZZ )
64 moddvds 
 |-  ( ( P e. NN /\ ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. ZZ /\ 2 e. ZZ ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = ( 2 mod P ) <-> P || ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 2 ) ) )
65 4 54 63 64 syl3anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = ( 2 mod P ) <-> P || ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 2 ) ) )
66 2re 
 |-  2 e. RR
67 66 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 e. RR )
68 4 nnrpd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P e. RR+ )
69 0le2 
 |-  0 <_ 2
70 69 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 0 <_ 2 )
71 4 nnred 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P e. RR )
72 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
73 2 72 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P e. ( ZZ>= ` 2 ) )
74 eluzle 
 |-  ( P e. ( ZZ>= ` 2 ) -> 2 <_ P )
75 73 74 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 <_ P )
76 eldifsni 
 |-  ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
77 76 3ad2ant2 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> P =/= 2 )
78 67 71 75 77 leneltd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 2 < P )
79 modid 
 |-  ( ( ( 2 e. RR /\ P e. RR+ ) /\ ( 0 <_ 2 /\ 2 < P ) ) -> ( 2 mod P ) = 2 )
80 67 68 70 78 79 syl22anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( 2 mod P ) = 2 )
81 80 eqeq2d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = ( 2 mod P ) <-> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) )
82 df-2 
 |-  2 = ( 1 + 1 )
83 82 oveq2i 
 |-  ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 2 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - ( 1 + 1 ) )
84 49 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> 1 e. CC )
85 48 84 84 pnpcan2d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - ( 1 + 1 ) ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) )
86 83 85 eqtrid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 2 ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) )
87 86 breq2d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P || ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 2 ) <-> P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) )
88 65 81 87 3bitr3rd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) <-> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) )
89 61 88 orbi12d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( P || ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) \/ P || ( ( A ^ ( ( P - 1 ) / 2 ) ) - 1 ) ) <-> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 \/ ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) ) )
90 59 89 mpbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 \/ ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) )
91 ovex 
 |-  ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. _V
92 91 elpr 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } <-> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 \/ ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) )
93 90 92 sylibr 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } )