lgsdirnn0

Description: Variation on lgsdir valid for all A , B but only for positive N . (The exact location of the failure of this law is for A = 0 , B < 0 , N = -u 1 in which case ( 0 /L -u 1 ) = 1 but ( B /L -u 1 ) = -u 1 .) (Contributed by Mario Carneiro, 28-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = B \to x /_{L} N = B /_{L} N$
2	1	oveq1d	$⊢ x = B \to (x /_{L} N) (0 /_{L} N) = (B /_{L} N) (0 /_{L} N)$
3	2	eqeq2d	$⊢ x = B \to (0 /_{L} N = (x /_{L} N) (0 /_{L} N) \leftrightarrow 0 /_{L} N = (B /_{L} N) (0 /_{L} N))$
4		id	$⊢ x \in ℤ \to x \in ℤ$
5		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
6		lgscl	$⊢ (x \in ℤ \land N \in ℤ) \to x /_{L} N \in ℤ$
7	4 5 6	syl2anr	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to x /_{L} N \in ℤ$
8	7	zcnd	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to x /_{L} N \in ℂ$
9	8	adantr	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N = 0) \to x /_{L} N \in ℂ$
10	9	mul01d	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N = 0) \to (x /_{L} N) \cdot 0 = 0$
11		simpr	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N = 0) \to 0 /_{L} N = 0$
12	11	oveq2d	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N = 0) \to (x /_{L} N) (0 /_{L} N) = (x /_{L} N) \cdot 0$
13	10 12 11	3eqtr4rd	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N = 0) \to 0 /_{L} N = (x /_{L} N) (0 /_{L} N)$
14		0z	$⊢ 0 \in ℤ$
15	5	adantr	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to N \in ℤ$
16		lgsne0	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 /_{L} N \neq 0 \leftrightarrow 0 \gcd N = 1)$
17	14 15 16	sylancr	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (0 /_{L} N \neq 0 \leftrightarrow 0 \gcd N = 1)$
18		gcdcom	$⊢ (0 \in ℤ \land N \in ℤ) \to 0 \gcd N = N \gcd 0$
19	14 15 18	sylancr	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to 0 \gcd N = N \gcd 0$
20		nn0gcdid0	$⊢ N \in ℕ_{0} \to N \gcd 0 = N$
21	20	adantr	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to N \gcd 0 = N$
22	19 21	eqtrd	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to 0 \gcd N = N$
23	22	eqeq1d	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (0 \gcd N = 1 \leftrightarrow N = 1)$
24		lgs1	$⊢ x \in ℤ \to x /_{L} 1 = 1$
25	24	adantl	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to x /_{L} 1 = 1$
26		oveq2	$⊢ N = 1 \to x /_{L} N = x /_{L} 1$
27	26	eqeq1d	$⊢ N = 1 \to (x /_{L} N = 1 \leftrightarrow x /_{L} 1 = 1)$
28	25 27	syl5ibrcom	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (N = 1 \to x /_{L} N = 1)$
29	23 28	sylbid	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (0 \gcd N = 1 \to x /_{L} N = 1)$
30	17 29	sylbid	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (0 /_{L} N \neq 0 \to x /_{L} N = 1)$
31	30	imp	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to x /_{L} N = 1$
32	31	oveq1d	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to (x /_{L} N) (0 /_{L} N) = 1 (0 /_{L} N)$
33	5	ad2antrr	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to N \in ℤ$
34		lgscl	$⊢ (0 \in ℤ \land N \in ℤ) \to 0 /_{L} N \in ℤ$
35	14 33 34	sylancr	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to 0 /_{L} N \in ℤ$
36	35	zcnd	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to 0 /_{L} N \in ℂ$
37	36	mulid2d	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to 1 (0 /_{L} N) = 0 /_{L} N$
38	32 37	eqtr2d	$⊢ ((N \in ℕ_{0} \land x \in ℤ) \land 0 /_{L} N \neq 0) \to 0 /_{L} N = (x /_{L} N) (0 /_{L} N)$
39	13 38	pm2.61dane	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to 0 /_{L} N = (x /_{L} N) (0 /_{L} N)$
40	39	ralrimiva	$⊢ N \in ℕ_{0} \to \forall x \in ℤ 0 /_{L} N = (x /_{L} N) (0 /_{L} N)$
41	40	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to \forall x \in ℤ 0 /_{L} N = (x /_{L} N) (0 /_{L} N)$
42		simp2	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to B \in ℤ$
43	3 41 42	rspcdva	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to 0 /_{L} N = (B /_{L} N) (0 /_{L} N)$
44	43	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to 0 /_{L} N = (B /_{L} N) (0 /_{L} N)$
45	5	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to N \in ℤ$
46	14 45 34	sylancr	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to 0 /_{L} N \in ℤ$
47	46	zcnd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to 0 /_{L} N \in ℂ$
48	47	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to 0 /_{L} N \in ℂ$
49		lgscl	$⊢ (B \in ℤ \land N \in ℤ) \to B /_{L} N \in ℤ$
50	42 45 49	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to B /_{L} N \in ℤ$
51	50	zcnd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to B /_{L} N \in ℂ$
52	51	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to B /_{L} N \in ℂ$
53	48 52	mulcomd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to (0 /_{L} N) (B /_{L} N) = (B /_{L} N) (0 /_{L} N)$
54	44 53	eqtr4d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to 0 /_{L} N = (0 /_{L} N) (B /_{L} N)$
55		oveq1	$⊢ A = 0 \to A B = 0 \cdot B$
56		zcn	$⊢ B \in ℤ \to B \in ℂ$
57	56	3ad2ant2	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to B \in ℂ$
58	57	mul02d	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to 0 \cdot B = 0$
59	55 58	sylan9eqr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to A B = 0$
60	59	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to A B /_{L} N = 0 /_{L} N$
61		simpr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to A = 0$
62	61	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to A /_{L} N = 0 /_{L} N$
63	62	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to (A /_{L} N) (B /_{L} N) = (0 /_{L} N) (B /_{L} N)$
64	54 60 63	3eqtr4d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land A = 0) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$
65		oveq1	$⊢ x = A \to x /_{L} N = A /_{L} N$
66	65	oveq1d	$⊢ x = A \to (x /_{L} N) (0 /_{L} N) = (A /_{L} N) (0 /_{L} N)$
67	66	eqeq2d	$⊢ x = A \to (0 /_{L} N = (x /_{L} N) (0 /_{L} N) \leftrightarrow 0 /_{L} N = (A /_{L} N) (0 /_{L} N))$
68		simp1	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A \in ℤ$
69	67 41 68	rspcdva	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to 0 /_{L} N = (A /_{L} N) (0 /_{L} N)$
70	69	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to 0 /_{L} N = (A /_{L} N) (0 /_{L} N)$
71		oveq2	$⊢ B = 0 \to A B = A \cdot 0$
72	68	zcnd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A \in ℂ$
73	72	mul01d	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A \cdot 0 = 0$
74	71 73	sylan9eqr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to A B = 0$
75	74	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to A B /_{L} N = 0 /_{L} N$
76		simpr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to B = 0$
77	76	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to B /_{L} N = 0 /_{L} N$
78	77	oveq2d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to (A /_{L} N) (B /_{L} N) = (A /_{L} N) (0 /_{L} N)$
79	70 75 78	3eqtr4d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land B = 0) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$
80		lgsdir	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$
81	5 80	syl3anl3	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \land (A \neq 0 \land B \neq 0)) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$
82	64 79 81	pm2.61da2ne	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$

Metamath Proof Explorer

Theorem lgsdirnn0

Proof