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 A N N 0 A / L -N = if A < 0 1 1 A / L N

Proof

Step Hyp Ref Expression
1 iftrue A < 0 if A < 0 1 1 = 1
2 1 adantl A N N 0 A < 0 if A < 0 1 1 = 1
3 2 oveq1d A N N 0 A < 0 if A < 0 1 1 if N < 0 A < 0 1 1 = -1 if N < 0 A < 0 1 1
4 oveq2 if N < 0 1 1 = 1 -1 if N < 0 1 1 = -1 -1
5 neg1mulneg1e1 -1 -1 = 1
6 4 5 eqtrdi if N < 0 1 1 = 1 -1 if N < 0 1 1 = 1
7 oveq2 if N < 0 1 1 = 1 -1 if N < 0 1 1 = -1 1
8 ax-1cn 1
9 8 mulm1i -1 1 = 1
10 7 9 eqtrdi if N < 0 1 1 = 1 -1 if N < 0 1 1 = 1
11 6 10 ifsb -1 if N < 0 1 1 = if N < 0 1 1
12 simpr A N N 0 A < 0 A < 0
13 12 biantrud A N N 0 A < 0 N < 0 N < 0 A < 0
14 13 ifbid A N N 0 A < 0 if N < 0 1 1 = if N < 0 A < 0 1 1
15 14 oveq2d A N N 0 A < 0 -1 if N < 0 1 1 = -1 if N < 0 A < 0 1 1
16 simpl3 A N N 0 A < 0 N 0
17 16 necomd A N N 0 A < 0 0 N
18 simpl2 A N N 0 A < 0 N
19 18 zred A N N 0 A < 0 N
20 0re 0
21 ltlen N 0 N < 0 N 0 0 N
22 19 20 21 sylancl A N N 0 A < 0 N < 0 N 0 0 N
23 17 22 mpbiran2d A N N 0 A < 0 N < 0 N 0
24 19 le0neg1d A N N 0 A < 0 N 0 0 N
25 19 renegcld A N N 0 A < 0 N
26 lenlt 0 N 0 N ¬ N < 0
27 20 25 26 sylancr A N N 0 A < 0 0 N ¬ N < 0
28 23 24 27 3bitrd A N N 0 A < 0 N < 0 ¬ N < 0
29 28 ifbid A N N 0 A < 0 if N < 0 1 1 = if ¬ N < 0 1 1
30 ifnot if ¬ N < 0 1 1 = if N < 0 1 1
31 29 30 eqtrdi A N N 0 A < 0 if N < 0 1 1 = if N < 0 1 1
32 11 15 31 3eqtr3a A N N 0 A < 0 -1 if N < 0 A < 0 1 1 = if N < 0 1 1
33 12 biantrud A N N 0 A < 0 N < 0 N < 0 A < 0
34 33 ifbid A N N 0 A < 0 if N < 0 1 1 = if N < 0 A < 0 1 1
35 3 32 34 3eqtrd A N N 0 A < 0 if A < 0 1 1 if N < 0 A < 0 1 1 = if N < 0 A < 0 1 1
36 1t1e1 1 1 = 1
37 iffalse ¬ A < 0 if A < 0 1 1 = 1
38 37 adantl A N N 0 ¬ A < 0 if A < 0 1 1 = 1
39 simpr A N N 0 ¬ A < 0 ¬ A < 0
40 39 intnand A N N 0 ¬ A < 0 ¬ N < 0 A < 0
41 40 iffalsed A N N 0 ¬ A < 0 if N < 0 A < 0 1 1 = 1
42 38 41 oveq12d A N N 0 ¬ A < 0 if A < 0 1 1 if N < 0 A < 0 1 1 = 1 1
43 39 intnand A N N 0 ¬ A < 0 ¬ N < 0 A < 0
44 43 iffalsed A N N 0 ¬ A < 0 if N < 0 A < 0 1 1 = 1
45 36 42 44 3eqtr4a A N N 0 ¬ A < 0 if A < 0 1 1 if N < 0 A < 0 1 1 = if N < 0 A < 0 1 1
46 35 45 pm2.61dan A N N 0 if A < 0 1 1 if N < 0 A < 0 1 1 = if N < 0 A < 0 1 1
47 46 eqcomd A N N 0 if N < 0 A < 0 1 1 = if A < 0 1 1 if N < 0 A < 0 1 1
48 simpr A N N 0 n n
49 simpl2 A N N 0 n N
50 zq N N
51 49 50 syl A N N 0 n N
52 pcneg n N n pCnt -N = n pCnt N
53 48 51 52 syl2anc A N N 0 n n pCnt -N = n pCnt N
54 53 oveq2d A N N 0 n A / L n n pCnt -N = A / L n n pCnt N
55 54 ifeq1da A N N 0 if n A / L n n pCnt -N 1 = if n A / L n n pCnt N 1
56 55 mpteq2dv A N N 0 n if n A / L n n pCnt -N 1 = n if n A / L n n pCnt N 1
57 56 seqeq3d A N N 0 seq 1 × n if n A / L n n pCnt -N 1 = seq 1 × n if n A / L n n pCnt N 1
58 zcn N N
59 58 3ad2ant2 A N N 0 N
60 59 absnegd A N N 0 N = N
61 57 60 fveq12d A N N 0 seq 1 × n if n A / L n n pCnt -N 1 N = seq 1 × n if n A / L n n pCnt N 1 N
62 47 61 oveq12d A N N 0 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt -N 1 N = if A < 0 1 1 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt N 1 N
63 neg1cn 1
64 63 8 ifcli if A < 0 1 1
65 64 a1i A N N 0 if A < 0 1 1
66 63 8 ifcli if N < 0 A < 0 1 1
67 66 a1i A N N 0 if N < 0 A < 0 1 1
68 nnabscl N N 0 N
69 68 3adant1 A N N 0 N
70 nnuz = 1
71 69 70 eleqtrdi A N N 0 N 1
72 eqid n if n A / L n n pCnt N 1 = n if n A / L n n pCnt N 1
73 72 lgsfcl3 A N N 0 n if n A / L n n pCnt N 1 :
74 elfznn x 1 N x
75 ffvelrn n if n A / L n n pCnt N 1 : x n if n A / L n n pCnt N 1 x
76 73 74 75 syl2an A N N 0 x 1 N n if n A / L n n pCnt N 1 x
77 zmulcl x y x y
78 77 adantl A N N 0 x y x y
79 71 76 78 seqcl A N N 0 seq 1 × n if n A / L n n pCnt N 1 N
80 79 zcnd A N N 0 seq 1 × n if n A / L n n pCnt N 1 N
81 65 67 80 mulassd A N N 0 if A < 0 1 1 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt N 1 N = if A < 0 1 1 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt N 1 N
82 62 81 eqtrd A N N 0 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt -N 1 N = if A < 0 1 1 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt N 1 N
83 simp1 A N N 0 A
84 znegcl N N
85 84 3ad2ant2 A N N 0 N
86 simp3 A N N 0 N 0
87 59 86 negne0d A N N 0 N 0
88 eqid n if n A / L n n pCnt -N 1 = n if n A / L n n pCnt -N 1
89 88 lgsval4 A N N 0 A / L -N = if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt -N 1 N
90 83 85 87 89 syl3anc A N N 0 A / L -N = if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt -N 1 N
91 72 lgsval4 A N N 0 A / L N = if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt N 1 N
92 91 oveq2d A N N 0 if A < 0 1 1 A / L N = if A < 0 1 1 if N < 0 A < 0 1 1 seq 1 × n if n A / L n n pCnt N 1 N
93 82 90 92 3eqtr4d A N N 0 A / L -N = if A < 0 1 1 A / L N