lgsneg

Description: The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Assertion	lgsneg	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} -N = if (A < 0, - 1, 1) (A /_{L} N)$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$⊢ A < 0 \to if (A < 0, - 1, 1) = - 1$
2	1	adantl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (A < 0, - 1, 1) = - 1$
3	2	oveq1d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) = -1 if ((N < 0 \land A < 0), - 1, 1)$
4		oveq2	$⊢ if (N < 0, - 1, 1) = - 1 \to -1 if (N < 0, - 1, 1) = -1 -1$
5		neg1mulneg1e1	$⊢ -1 -1 = 1$
6	4 5	syl6eq	$⊢ if (N < 0, - 1, 1) = - 1 \to -1 if (N < 0, - 1, 1) = 1$
7		oveq2	$⊢ if (N < 0, - 1, 1) = 1 \to -1 if (N < 0, - 1, 1) = -1 \cdot 1$
8		ax-1cn	$⊢ 1 \in ℂ$
9	8	mulm1i	$⊢ -1 \cdot 1 = - 1$
10	7 9	syl6eq	$⊢ if (N < 0, - 1, 1) = 1 \to -1 if (N < 0, - 1, 1) = - 1$
11	6 10	ifsb	$⊢ -1 if (N < 0, - 1, 1) = if (N < 0, 1, - 1)$
12		simpr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to A < 0$
13	12	biantrud	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (N < 0 \leftrightarrow (N < 0 \land A < 0))$
14	13	ifbid	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (N < 0, - 1, 1) = if ((N < 0 \land A < 0), - 1, 1)$
15	14	oveq2d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to -1 if (N < 0, - 1, 1) = -1 if ((N < 0 \land A < 0), - 1, 1)$
16		simpl3	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to N \neq 0$
17	16	necomd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to 0 \neq N$
18		simpl2	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to N \in ℤ$
19	18	zred	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to N \in ℝ$
20		0re	$⊢ 0 \in ℝ$
21		ltlen	$⊢ (N \in ℝ \land 0 \in ℝ) \to (N < 0 \leftrightarrow (N \leq 0 \land 0 \neq N))$
22	19 20 21	sylancl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (N < 0 \leftrightarrow (N \leq 0 \land 0 \neq N))$
23	17 22	mpbiran2d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (N < 0 \leftrightarrow N \leq 0)$
24	19	le0neg1d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (N \leq 0 \leftrightarrow 0 \leq - N)$
25	19	renegcld	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to - N \in ℝ$
26		lenlt	$⊢ (0 \in ℝ \land - N \in ℝ) \to (0 \leq - N \leftrightarrow \neg - N < 0)$
27	20 25 26	sylancr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (0 \leq - N \leftrightarrow \neg - N < 0)$
28	23 24 27	3bitrd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (N < 0 \leftrightarrow \neg - N < 0)$
29	28	ifbid	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (N < 0, 1, - 1) = if (\neg - N < 0, 1, - 1)$
30		ifnot	$⊢ if (\neg - N < 0, 1, - 1) = if (- N < 0, - 1, 1)$
31	29 30	syl6eq	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (N < 0, 1, - 1) = if (- N < 0, - 1, 1)$
32	11 15 31	3eqtr3a	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to -1 if ((N < 0 \land A < 0), - 1, 1) = if (- N < 0, - 1, 1)$
33	12	biantrud	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to (- N < 0 \leftrightarrow (- N < 0 \land A < 0))$
34	33	ifbid	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (- N < 0, - 1, 1) = if ((- N < 0 \land A < 0), - 1, 1)$
35	3 32 34	3eqtrd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A < 0) \to if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) = if ((- N < 0 \land A < 0), - 1, 1)$
36		1t1e1	$⊢ 1 \cdot 1 = 1$
37		iffalse	$⊢ \neg A < 0 \to if (A < 0, - 1, 1) = 1$
38	37	adantl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to if (A < 0, - 1, 1) = 1$
39		simpr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to \neg A < 0$
40	39	intnand	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to \neg (N < 0 \land A < 0)$
41	40	iffalsed	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to if ((N < 0 \land A < 0), - 1, 1) = 1$
42	38 41	oveq12d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) = 1 \cdot 1$
43	39	intnand	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to \neg (- N < 0 \land A < 0)$
44	43	iffalsed	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to if ((- N < 0 \land A < 0), - 1, 1) = 1$
45	36 42 44	3eqtr4a	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land \neg A < 0) \to if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) = if ((- N < 0 \land A < 0), - 1, 1)$
46	35 45	pm2.61dan	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) = if ((- N < 0 \land A < 0), - 1, 1)$
47	46	eqcomd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if ((- N < 0 \land A < 0), - 1, 1) = if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1)$
48		simpr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℙ) \to n \in ℙ$
49		simpl2	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℙ) \to N \in ℤ$
50		zq	$⊢ N \in ℤ \to N \in ℚ$
51	49 50	syl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℙ) \to N \in ℚ$
52		pcneg	$⊢ (n \in ℙ \land N \in ℚ) \to n pCnt -N = n pCnt N$
53	48 51 52	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℙ) \to n pCnt -N = n pCnt N$
54	53	oveq2d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℙ) \to {(A /_{L} n)}^{n pCnt -N} = {(A /_{L} n)}^{n pCnt N}$
55	54	ifeq1da	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1) = if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)$
56	55	mpteq2dv	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
57	56	seqeq3d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)))$
58		zcn	$⊢ N \in ℤ \to N \in ℂ$
59	58	3ad2ant2	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to N \in ℂ$
60	59	absnegd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to \|- N\| = \|N\|$
61	57 60	fveq12d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))) (\|- N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
62	47 61	oveq12d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if ((- N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))) (\|- N\|) = if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
63		neg1cn	$⊢ - 1 \in ℂ$
64	63 8	ifcli	$⊢ if (A < 0, - 1, 1) \in ℂ$
65	64	a1i	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if (A < 0, - 1, 1) \in ℂ$
66	63 8	ifcli	$⊢ if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
67	66	a1i	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
68		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
69	68	3adant1	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
70		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
71	69 70	eleqtrdi	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to \|N\| \in ℤ_{\geq 1}$
72		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
73	72	lgsfcl3	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
74		elfznn	$⊢ x \in (1 \dots \|N\|) \to x \in ℕ$
75		ffvelrn	$⊢ ((n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ \land x \in ℕ) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (x) \in ℤ$
76	73 74 75	syl2an	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land x \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (x) \in ℤ$
77		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
78	77	adantl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
79	71 76 78	seqcl	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℤ$
80	79	zcnd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℂ$
81	65 67 80	mulassd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
82	62 81	eqtrd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if ((- N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))) (\|- N\|) = if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
83		simp1	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A \in ℤ$
84		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
85	84	3ad2ant2	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to - N \in ℤ$
86		simp3	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to N \neq 0$
87	59 86	negne0d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to - N \neq 0$
88		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))$
89	88	lgsval4	$⊢ (A \in ℤ \land - N \in ℤ \land - N \neq 0) \to A /_{L} -N = if ((- N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))) (\|- N\|)$
90	83 85 87 89	syl3anc	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} -N = if ((- N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt -N}, 1))) (\|- N\|)$
91	72	lgsval4	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} N = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
92	91	oveq2d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if (A < 0, - 1, 1) (A /_{L} N) = if (A < 0, - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
93	82 90 92	3eqtr4d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} -N = if (A < 0, - 1, 1) (A /_{L} N)$

Metamath Proof Explorer

Theorem lgsneg

Proof