Metamath Proof Explorer

Theorem lgsqr

Description: The Legendre symbol for odd primes is 1 iff the number is not a multiple of the prime (in which case it is 0 , see lgsne0 ) and the number is a quadratic residue mod P (it is -u 1 for nonresidues by the process of elimination from lgsabs1 ). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion lgsqr 
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 <-> ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) ) )

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 simpl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> A e. ZZ )
6 4 5 gcdcomd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( P gcd A ) = ( A gcd P ) )
7 6 eqeq1d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( P gcd A ) = 1 <-> ( A gcd P ) = 1 ) )
8 coprm 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
9 2 5 8 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
10 lgsne0 
 |-  ( ( A e. ZZ /\ P e. ZZ ) -> ( ( A /L P ) =/= 0 <-> ( A gcd P ) = 1 ) )
11 5 4 10 syl2anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) =/= 0 <-> ( A gcd P ) = 1 ) )
12 7 9 11 3bitr4d 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( -. P || A <-> ( A /L P ) =/= 0 ) )
13 12 necon4bbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( P || A <-> ( A /L P ) = 0 ) )
14 0ne1 
 |-  0 =/= 1
15 neeq1 
 |-  ( ( A /L P ) = 0 -> ( ( A /L P ) =/= 1 <-> 0 =/= 1 ) )
16 14 15 mpbiri 
 |-  ( ( A /L P ) = 0 -> ( A /L P ) =/= 1 )
17 13 16 biimtrdi 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( P || A -> ( A /L P ) =/= 1 ) )
18 17 necon2bd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> -. P || A ) )
19 lgsqrlem5 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A /L P ) = 1 ) -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )
20 19 3expia 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) )
21 18 20 jcad 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) ) )
22 simprl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> x e. ZZ )
23 22 zred 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> x e. RR )
24 absresq 
 |-  ( x e. RR -> ( ( abs ` x ) ^ 2 ) = ( x ^ 2 ) )
25 23 24 syl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( abs ` x ) ^ 2 ) = ( x ^ 2 ) )
26 25 oveq1d 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( ( abs ` x ) ^ 2 ) /L P ) = ( ( x ^ 2 ) /L P ) )
27 simplr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> -. P || A )
28 1 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> P e. Prime )
29 28 3 syl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> P e. ZZ )
30 zsqcl 
 |-  ( x e. ZZ -> ( x ^ 2 ) e. ZZ )
31 22 30 syl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( x ^ 2 ) e. ZZ )
32 simplll 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> A e. ZZ )
33 simprr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> P || ( ( x ^ 2 ) - A ) )
34 dvdssub2 
 |-  ( ( ( P e. ZZ /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) /\ P || ( ( x ^ 2 ) - A ) ) -> ( P || ( x ^ 2 ) <-> P || A ) )
35 29 31 32 33 34 syl31anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( P || ( x ^ 2 ) <-> P || A ) )
36 27 35 mtbird 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> -. P || ( x ^ 2 ) )
37 2nn 
 |-  2 e. NN
38 37 a1i 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> 2 e. NN )
39 prmdvdsexp 
 |-  ( ( P e. Prime /\ x e. ZZ /\ 2 e. NN ) -> ( P || ( x ^ 2 ) <-> P || x ) )
40 28 22 38 39 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( P || ( x ^ 2 ) <-> P || x ) )
41 36 40 mtbid 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> -. P || x )
42 dvds0 
 |-  ( P e. ZZ -> P || 0 )
43 29 42 syl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> P || 0 )
44 breq2 
 |-  ( x = 0 -> ( P || x <-> P || 0 ) )
45 43 44 syl5ibrcom 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( x = 0 -> P || x ) )
46 45 necon3bd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( -. P || x -> x =/= 0 ) )
47 41 46 mpd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> x =/= 0 )
48 nnabscl 
 |-  ( ( x e. ZZ /\ x =/= 0 ) -> ( abs ` x ) e. NN )
