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 lgsval3 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) )
24 23 eqcomd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( A /L P ) )
25 17 22 modcld 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. RR )
26 25 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. CC )
27 ax-1cn 
 |-  1 e. CC
28 27 a1i 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> 1 e. CC )
29 7 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) e. CC )
30 26 28 29 subadd2d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( A /L P ) <-> ( ( A /L P ) + 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) ) )
31 24 30 mpbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) + 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
32 31 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) mod P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) mod P ) )
33 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 ) )
34 17 22 33 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) mod P ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
35 32 34 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) mod P ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) )
36 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 ) )
37 9 17 19 22 35 36 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 ) )
38 9 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) + 1 ) e. CC )
39 negsub 
 |-  ( ( ( ( A /L P ) + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( A /L P ) + 1 ) + -u 1 ) = ( ( ( A /L P ) + 1 ) - 1 ) )
40 38 27 39 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) + -u 1 ) = ( ( ( A /L P ) + 1 ) - 1 ) )
41 pncan 
 |-  ( ( ( A /L P ) e. CC /\ 1 e. CC ) -> ( ( ( A /L P ) + 1 ) - 1 ) = ( A /L P ) )
42 29 27 41 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) - 1 ) = ( A /L P ) )
43 40 42 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A /L P ) + 1 ) + -u 1 ) = ( A /L P ) )
44 43 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A /L P ) + 1 ) + -u 1 ) mod P ) = ( ( A /L P ) mod P ) )
45 17 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. CC )
46 negsub 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) )
47 45 27 46 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) = ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) )
48 15 recnd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A ^ ( ( P - 1 ) / 2 ) ) e. CC )
49 pncan 
 |-  ( ( ( A ^ ( ( P - 1 ) / 2 ) ) e. CC /\ 1 e. CC ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
50 48 27 49 sylancl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) - 1 ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
51 47 50 eqtrd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) = ( A ^ ( ( P - 1 ) / 2 ) ) )
52 51 oveq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) + -u 1 ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )
53 37 44 52 3eqtr3d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )