Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℤ) |
2 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ) |
3 | | nn0z 11277 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
4 | | lgscl 24836 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 /L 𝑁) ∈
ℤ) |
5 | 2, 3, 4 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥
/L 𝑁)
∈ ℤ) |
6 | 5 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥
/L 𝑁)
∈ ℂ) |
7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → (𝑥 /L 𝑁) ∈ ℂ) |
8 | 7 | mul01d 10114 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → ((𝑥 /L 𝑁) · 0) = 0) |
9 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → (0 /L 𝑁) = 0) |
10 | 9 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = ((𝑥 /L 𝑁) · 0)) |
11 | 8, 10, 9 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) = 0) → (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
12 | | 0z 11265 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
13 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
14 | | lgsne0 24860 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → ((0 /L 𝑁) ≠ 0 ↔ (0 gcd 𝑁) = 1)) |
15 | 12, 13, 14 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 /L 𝑁) ≠ 0 ↔ (0 gcd 𝑁) = 1)) |
16 | | gcdcom 15073 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 gcd 𝑁) = (𝑁 gcd 0)) |
17 | 12, 13, 16 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (0 gcd 𝑁) = (𝑁 gcd 0)) |
18 | | nn0gcdid0 15080 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (𝑁 gcd 0) = 𝑁) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑁 gcd 0) = 𝑁) |
20 | 17, 19 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (0 gcd 𝑁) = 𝑁) |
21 | 20 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 gcd 𝑁) = 1
↔ 𝑁 =
1)) |
22 | | lgs1 24866 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (𝑥 /L 1) =
1) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥
/L 1) = 1) |
24 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = 1 → (𝑥 /L 𝑁) = (𝑥 /L 1)) |
25 | 24 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = 1 → ((𝑥 /L 𝑁) = 1 ↔ (𝑥 /L 1) =
1)) |
26 | 23, 25 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑁 = 1 → (𝑥 /L 𝑁) = 1)) |
27 | 21, 26 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 gcd 𝑁) = 1
→ (𝑥
/L 𝑁) =
1)) |
28 | 15, 27 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((0 /L 𝑁) ≠ 0 → (𝑥 /L 𝑁) = 1)) |
29 | 28 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (𝑥 /L 𝑁) = 1) |
30 | 29 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = (1 · (0
/L 𝑁))) |
31 | 3 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → 𝑁 ∈ ℤ) |
32 | | lgscl 24836 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 /L 𝑁) ∈ ℤ) |
33 | 12, 31, 32 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (0 /L
𝑁) ∈
ℤ) |
34 | 33 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (0 /L
𝑁) ∈
ℂ) |
35 | 34 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (1 · (0
/L 𝑁)) =
(0 /L 𝑁)) |
36 | 30, 35 | eqtr2d 2645 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (0 /L 𝑁) ≠ 0) → (0 /L
𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
37 | 11, 36 | pm2.61dane 2869 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
38 | 37 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
ℤ (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
39 | 38 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ∀𝑥 ∈
ℤ (0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁))) |
40 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝑥 /L 𝑁) = (𝐵 /L 𝑁)) |
41 | 40 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = ((𝐵 /L 𝑁) · (0 /L 𝑁))) |
42 | 41 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁)) ↔ (0
/L 𝑁) =
((𝐵 /L
𝑁) · (0
/L 𝑁)))) |
43 | 42 | rspcv 3278 |
. . . . . 6
⊢ (𝐵 ∈ ℤ →
(∀𝑥 ∈ ℤ
(0 /L 𝑁)
= ((𝑥 /L
𝑁) · (0
/L 𝑁))
→ (0 /L 𝑁) = ((𝐵 /L 𝑁) · (0 /L 𝑁)))) |
44 | 1, 39, 43 | sylc 63 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) = ((𝐵 /L 𝑁) · (0 /L 𝑁))) |
45 | 44 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (0
/L 𝑁) =
((𝐵 /L
𝑁) · (0
/L 𝑁))) |
46 | 3 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
47 | 12, 46, 32 | sylancr 694 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) ∈ ℤ) |
48 | 47 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) ∈ ℂ) |
49 | 48 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (0
/L 𝑁)
∈ ℂ) |
50 | | lgscl 24836 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵 /L 𝑁) ∈
ℤ) |
51 | 1, 46, 50 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐵
/L 𝑁)
∈ ℤ) |
52 | 51 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐵
/L 𝑁)
∈ ℂ) |
53 | 52 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (𝐵 /L 𝑁) ∈
ℂ) |
54 | 49, 53 | mulcomd 9940 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((0
/L 𝑁)
· (𝐵
/L 𝑁)) =
((𝐵 /L
𝑁) · (0
/L 𝑁))) |
55 | 45, 54 | eqtr4d 2647 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (0
/L 𝑁) =
((0 /L 𝑁)
· (𝐵
/L 𝑁))) |
56 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = 0 → (𝐴 · 𝐵) = (0 · 𝐵)) |
57 | | zcn 11259 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
58 | 57 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℂ) |
59 | 58 | mul02d 10113 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 · 𝐵) =
0) |
60 | 56, 59 | sylan9eqr 2666 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (𝐴 · 𝐵) = 0) |
61 | 60 | oveq1d 6564 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((𝐴 · 𝐵) /L 𝑁) = (0 /L 𝑁)) |
62 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → 𝐴 = 0) |
63 | 62 | oveq1d 6564 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → (𝐴 /L 𝑁) = (0 /L
𝑁)) |
64 | 63 | oveq1d 6564 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = ((0 /L 𝑁) · (𝐵 /L 𝑁))) |
65 | 55, 61, 64 | 3eqtr4d 2654 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 = 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
66 | | simp1 1054 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
67 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 /L 𝑁) = (𝐴 /L 𝑁)) |
68 | 67 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 /L 𝑁) · (0 /L 𝑁)) = ((𝐴 /L 𝑁) · (0 /L 𝑁))) |
69 | 68 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((0 /L 𝑁) = ((𝑥 /L 𝑁) · (0 /L 𝑁)) ↔ (0
/L 𝑁) =
((𝐴 /L
𝑁) · (0
/L 𝑁)))) |
70 | 69 | rspcv 3278 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
(∀𝑥 ∈ ℤ
(0 /L 𝑁)
= ((𝑥 /L
𝑁) · (0
/L 𝑁))
→ (0 /L 𝑁) = ((𝐴 /L 𝑁) · (0 /L 𝑁)))) |
71 | 66, 39, 70 | sylc 63 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (0 /L 𝑁) = ((𝐴 /L 𝑁) · (0 /L 𝑁))) |
72 | 71 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → (0
/L 𝑁) =
((𝐴 /L
𝑁) · (0
/L 𝑁))) |
73 | | oveq2 6557 |
. . . . 5
⊢ (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0)) |
74 | 66 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
75 | 74 | mul01d 10114 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 · 0) =
0) |
76 | 73, 75 | sylan9eqr 2666 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → (𝐴 · 𝐵) = 0) |
77 | 76 | oveq1d 6564 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → ((𝐴 · 𝐵) /L 𝑁) = (0 /L 𝑁)) |
78 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → 𝐵 = 0) |
79 | 78 | oveq1d 6564 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → (𝐵 /L 𝑁) = (0 /L
𝑁)) |
80 | 79 | oveq2d 6565 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = ((𝐴 /L 𝑁) · (0 /L 𝑁))) |
81 | 72, 77, 80 | 3eqtr4d 2654 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝐵 = 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
82 | | lgsdir 24857 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
83 | 3, 82 | syl3anl3 1368 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
84 | 65, 81, 83 | pm2.61da2ne 2870 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |