Metamath Proof Explorer


Theorem lgsneg

Description: The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsneg ANN0A/L- N=ifA<011A/LN

Proof

Step Hyp Ref Expression
1 iftrue A<0ifA<011=1
2 1 adantl ANN0A<0ifA<011=1
3 2 oveq1d ANN0A<0ifA<011ifN<0A<011=-1ifN<0A<011
4 oveq2 ifN<011=1-1ifN<011=-1-1
5 neg1mulneg1e1 -1-1=1
6 4 5 eqtrdi ifN<011=1-1ifN<011=1
7 oveq2 ifN<011=1-1ifN<011=-11
8 ax-1cn 1
9 8 mulm1i -11=1
10 7 9 eqtrdi ifN<011=1-1ifN<011=1
11 6 10 ifsb -1ifN<011=ifN<011
12 simpr ANN0A<0A<0
13 12 biantrud ANN0A<0N<0N<0A<0
14 13 ifbid ANN0A<0ifN<011=ifN<0A<011
15 14 oveq2d ANN0A<0-1ifN<011=-1ifN<0A<011
16 simpl3 ANN0A<0N0
17 16 necomd ANN0A<00N
18 simpl2 ANN0A<0N
19 18 zred ANN0A<0N
20 0re 0
21 ltlen N0N<0N00N
22 19 20 21 sylancl ANN0A<0N<0N00N
23 17 22 mpbiran2d ANN0A<0N<0N0
24 19 le0neg1d ANN0A<0N00N
25 19 renegcld ANN0A<0N
26 lenlt 0N0N¬N<0
27 20 25 26 sylancr ANN0A<00N¬N<0
28 23 24 27 3bitrd ANN0A<0N<0¬N<0
29 28 ifbid ANN0A<0ifN<011=if¬N<011
30 ifnot if¬N<011=ifN<011
31 29 30 eqtrdi ANN0A<0ifN<011=ifN<011
32 11 15 31 3eqtr3a ANN0A<0-1ifN<0A<011=ifN<011
33 12 biantrud ANN0A<0N<0N<0A<0
34 33 ifbid ANN0A<0ifN<011=ifN<0A<011
35 3 32 34 3eqtrd ANN0A<0ifA<011ifN<0A<011=ifN<0A<011
36 1t1e1 11=1
37 iffalse ¬A<0ifA<011=1
38 37 adantl ANN0¬A<0ifA<011=1
39 simpr ANN0¬A<0¬A<0
40 39 intnand ANN0¬A<0¬N<0A<0
41 40 iffalsed ANN0¬A<0ifN<0A<011=1
42 38 41 oveq12d ANN0¬A<0ifA<011ifN<0A<011=11
43 39 intnand ANN0¬A<0¬N<0A<0
44 43 iffalsed ANN0¬A<0ifN<0A<011=1
45 36 42 44 3eqtr4a ANN0¬A<0ifA<011ifN<0A<011=ifN<0A<011
46 35 45 pm2.61dan ANN0ifA<011ifN<0A<011=ifN<0A<011
47 46 eqcomd ANN0ifN<0A<011=ifA<011ifN<0A<011
48 simpr ANN0nn
49 simpl2 ANN0nN
50 zq NN
51 49 50 syl ANN0nN
52 pcneg nNnpCnt- N=npCntN
53 48 51 52 syl2anc ANN0nnpCnt- N=npCntN
54 53 oveq2d ANN0nA/LnnpCnt- N=A/LnnpCntN
55 54 ifeq1da ANN0ifnA/LnnpCnt- N1=ifnA/LnnpCntN1
56 55 mpteq2dv ANN0nifnA/LnnpCnt- N1=nifnA/LnnpCntN1
57 56 seqeq3d ANN0seq1×nifnA/LnnpCnt- N1=seq1×nifnA/LnnpCntN1
58 zcn NN
59 58 3ad2ant2 ANN0N
60 59 absnegd ANN0N=N
61 57 60 fveq12d ANN0seq1×nifnA/LnnpCnt- N1N=seq1×nifnA/LnnpCntN1N
62 47 61 oveq12d ANN0ifN<0A<011seq1×nifnA/LnnpCnt- N1N=ifA<011ifN<0A<011seq1×nifnA/LnnpCntN1N
63 neg1cn 1
64 63 8 ifcli ifA<011
65 64 a1i ANN0ifA<011
66 63 8 ifcli ifN<0A<011
67 66 a1i ANN0ifN<0A<011
68 nnabscl NN0N
69 68 3adant1 ANN0N
70 nnuz =1
71 69 70 eleqtrdi ANN0N1
72 eqid nifnA/LnnpCntN1=nifnA/LnnpCntN1
73 72 lgsfcl3 ANN0nifnA/LnnpCntN1:
74 elfznn x1Nx
75 ffvelrn nifnA/LnnpCntN1:xnifnA/LnnpCntN1x
76 73 74 75 syl2an ANN0x1NnifnA/LnnpCntN1x
77 zmulcl xyxy
78 77 adantl ANN0xyxy
79 71 76 78 seqcl ANN0seq1×nifnA/LnnpCntN1N
80 79 zcnd ANN0seq1×nifnA/LnnpCntN1N
81 65 67 80 mulassd ANN0ifA<011ifN<0A<011seq1×nifnA/LnnpCntN1N=ifA<011ifN<0A<011seq1×nifnA/LnnpCntN1N
82 62 81 eqtrd ANN0ifN<0A<011seq1×nifnA/LnnpCnt- N1N=ifA<011ifN<0A<011seq1×nifnA/LnnpCntN1N
83 simp1 ANN0A
84 znegcl NN
85 84 3ad2ant2 ANN0N
86 simp3 ANN0N0
87 59 86 negne0d ANN0N0
88 eqid nifnA/LnnpCnt- N1=nifnA/LnnpCnt- N1
89 88 lgsval4 ANN0A/L- N=ifN<0A<011seq1×nifnA/LnnpCnt- N1N
90 83 85 87 89 syl3anc ANN0A/L- N=ifN<0A<011seq1×nifnA/LnnpCnt- N1N
91 72 lgsval4 ANN0A/LN=ifN<0A<011seq1×nifnA/LnnpCntN1N
92 91 oveq2d ANN0ifA<011A/LN=ifA<011ifN<0A<011seq1×nifnA/LnnpCntN1N
93 82 90 92 3eqtr4d ANN0A/L- N=ifA<011A/LN