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 mullidd ⊢ ( ( 𝐴 ∈ ℕ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 𝑁 ) )