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 𝑁 ) )