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

Proof

Step Hyp Ref Expression
1 neg0 0 = 0
2 simpr A 0 N N = 0 N = 0
3 2 negeqd A 0 N N = 0 N = 0
4 1 3 2 3eqtr4a A 0 N N = 0 N = N
5 4 oveq2d A 0 N N = 0 A / L -N = A / L N
6 nn0z A 0 A
7 lgsneg A N N 0 A / L -N = if A < 0 1 1 A / L N
8 6 7 syl3an1 A 0 N N 0 A / L -N = if A < 0 1 1 A / L N
9 nn0nlt0 A 0 ¬ A < 0
10 9 3ad2ant1 A 0 N N 0 ¬ A < 0
11 10 iffalsed A 0 N N 0 if A < 0 1 1 = 1
12 11 oveq1d A 0 N N 0 if A < 0 1 1 A / L N = 1 A / L N
13 6 3ad2ant1 A 0 N N 0 A
14 simp2 A 0 N N 0 N
15 lgscl A N A / L N
16 13 14 15 syl2anc A 0 N N 0 A / L N
17 16 zcnd A 0 N N 0 A / L N
18 17 mulid2d A 0 N N 0 1 A / L N = A / L N
19 8 12 18 3eqtrd A 0 N N 0 A / L -N = A / L N
20 19 3expa A 0 N N 0 A / L -N = A / L N
21 5 20 pm2.61dane A 0 N A / L -N = A / L N