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 \in ℕ_{0} \land N \in ℤ) \to A /_{L} -N = A /_{L} N$

Proof

Step	Hyp	Ref	Expression
1		neg0	$⊢ - 0 = 0$
2		simpr	$⊢ ((A \in ℕ_{0} \land N \in ℤ) \land N = 0) \to N = 0$
3	2	negeqd	$⊢ ((A \in ℕ_{0} \land N \in ℤ) \land N = 0) \to - N = - 0$
4	1 3 2	3eqtr4a	$⊢ ((A \in ℕ_{0} \land N \in ℤ) \land N = 0) \to - N = N$
5	4	oveq2d	$⊢ ((A \in ℕ_{0} \land N \in ℤ) \land N = 0) \to A /_{L} -N = A /_{L} N$
6		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
7		lgsneg	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} -N = if (A < 0, - 1, 1) (A /_{L} N)$
8	6 7	syl3an1	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to A /_{L} -N = if (A < 0, - 1, 1) (A /_{L} N)$
9		nn0nlt0	$⊢ A \in ℕ_{0} \to \neg A < 0$
10	9	3ad2ant1	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to \neg A < 0$
11	10	iffalsed	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to if (A < 0, - 1, 1) = 1$
12	11	oveq1d	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to if (A < 0, - 1, 1) (A /_{L} N) = 1 (A /_{L} N)$
13	6	3ad2ant1	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to A \in ℤ$
14		simp2	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to N \in ℤ$
15		lgscl	$⊢ (A \in ℤ \land N \in ℤ) \to A /_{L} N \in ℤ$
16	13 14 15	syl2anc	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to A /_{L} N \in ℤ$
17	16	zcnd	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to A /_{L} N \in ℂ$
18	17	mullidd	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to 1 (A /_{L} N) = A /_{L} N$
19	8 12 18	3eqtrd	$⊢ (A \in ℕ_{0} \land N \in ℤ \land N \neq 0) \to A /_{L} -N = A /_{L} N$
20	19	3expa	$⊢ ((A \in ℕ_{0} \land N \in ℤ) \land N \neq 0) \to A /_{L} -N = A /_{L} N$
21	5 20	pm2.61dane	$⊢ (A \in ℕ_{0} \land N \in ℤ) \to A /_{L} -N = A /_{L} N$

Metamath Proof Explorer

Theorem lgsneg1

Proof