Theorem 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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )

Proof

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