lgsdinn0

Description: Variation on lgsdi valid for all M , N but only for positive A . (The exact location of the failure of this law is for A = -u 1 , M = 0 , and some N in which case ( -u 1 /L 0 ) = 1 but ( -u 1 /L N ) = -u 1 when -u 1 is not a quadratic residue mod N .) (Contributed by Mario Carneiro, 28-Apr-2016)

		Ref	Expression
	Assertion	lgsdinn0	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = N \to A /_{L} x = A /_{L} N$
2	1	oveq1d	$⊢ x = N \to (A /_{L} x) (A /_{L} 0) = (A /_{L} N) (A /_{L} 0)$
3	2	eqeq2d	$⊢ x = N \to (A /_{L} 0 = (A /_{L} x) (A /_{L} 0) \leftrightarrow A /_{L} 0 = (A /_{L} N) (A /_{L} 0))$
4		sq1	$⊢ 1^{2} = 1$
5	4	eqeq2i	$⊢ A^{2} = 1^{2} \leftrightarrow A^{2} = 1$
6		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
7		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
8		1re	$⊢ 1 \in ℝ$
9		0le1	$⊢ 0 \leq 1$
10		sq11	$⊢ ((A \in ℝ \land 0 \leq A) \land (1 \in ℝ \land 0 \leq 1)) \to (A^{2} = 1^{2} \leftrightarrow A = 1)$
11	8 9 10	mpanr12	$⊢ (A \in ℝ \land 0 \leq A) \to (A^{2} = 1^{2} \leftrightarrow A = 1)$
12	6 7 11	syl2anc	$⊢ A \in ℕ_{0} \to (A^{2} = 1^{2} \leftrightarrow A = 1)$
13	12	adantr	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to (A^{2} = 1^{2} \leftrightarrow A = 1)$
14	5 13	bitr3id	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to (A^{2} = 1 \leftrightarrow A = 1)$
15	14	biimpa	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A = 1$
16	15	oveq1d	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A /_{L} x = 1 /_{L} x$
17		1lgs	$⊢ x \in ℤ \to 1 /_{L} x = 1$
18	17	ad2antlr	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to 1 /_{L} x = 1$
19	16 18	eqtrd	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A /_{L} x = 1$
20	19	oveq1d	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to (A /_{L} x) (A /_{L} 0) = 1 (A /_{L} 0)$
21		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
22	21	ad2antrr	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A \in ℤ$
23		0z	$⊢ 0 \in ℤ$
24		lgscl	$⊢ (A \in ℤ \land 0 \in ℤ) \to A /_{L} 0 \in ℤ$
25	22 23 24	sylancl	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A /_{L} 0 \in ℤ$
26	25	zcnd	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A /_{L} 0 \in ℂ$
27	26	mullidd	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to 1 (A /_{L} 0) = A /_{L} 0$
28	20 27	eqtr2d	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} = 1) \to A /_{L} 0 = (A /_{L} x) (A /_{L} 0)$
29		lgscl	$⊢ (A \in ℤ \land x \in ℤ) \to A /_{L} x \in ℤ$
30	21 29	sylan	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to A /_{L} x \in ℤ$
31	30	zcnd	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to A /_{L} x \in ℂ$
32	31	adantr	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} \neq 1) \to A /_{L} x \in ℂ$
33	32	mul01d	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} \neq 1) \to (A /_{L} x) \cdot 0 = 0$
34	21	adantr	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to A \in ℤ$
35		lgs0	$⊢ A \in ℤ \to A /_{L} 0 = if (A^{2} = 1, 1, 0)$
36	34 35	syl	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to A /_{L} 0 = if (A^{2} = 1, 1, 0)$
37		ifnefalse	$⊢ A^{2} \neq 1 \to if (A^{2} = 1, 1, 0) = 0$
38	36 37	sylan9eq	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} \neq 1) \to A /_{L} 0 = 0$
39	38	oveq2d	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} \neq 1) \to (A /_{L} x) (A /_{L} 0) = (A /_{L} x) \cdot 0$
40	33 39 38	3eqtr4rd	$⊢ ((A \in ℕ_{0} \land x \in ℤ) \land A^{2} \neq 1) \to A /_{L} 0 = (A /_{L} x) (A /_{L} 0)$
41	28 40	pm2.61dane	$⊢ (A \in ℕ_{0} \land x \in ℤ) \to A /_{L} 0 = (A /_{L} x) (A /_{L} 0)$
42	41	ralrimiva	$⊢ A \in ℕ_{0} \to \forall x \in ℤ A /_{L} 0 = (A /_{L} x) (A /_{L} 0)$
43	42	3ad2ant1	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to \forall x \in ℤ A /_{L} 0 = (A /_{L} x) (A /_{L} 0)$
44		simp3	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
45	3 43 44	rspcdva	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} 0 = (A /_{L} N) (A /_{L} 0)$
46	45	adantr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} 0 = (A /_{L} N) (A /_{L} 0)$
47	21	3ad2ant1	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A \in ℤ$
48	47 23 24	sylancl	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} 0 \in ℤ$
49	48	zcnd	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} 0 \in ℂ$
50	49	adantr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} 0 \in ℂ$
51		lgscl	$⊢ (A \in ℤ \land N \in ℤ) \to A /_{L} N \in ℤ$
52	47 44 51	syl2anc	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} N \in ℤ$
53	52	zcnd	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} N \in ℂ$
54	53	adantr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} N \in ℂ$
55	50 54	mulcomd	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to (A /_{L} 0) (A /_{L} N) = (A /_{L} N) (A /_{L} 0)$
56	46 55	eqtr4d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} 0 = (A /_{L} 0) (A /_{L} N)$
57		oveq1	$⊢ M = 0 \to M \cdot N = 0 \cdot N$
58	44	zcnd	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to N \in ℂ$
59	58	mul02d	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to 0 \cdot N = 0$
60	57 59	sylan9eqr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to M \cdot N = 0$
61	60	oveq2d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} M \cdot N = A /_{L} 0$
62		simpr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to M = 0$
63	62	oveq2d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} M = A /_{L} 0$
64	63	oveq1d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to (A /_{L} M) (A /_{L} N) = (A /_{L} 0) (A /_{L} N)$
65	56 61 64	3eqtr4d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$
66		oveq2	$⊢ x = M \to A /_{L} x = A /_{L} M$
67	66	oveq1d	$⊢ x = M \to (A /_{L} x) (A /_{L} 0) = (A /_{L} M) (A /_{L} 0)$
68	67	eqeq2d	$⊢ x = M \to (A /_{L} 0 = (A /_{L} x) (A /_{L} 0) \leftrightarrow A /_{L} 0 = (A /_{L} M) (A /_{L} 0))$
69		simp2	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
70	68 43 69	rspcdva	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} 0 = (A /_{L} M) (A /_{L} 0)$
71	70	adantr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to A /_{L} 0 = (A /_{L} M) (A /_{L} 0)$
72		oveq2	$⊢ N = 0 \to M \cdot N = M \cdot 0$
73	69	zcnd	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to M \in ℂ$
74	73	mul01d	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to M \cdot 0 = 0$
75	72 74	sylan9eqr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to M \cdot N = 0$
76	75	oveq2d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to A /_{L} M \cdot N = A /_{L} 0$
77		simpr	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to N = 0$
78	77	oveq2d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to A /_{L} N = A /_{L} 0$
79	78	oveq2d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to (A /_{L} M) (A /_{L} N) = (A /_{L} M) (A /_{L} 0)$
80	71 76 79	3eqtr4d	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land N = 0) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$
81		lgsdi	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$
82	21 81	syl3anl1	$⊢ ((A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$
83	65 80 82	pm2.61da2ne	$⊢ (A \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$

Metamath Proof Explorer

Theorem lgsdinn0

Proof