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