lgsdilem

Description: Lemma for lgsdi and lgsdir : the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Assertion	lgsdilem	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to if ((N < 0 \land A B < 0), - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$

Proof

Step	Hyp	Ref	Expression
1		simplrr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to B \neq 0$
2	1	biantrud	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (0 \leq B \leftrightarrow (0 \leq B \land B \neq 0))$
3		0re	$⊢ 0 \in ℝ$
4		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to B \in ℤ$
5	4	zred	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to B \in ℝ$
6	5	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to B \in ℝ$
7		ltlen	$⊢ (0 \in ℝ \land B \in ℝ) \to (0 < B \leftrightarrow (0 \leq B \land B \neq 0))$
8	3 6 7	sylancr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (0 < B \leftrightarrow (0 \leq B \land B \neq 0))$
9		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A \in ℤ$
10	9	zred	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A \in ℝ$
11	10	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to A \in ℝ$
12	11	renegcld	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to - A \in ℝ$
13	12	recnd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to - A \in ℂ$
14	13	mul01d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (- A) \cdot 0 = 0$
15	11	recnd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to A \in ℂ$
16	6	recnd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to B \in ℂ$
17	15 16	mulneg1d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (- A) B = - A B$
18	14 17	breq12d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to ((- A) \cdot 0 < (- A) B \leftrightarrow 0 < - A B)$
19		0red	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to 0 \in ℝ$
20	10	lt0neg1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to (A < 0 \leftrightarrow 0 < - A)$
21	20	biimpa	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to 0 < - A$
22		ltmul2	$⊢ (0 \in ℝ \land B \in ℝ \land (- A \in ℝ \land 0 < - A)) \to (0 < B \leftrightarrow (- A) \cdot 0 < (- A) B)$
23	19 6 12 21 22	syl112anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (0 < B \leftrightarrow (- A) \cdot 0 < (- A) B)$
24	10 5	remulcld	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A B \in ℝ$
25	24	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to A B \in ℝ$
26	25	lt0neg1d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (A B < 0 \leftrightarrow 0 < - A B)$
27	18 23 26	3bitr4d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (0 < B \leftrightarrow A B < 0)$
28	2 8 27	3bitr2rd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (A B < 0 \leftrightarrow 0 \leq B)$
29		lenlt	$⊢ (0 \in ℝ \land B \in ℝ) \to (0 \leq B \leftrightarrow \neg B < 0)$
30	3 6 29	sylancr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (0 \leq B \leftrightarrow \neg B < 0)$
31	28 30	bitrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to (A B < 0 \leftrightarrow \neg B < 0)$
32	31	ifbid	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to if (A B < 0, - 1, 1) = if (\neg B < 0, - 1, 1)$
33		oveq2	$⊢ if (B < 0, - 1, 1) = - 1 \to -1 if (B < 0, - 1, 1) = -1 -1$
34		neg1mulneg1e1	$⊢ -1 -1 = 1$
35	33 34	eqtrdi	$⊢ if (B < 0, - 1, 1) = - 1 \to -1 if (B < 0, - 1, 1) = 1$
36		oveq2	$⊢ if (B < 0, - 1, 1) = 1 \to -1 if (B < 0, - 1, 1) = -1 \cdot 1$
37		ax-1cn	$⊢ 1 \in ℂ$
38	37	mulm1i	$⊢ -1 \cdot 1 = - 1$
39	36 38	eqtrdi	$⊢ if (B < 0, - 1, 1) = 1 \to -1 if (B < 0, - 1, 1) = - 1$
40	35 39	ifsb	$⊢ -1 if (B < 0, - 1, 1) = if (B < 0, 1, - 1)$
41		ifnot	$⊢ if (\neg B < 0, - 1, 1) = if (B < 0, 1, - 1)$
42	40 41	eqtr4i	$⊢ -1 if (B < 0, - 1, 1) = if (\neg B < 0, - 1, 1)$
43	32 42	eqtr4di	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to if (A B < 0, - 1, 1) = -1 if (B < 0, - 1, 1)$
44		iftrue	$⊢ A < 0 \to if (A < 0, - 1, 1) = - 1$
45	44	adantl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to if (A < 0, - 1, 1) = - 1$
46	45	oveq1d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to if (A < 0, - 1, 1) if (B < 0, - 1, 1) = -1 if (B < 0, - 1, 1)$
47	43 46	eqtr4d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land A < 0) \to if (A B < 0, - 1, 1) = if (A < 0, - 1, 1) if (B < 0, - 1, 1)$
48		iffalse	$⊢ \neg A < 0 \to if (A < 0, - 1, 1) = 1$
49	48	adantl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to if (A < 0, - 1, 1) = 1$
50	49	oveq1d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to if (A < 0, - 1, 1) if (B < 0, - 1, 1) = 1 if (B < 0, - 1, 1)$
51		neg1cn	$⊢ - 1 \in ℂ$
52	51 37	ifcli	$⊢ if (B < 0, - 1, 1) \in ℂ$
53	52	mulid2i	$⊢ 1 if (B < 0, - 1, 1) = if (B < 0, - 1, 1)$
54	5	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to B \in ℝ$
55		0red	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to 0 \in ℝ$
56	10	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to A \in ℝ$
57		lenlt	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow \neg A < 0)$
58	3 10 57	sylancr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to (0 \leq A \leftrightarrow \neg A < 0)$
59	58	biimpar	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to 0 \leq A$
60		simplrl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to A \neq 0$
61	56 59 60	ne0gt0d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to 0 < A$
62		ltmul2	$⊢ (B \in ℝ \land 0 \in ℝ \land (A \in ℝ \land 0 < A)) \to (B < 0 \leftrightarrow A B < A \cdot 0)$
63	54 55 56 61 62	syl112anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to (B < 0 \leftrightarrow A B < A \cdot 0)$
64	56	recnd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to A \in ℂ$
65	64	mul01d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to A \cdot 0 = 0$
66	65	breq2d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to (A B < A \cdot 0 \leftrightarrow A B < 0)$
67	63 66	bitrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to (B < 0 \leftrightarrow A B < 0)$
68	67	ifbid	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to if (B < 0, - 1, 1) = if (A B < 0, - 1, 1)$
69	53 68	syl5eq	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to 1 if (B < 0, - 1, 1) = if (A B < 0, - 1, 1)$
70	50 69	eqtr2d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg A < 0) \to if (A B < 0, - 1, 1) = if (A < 0, - 1, 1) if (B < 0, - 1, 1)$
71	47 70	pm2.61dan	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to if (A B < 0, - 1, 1) = if (A < 0, - 1, 1) if (B < 0, - 1, 1)$
72	71	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to if (A B < 0, - 1, 1) = if (A < 0, - 1, 1) if (B < 0, - 1, 1)$
73		simpr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to N < 0$
74	73	biantrurd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to (A B < 0 \leftrightarrow (N < 0 \land A B < 0))$
75	74	ifbid	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to if (A B < 0, - 1, 1) = if ((N < 0 \land A B < 0), - 1, 1)$
76	73	biantrurd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to (A < 0 \leftrightarrow (N < 0 \land A < 0))$
77	76	ifbid	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to if (A < 0, - 1, 1) = if ((N < 0 \land A < 0), - 1, 1)$
78	73	biantrurd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to (B < 0 \leftrightarrow (N < 0 \land B < 0))$
79	78	ifbid	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to if (B < 0, - 1, 1) = if ((N < 0 \land B < 0), - 1, 1)$
80	77 79	oveq12d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to if (A < 0, - 1, 1) if (B < 0, - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$
81	72 75 80	3eqtr3d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N < 0) \to if ((N < 0 \land A B < 0), - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$
82		simpr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to \neg N < 0$
83	82	intnanrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to \neg (N < 0 \land A B < 0)$
84	83	iffalsed	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to if ((N < 0 \land A B < 0), - 1, 1) = 1$
85		1t1e1	$⊢ 1 \cdot 1 = 1$
86	84 85	eqtr4di	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to if ((N < 0 \land A B < 0), - 1, 1) = 1 \cdot 1$
87	82	intnanrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to \neg (N < 0 \land A < 0)$
88	87	iffalsed	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to if ((N < 0 \land A < 0), - 1, 1) = 1$
89	82	intnanrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to \neg (N < 0 \land B < 0)$
90	89	iffalsed	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to if ((N < 0 \land B < 0), - 1, 1) = 1$
91	88 90	oveq12d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1) = 1 \cdot 1$
92	86 91	eqtr4d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land \neg N < 0) \to if ((N < 0 \land A B < 0), - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$
93	81 92	pm2.61dan	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to if ((N < 0 \land A B < 0), - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$

Metamath Proof Explorer

Theorem lgsdilem

Proof