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 ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) → ( 𝐴 /L - 𝑁 ) = ( 𝐴 /L 𝑁 ) )

Proof

Step Hyp Ref Expression
1 neg0 - 0 = 0
2 simpr ( ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → 𝑁 = 0 )
3 2 negeqd ( ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → - 𝑁 = - 0 )
4 1 3 2 3eqtr4a ( ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → - 𝑁 = 𝑁 )
5 4 oveq2d ( ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝐴 /L - 𝑁 ) = ( 𝐴 /L 𝑁 ) )
6 nn0z ( 𝐴 ∈ ℕ0𝐴 ∈ ℤ )
7 lgsneg ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( 𝐴 /L 𝑁 ) ) )
8 6 7 syl3an1 ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( 𝐴 /L 𝑁 ) ) )
9 nn0nlt0 ( 𝐴 ∈ ℕ0 → ¬ 𝐴 < 0 )
10 9 3ad2ant1 ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ¬ 𝐴 < 0 )
11 10 iffalsed ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → if ( 𝐴 < 0 , - 1 , 1 ) = 1 )
12 11 oveq1d ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · ( 𝐴 /L 𝑁 ) ) = ( 1 · ( 𝐴 /L 𝑁 ) ) )
13 6 3ad2ant1 ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝐴 ∈ ℤ )
14 simp2 ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℤ )
15 lgscl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
16 13 14 15 syl2anc ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
17 16 zcnd ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) ∈ ℂ )
18 17 mulid2d ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 1 · ( 𝐴 /L 𝑁 ) ) = ( 𝐴 /L 𝑁 ) )
19 8 12 18 3eqtrd ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( 𝐴 /L 𝑁 ) )
20 19 3expa ( ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( 𝐴 /L 𝑁 ) )
21 5 20 pm2.61dane ( ( 𝐴 ∈ ℕ0𝑁 ∈ ℤ ) → ( 𝐴 /L - 𝑁 ) = ( 𝐴 /L 𝑁 ) )