Metamath Proof Explorer

Theorem lgsvalmod

Description: The Legendre symbol is equivalent to a ^ ( ( p - 1 ) / 2 ) , mod p . This theorem is also called "Euler's criterion", see theorem 9.2 in ApostolNT p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr . (Contributed by Mario Carneiro, 4-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
2 1 adantl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> P e. Prime )
3 prmz 
 |-  ( P e. Prime -> P e. ZZ )
4 2 3 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> P e. ZZ )
5 lgscl 
 |-  ( ( A e. ZZ /\ P e. ZZ ) -> ( A /L P ) e. ZZ )
6 4 5 syldan 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) e. ZZ )
7 6 zred 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) e. RR )
8 peano2re 
 |-  ( ( A /L P ) e. RR -> ( ( A /L P ) + 1 ) e. RR )
9 7 8 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) + 1 ) e. RR )
10 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
11 10 adantl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( P - 1 ) / 2 ) e. NN )
12 11 nnnn0d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( P - 1 ) / 2 ) e. NN0 )
13 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
14 12 13 syldan 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
15 14 zred 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. RR )
16 peano2re 
 |-  ( ( A ^ ( ( P - 1 ) / 2 ) ) e. RR -> ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. RR )
17 15 16 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. RR )
18 neg1rr 
 |-  -u 1 e. RR
19 18 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> -u 1 e. RR )
20 prmnn 
 |-  ( P e. Prime -> P e. NN )
21 2 20 syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> P e. NN )
22 21 nnrpd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> P e. RR+ )
23 17 22 modcld 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. RR )
24 23 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. CC )
25 ax-1cn 
 |-  1 e. CC
26 25 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> 1 e. CC )
27 lgsval3 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) )
28 24 26 27 mvrrsubd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) + 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
29 28 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) mod P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) mod P ) )
30 modabs2 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. RR /\ P e. RR+ ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) mod P ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
31 17 22 30 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) mod P ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
32 29 31 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) mod P ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
33 modadd1 
 |-  ( ( ( ( ( A /L P ) + 1 ) e. RR /\ ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. RR ) /\ ( -u 1 e. RR /\ P e. RR+ ) /\ ( ( ( A /L P ) + 1 ) mod P ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) ) -> ( ( ( ( A /L P ) + 1 ) + -u 1 ) mod P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) mod P ) )
34 9 17 19 22 32 33 syl221anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A /L P ) + 1 ) + -u 1 ) mod P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) mod P ) )
35 9 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) + 1 ) e. CC )
36 negsub 
 |-  ( ( ( ( A /L P ) + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( A /L P ) + 1 ) + -u 1 ) = ( ( ( A /L P ) + 1 ) - 1 ) )
37 35 25 36 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) + -u 1 ) = ( ( ( A /L P ) + 1 ) - 1 ) )
38 7 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) e. CC )
39 pncan 
 |-  ( ( ( A /L P ) e. CC /\ 1 e. CC ) -> ( ( ( A /L P ) + 1 ) - 1 ) = ( A /L P ) )
40 38 25 39 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) - 1 ) = ( A /L P ) )
41 37 40 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) + -u 1 ) = ( A /L P ) )
42 41 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A /L P ) + 1 ) + -u 1 ) mod P ) = ( ( A /L P ) mod P ) )
43 17 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. CC )
44 negsub 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) )
45 43 25 44 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) )
46 15 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. CC )
47 pncan 
 |-  ( ( ( A ^ ( ( P - 1 ) / 2 ) ) e. CC /\ 1 e. CC ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
48 46 25 47 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
49 45 48 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
50 49 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )
51 34 42 50 3eqtr3d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )