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 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 𝑁 ) ) )