Step | Hyp | Ref
| Expression |
1 | | simp3 1056 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
2 | | sq1 12820 |
. . . . . . . . . . . . . . . 16
⊢
(1↑2) = 1 |
3 | 2 | eqeq2i 2622 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴↑2) = (1↑2) ↔
(𝐴↑2) =
1) |
4 | | nn0re 11178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
5 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
6 | | 1re 9918 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
7 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
1 |
8 | | sq11 12798 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (1 ∈ ℝ
∧ 0 ≤ 1)) → ((𝐴↑2) = (1↑2) ↔ 𝐴 = 1)) |
9 | 6, 7, 8 | mpanr12 717 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝐴↑2) = (1↑2) ↔
𝐴 = 1)) |
10 | 4, 5, 9 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℕ0
→ ((𝐴↑2) =
(1↑2) ↔ 𝐴 =
1)) |
11 | 10 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((𝐴↑2) =
(1↑2) ↔ 𝐴 =
1)) |
12 | 3, 11 | syl5bbr 273 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((𝐴↑2) = 1
↔ 𝐴 =
1)) |
13 | 12 | biimpa 500 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ 𝐴 =
1) |
14 | 13 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (𝐴
/L 𝑥) =
(1 /L 𝑥)) |
15 | | 1lgs 24865 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → (1
/L 𝑥) =
1) |
16 | 15 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (1 /L 𝑥) = 1) |
17 | 14, 16 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (𝐴
/L 𝑥) =
1) |
18 | 17 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ ((𝐴
/L 𝑥)
· (𝐴
/L 0)) = (1 · (𝐴 /L 0))) |
19 | | nn0z 11277 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
20 | 19 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ 𝐴 ∈
ℤ) |
21 | | 0z 11265 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
22 | | lgscl 24836 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 0 ∈
ℤ) → (𝐴
/L 0) ∈ ℤ) |
23 | 20, 21, 22 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (𝐴
/L 0) ∈ ℤ) |
24 | 23 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (𝐴
/L 0) ∈ ℂ) |
25 | 24 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (1 · (𝐴
/L 0)) = (𝐴 /L 0)) |
26 | 18, 25 | eqtr2d 2645 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) = 1)
→ (𝐴
/L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0))) |
27 | | lgscl 24836 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝐴 /L 𝑥) ∈
ℤ) |
28 | 19, 27 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝐴
/L 𝑥)
∈ ℤ) |
29 | 28 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝐴
/L 𝑥)
∈ ℂ) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) ≠ 1)
→ (𝐴
/L 𝑥)
∈ ℂ) |
31 | 30 | mul01d 10114 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) ≠ 1)
→ ((𝐴
/L 𝑥)
· 0) = 0) |
32 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
33 | | lgs0 24835 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (𝐴 /L 0) =
if((𝐴↑2) = 1, 1,
0)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝐴
/L 0) = if((𝐴↑2) = 1, 1, 0)) |
35 | | ifnefalse 4048 |
. . . . . . . . . . . 12
⊢ ((𝐴↑2) ≠ 1 → if((𝐴↑2) = 1, 1, 0) =
0) |
36 | 34, 35 | sylan9eq 2664 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) ≠ 1)
→ (𝐴
/L 0) = 0) |
37 | 36 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) ≠ 1)
→ ((𝐴
/L 𝑥)
· (𝐴
/L 0)) = ((𝐴 /L 𝑥) · 0)) |
38 | 31, 37, 36 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
∧ (𝐴↑2) ≠ 1)
→ (𝐴
/L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0))) |
39 | 26, 38 | pm2.61dane 2869 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝐴
/L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0))) |
40 | 39 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ ∀𝑥 ∈
ℤ (𝐴
/L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0))) |
41 | 40 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ ∀𝑥 ∈
ℤ (𝐴
/L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0))) |
42 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝐴 /L 𝑥) = (𝐴 /L 𝑁)) |
43 | 42 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝐴 /L 𝑥) · (𝐴 /L 0)) = ((𝐴 /L 𝑁) · (𝐴 /L 0))) |
44 | 43 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝐴 /L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0)) ↔ (𝐴 /L 0) =
((𝐴 /L
𝑁) · (𝐴 /L
0)))) |
45 | 44 | rspcv 3278 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(∀𝑥 ∈ ℤ
(𝐴 /L 0)
= ((𝐴 /L
𝑥) · (𝐴 /L 0)) →
(𝐴 /L 0)
= ((𝐴 /L
𝑁) · (𝐴 /L
0)))) |
46 | 1, 41, 45 | sylc 63 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L 0) = ((𝐴 /L 𝑁) · (𝐴 /L 0))) |
47 | 46 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L 0) =
((𝐴 /L
𝑁) · (𝐴 /L
0))) |
48 | 19 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
49 | 48, 21, 22 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L 0) ∈ ℤ) |
50 | 49 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L 0) ∈ ℂ) |
51 | 50 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L 0) ∈
ℂ) |
52 | | lgscl 24836 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈
ℤ) |
53 | 48, 1, 52 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L 𝑁)
∈ ℤ) |
54 | 53 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L 𝑁)
∈ ℂ) |
55 | 54 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L 𝑁) ∈
ℂ) |
56 | 51, 55 | mulcomd 9940 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → ((𝐴 /L 0)
· (𝐴
/L 𝑁)) =
((𝐴 /L
𝑁) · (𝐴 /L
0))) |
57 | 47, 56 | eqtr4d 2647 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L 0) =
((𝐴 /L 0)
· (𝐴
/L 𝑁))) |
58 | | oveq1 6556 |
. . . . 5
⊢ (𝑀 = 0 → (𝑀 · 𝑁) = (0 · 𝑁)) |
59 | 1 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ 𝑁 ∈
ℂ) |
60 | 59 | mul02d 10113 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (0 · 𝑁) =
0) |
61 | 58, 60 | sylan9eqr 2666 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝑀 · 𝑁) = 0) |
62 | 61 | oveq2d 6565 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L (𝑀 · 𝑁)) = (𝐴 /L 0)) |
63 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → 𝑀 = 0) |
64 | 63 | oveq2d 6565 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L 𝑀) = (𝐴 /L 0)) |
65 | 64 | oveq1d 6564 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)) = ((𝐴 /L 0) · (𝐴 /L 𝑁))) |
66 | 57, 62, 65 | 3eqtr4d 2654 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑀 = 0) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |
67 | | simp2 1055 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ 𝑀 ∈
ℤ) |
68 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝐴 /L 𝑥) = (𝐴 /L 𝑀)) |
69 | 68 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → ((𝐴 /L 𝑥) · (𝐴 /L 0)) = ((𝐴 /L 𝑀) · (𝐴 /L 0))) |
70 | 69 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝐴 /L 0) = ((𝐴 /L 𝑥) · (𝐴 /L 0)) ↔ (𝐴 /L 0) =
((𝐴 /L
𝑀) · (𝐴 /L
0)))) |
71 | 70 | rspcv 3278 |
. . . . 5
⊢ (𝑀 ∈ ℤ →
(∀𝑥 ∈ ℤ
(𝐴 /L 0)
= ((𝐴 /L
𝑥) · (𝐴 /L 0)) →
(𝐴 /L 0)
= ((𝐴 /L
𝑀) · (𝐴 /L
0)))) |
72 | 67, 41, 71 | sylc 63 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L 0) = ((𝐴 /L 𝑀) · (𝐴 /L 0))) |
73 | 72 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → (𝐴 /L 0) =
((𝐴 /L
𝑀) · (𝐴 /L
0))) |
74 | | oveq2 6557 |
. . . . 5
⊢ (𝑁 = 0 → (𝑀 · 𝑁) = (𝑀 · 0)) |
75 | 67 | zcnd 11359 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ 𝑀 ∈
ℂ) |
76 | 75 | mul01d 10114 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝑀 · 0) =
0) |
77 | 74, 76 | sylan9eqr 2666 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → (𝑀 · 𝑁) = 0) |
78 | 77 | oveq2d 6565 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → (𝐴 /L (𝑀 · 𝑁)) = (𝐴 /L 0)) |
79 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → 𝑁 = 0) |
80 | 79 | oveq2d 6565 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → (𝐴 /L 𝑁) = (𝐴 /L 0)) |
81 | 80 | oveq2d 6565 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 0))) |
82 | 73, 78, 81 | 3eqtr4d 2654 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ 𝑁 = 0) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |
83 | | lgsdi 24859 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |
84 | 19, 83 | syl3anl1 1366 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |
85 | 66, 82, 84 | pm2.61da2ne 2870 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ (𝐴
/L (𝑀
· 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |