Metamath Proof Explorer


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 mulid2d ( ( ( 𝑁 ∈ ℕ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 𝑁 ) ) )