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 e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) )

Proof

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