Step | Hyp | Ref
| Expression |
1 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑥 /L 𝑁) = (𝐵 /L 𝑁)) |
2 | 1 | oveq1d 7185 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = ((𝐵 /L 𝑁) · (0 /L 𝑁))) |
3 | 2 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁)) ↔ (0
/L 𝑁) =
((𝐵 /L
𝑁) · (0
/L 𝑁)))) |
4 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ) |
5 | | nn0z 12086 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
6 | | lgscl 26047 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 /L 𝑁) ∈
ℤ) |
7 | 4, 5, 6 | syl2anr 600 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥
/L 𝑁)
∈ ℤ) |
8 | 7 | zcnd 12169 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥
/L 𝑁)
∈ ℂ) |
9 | 8 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → (𝑥 /L 𝑁) ∈ ℂ) |
10 | 9 | mul01d 10917 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → ((𝑥 /L 𝑁) · 0) = 0) |
11 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → (0 /L 𝑁) = 0) |
12 | 11 | oveq2d 7186 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = ((𝑥 /L 𝑁) · 0)) |
13 | 10, 12, 11 | 3eqtr4rd 2784 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
14 | | 0z 12073 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
15 | 5 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
16 | | lgsne0 26071 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → ((0 /L 𝑁) ≠ 0 ↔ (0 gcd 𝑁) = 1)) |
17 | 14, 15, 16 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 /L 𝑁) ≠ 0 ↔ (0 gcd 𝑁) = 1)) |
18 | | gcdcom 15956 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 gcd 𝑁) = (𝑁 gcd 0)) |
19 | 14, 15, 18 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (0 gcd 𝑁) = (𝑁 gcd 0)) |
20 | | nn0gcdid0 15964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (𝑁 gcd 0) = 𝑁) |
21 | 20 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑁 gcd 0) = 𝑁) |
22 | 19, 21 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (0 gcd 𝑁) = 𝑁) |
23 | 22 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 gcd 𝑁) = 1
↔ 𝑁 =
1)) |
24 | | lgs1 26077 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (𝑥 /L 1) =
1) |
25 | 24 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥
/L 1) = 1) |
26 | | oveq2 7178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = 1 → (𝑥 /L 𝑁) = (𝑥 /L 1)) |
27 | 26 | eqeq1d 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = 1 → ((𝑥 /L 𝑁) = 1 ↔ (𝑥 /L 1) =
1)) |
28 | 25, 27 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑁 = 1 → (𝑥 /L 𝑁) = 1)) |
29 | 23, 28 | sylbid 243 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 gcd 𝑁) = 1
→ (𝑥
/L 𝑁) =
1)) |
30 | 17, 29 | sylbid 243 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 /L 𝑁) ≠ 0 → (𝑥 /L 𝑁) = 1)) |
31 | 30 | imp 410 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (𝑥 /L 𝑁) = 1) |
32 | 31 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = (1 · (0
/L 𝑁))) |
33 | 5 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → 𝑁 ∈ ℤ) |
34 | | lgscl 26047 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 /L 𝑁) ∈ ℤ) |
35 | 14, 33, 34 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (0 /L
𝑁) ∈
ℤ) |
36 | 35 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (0 /L
𝑁) ∈
ℂ) |
37 | 36 | mulid2d 10737 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (1 · (0
/L 𝑁)) =
(0 /L 𝑁)) |
38 | 32, 37 | eqtr2d 2774 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (0 /L
𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
39 | 13, 38 | pm2.61dane 3021 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
40 | 39 | ralrimiva 3096 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
ℤ (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
41 | 40 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ∀𝑥 ∈
ℤ (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
42 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℤ) |
43 | 3, 41, 42 | rspcdva 3528 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) = ((𝐵 /L 𝑁) · (0 /L 𝑁))) |
44 | 43 | adantr 484 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (0
/L 𝑁) =
((𝐵 /L
𝑁) · (0
/L 𝑁))) |
45 | 5 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
46 | 14, 45, 34 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) ∈ ℤ) |
47 | 46 | zcnd 12169 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) ∈ ℂ) |
48 | 47 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (0
/L 𝑁)
∈ ℂ) |
49 | | lgscl 26047 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵 /L 𝑁) ∈
ℤ) |
50 | 42, 45, 49 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐵
/L 𝑁)
∈ ℤ) |
51 | 50 | zcnd 12169 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐵
/L 𝑁)
∈ ℂ) |
52 | 51 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (𝐵 /L 𝑁) ∈
ℂ) |
53 | 48, 52 | mulcomd 10740 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((0
/L 𝑁)
· (𝐵
/L 𝑁)) =
((𝐵 /L
𝑁) · (0
/L 𝑁))) |
54 | 44, 53 | eqtr4d 2776 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (0
/L 𝑁) =
((0 /L 𝑁)
· (𝐵
/L 𝑁))) |
55 | | oveq1 7177 |
. . . . 5
⊢ (𝐴 = 0 → (𝐴 · 𝐵) = (0 · 𝐵)) |
56 | | zcn 12067 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
57 | 56 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℂ) |
58 | 57 | mul02d 10916 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 · 𝐵) =
0) |
59 | 55, 58 | sylan9eqr 2795 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (𝐴 · 𝐵) = 0) |
60 | 59 | oveq1d 7185 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((𝐴 · 𝐵) /L 𝑁) = (0 /L 𝑁)) |
61 | | simpr 488 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → 𝐴 = 0) |
62 | 61 | oveq1d 7185 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (𝐴 /L 𝑁) = (0 /L
𝑁)) |
63 | 62 | oveq1d 7185 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = ((0 /L 𝑁) · (𝐵 /L 𝑁))) |
64 | 54, 60, 63 | 3eqtr4d 2783 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
65 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 /L 𝑁) = (𝐴 /L 𝑁)) |
66 | 65 | oveq1d 7185 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = ((𝐴 /L 𝑁) · (0 /L 𝑁))) |
67 | 66 | eqeq2d 2749 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁)) ↔ (0
/L 𝑁) =
((𝐴 /L
𝑁) · (0
/L 𝑁)))) |
68 | | simp1 1137 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
69 | 67, 41, 68 | rspcdva 3528 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) = ((𝐴 /L 𝑁) · (0 /L 𝑁))) |
70 | 69 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → (0
/L 𝑁) =
((𝐴 /L
𝑁) · (0
/L 𝑁))) |
71 | | oveq2 7178 |
. . . . 5
⊢ (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0)) |
72 | 68 | zcnd 12169 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
73 | 72 | mul01d 10917 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 · 0) =
0) |
74 | 71, 73 | sylan9eqr 2795 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → (𝐴 · 𝐵) = 0) |
75 | 74 | oveq1d 7185 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → ((𝐴 · 𝐵) /L 𝑁) = (0 /L 𝑁)) |
76 | | simpr 488 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → 𝐵 = 0) |
77 | 76 | oveq1d 7185 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → (𝐵 /L 𝑁) = (0 /L
𝑁)) |
78 | 77 | oveq2d 7186 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = ((𝐴 /L 𝑁) · (0 /L 𝑁))) |
79 | 70, 75, 78 | 3eqtr4d 2783 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
80 | | lgsdir 26068 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
81 | 5, 80 | syl3anl3 1415 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
82 | 64, 79, 81 | pm2.61da2ne 3022 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |