Metamath Proof Explorer

Theorem lgsneg1

Description: The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsneg1 
|- ( ( A e. NN0 /\ N e. ZZ ) -> ( A /L -u N ) = ( A /L N ) )

Proof

Step Hyp Ref Expression
1 neg0 
 |-  -u 0 = 0
2 simpr 
 |-  ( ( ( A e. NN0 /\ N e. ZZ ) /\ N = 0 ) -> N = 0 )
3 2 negeqd 
 |-  ( ( ( A e. NN0 /\ N e. ZZ ) /\ N = 0 ) -> -u N = -u 0 )
4 1 3 2 3eqtr4a 
 |-  ( ( ( A e. NN0 /\ N e. ZZ ) /\ N = 0 ) -> -u N = N )
5 4 oveq2d 
 |-  ( ( ( A e. NN0 /\ N e. ZZ ) /\ N = 0 ) -> ( A /L -u N ) = ( A /L N ) )
6 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
7 lgsneg 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) )
8 6 7 syl3an1 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) )
9 nn0nlt0 
 |-  ( A e. NN0 -> -. A < 0 )
10 9 3ad2ant1 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> -. A < 0 )
11 10 iffalsed 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> if ( A < 0 , -u 1 , 1 ) = 1 )
12 11 oveq1d 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) = ( 1 x. ( A /L N ) ) )
13 6 3ad2ant1 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> A e. ZZ )
14 simp2 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> N e. ZZ )
15 lgscl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
16 13 14 15 syl2anc 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> ( A /L N ) e. ZZ )
17 16 zcnd 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> ( A /L N ) e. CC )
18 17 mullidd 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> ( 1 x. ( A /L N ) ) = ( A /L N ) )
19 8 12 18 3eqtrd 
 |-  ( ( A e. NN0 /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( A /L N ) )
20 19 3expa 
 |-  ( ( ( A e. NN0 /\ N e. ZZ ) /\ N =/= 0 ) -> ( A /L -u N ) = ( A /L N ) )
21 5 20 pm2.61dane 
 |-  ( ( A e. NN0 /\ N e. ZZ ) -> ( A /L -u N ) = ( A /L N ) )