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 ffvelrn
 |-  ( ( ( 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 ) ) )