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