49 22 47 48 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( abs ` x ) e. NN )
50 49 nnzd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( abs ` x ) e. ZZ )
51 49 nnne0d 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( abs ` x ) =/= 0 )
52 50 29 gcdcomd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( abs ` x ) gcd P ) = ( P gcd ( abs ` x ) ) )
53 dvdsabsb 
 |-  ( ( P e. ZZ /\ x e. ZZ ) -> ( P || x <-> P || ( abs ` x ) ) )
54 29 22 53 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( P || x <-> P || ( abs ` x ) ) )
55 41 54 mtbid 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> -. P || ( abs ` x ) )
56 coprm 
 |-  ( ( P e. Prime /\ ( abs ` x ) e. ZZ ) -> ( -. P || ( abs ` x ) <-> ( P gcd ( abs ` x ) ) = 1 ) )
57 28 50 56 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( -. P || ( abs ` x ) <-> ( P gcd ( abs ` x ) ) = 1 ) )
58 55 57 mpbid 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( P gcd ( abs ` x ) ) = 1 )
59 52 58 eqtrd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( abs ` x ) gcd P ) = 1 )
60 lgssq 
 |-  ( ( ( ( abs ` x ) e. ZZ /\ ( abs ` x ) =/= 0 ) /\ P e. ZZ /\ ( ( abs ` x ) gcd P ) = 1 ) -> ( ( ( abs ` x ) ^ 2 ) /L P ) = 1 )
61 50 51 29 59 60 syl211anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( ( abs ` x ) ^ 2 ) /L P ) = 1 )
62 prmnn 
 |-  ( P e. Prime -> P e. NN )
63 28 62 syl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> P e. NN )
64 moddvds 
 |-  ( ( P e. NN /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) <-> P || ( ( x ^ 2 ) - A ) ) )
65 63 31 32 64 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) <-> P || ( ( x ^ 2 ) - A ) ) )
66 33 65 mpbird 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( x ^ 2 ) mod P ) = ( A mod P ) )
67 66 oveq1d 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( ( x ^ 2 ) mod P ) /L P ) = ( ( A mod P ) /L P ) )
68 eldifsni 
 |-  ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
69 68 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> P =/= 2 )
70 69 necomd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> 2 =/= P )
71 2z 
 |-  2 e. ZZ
72 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
73 71 72 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
74 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 2 || P <-> 2 = P ) )
75 74 necon3bbid 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( -. 2 || P <-> 2 =/= P ) )
76 73 28 75 sylancr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( -. 2 || P <-> 2 =/= P ) )
77 70 76 mpbird 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> -. 2 || P )
78 lgsmod 
 |-  ( ( ( x ^ 2 ) e. ZZ /\ P e. NN /\ -. 2 || P ) -> ( ( ( x ^ 2 ) mod P ) /L P ) = ( ( x ^ 2 ) /L P ) )
79 31 63 77 78 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( ( x ^ 2 ) mod P ) /L P ) = ( ( x ^ 2 ) /L P ) )
80 lgsmod 
 |-  ( ( A e. ZZ /\ P e. NN /\ -. 2 || P ) -> ( ( A mod P ) /L P ) = ( A /L P ) )
81 32 63 77 80 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( A mod P ) /L P ) = ( A /L P ) )
82 67 79 81 3eqtr3d 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( ( x ^ 2 ) /L P ) = ( A /L P ) )
83 26 61 82 3eqtr3rd 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) /\ ( x e. ZZ /\ P || ( ( x ^ 2 ) - A ) ) ) -> ( A /L P ) = 1 )
84 83 rexlimdvaa 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) -> ( E. x e. ZZ P || ( ( x ^ 2 ) - A ) -> ( A /L P ) = 1 ) )
85 84 expimpd 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) -> ( A /L P ) = 1 ) )
86 21 85 impbid 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 <-> ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) ) )