Step | Hyp | Ref
| Expression |
1 | | oveq2 5463 |
. . . . . . 7
⊢ (𝑗 = 0 → (𝑀 · 𝑗) = (𝑀 · 0)) |
2 | 1 | oveq2d 5471 |
. . . . . 6
⊢ (𝑗 = 0 → (A↑(𝑀 · 𝑗)) = (A↑(𝑀 · 0))) |
3 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = 0 → ((A↑𝑀)↑𝑗) = ((A↑𝑀)↑0)) |
4 | 2, 3 | eqeq12d 2051 |
. . . . 5
⊢ (𝑗 = 0 → ((A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗) ↔ (A↑(𝑀 · 0)) = ((A↑𝑀)↑0))) |
5 | 4 | imbi2d 219 |
. . . 4
⊢ (𝑗 = 0 → (((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗)) ↔ ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 0)) = ((A↑𝑀)↑0)))) |
6 | | oveq2 5463 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑀 · 𝑗) = (𝑀 · 𝑘)) |
7 | 6 | oveq2d 5471 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (A↑(𝑀 · 𝑗)) = (A↑(𝑀 · 𝑘))) |
8 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((A↑𝑀)↑𝑗) = ((A↑𝑀)↑𝑘)) |
9 | 7, 8 | eqeq12d 2051 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗) ↔ (A↑(𝑀 · 𝑘)) = ((A↑𝑀)↑𝑘))) |
10 | 9 | imbi2d 219 |
. . . 4
⊢ (𝑗 = 𝑘 → (((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗)) ↔ ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑘)) = ((A↑𝑀)↑𝑘)))) |
11 | | oveq2 5463 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑀 · 𝑗) = (𝑀 · (𝑘 + 1))) |
12 | 11 | oveq2d 5471 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (A↑(𝑀 · 𝑗)) = (A↑(𝑀 · (𝑘 + 1)))) |
13 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((A↑𝑀)↑𝑗) = ((A↑𝑀)↑(𝑘 + 1))) |
14 | 12, 13 | eqeq12d 2051 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗) ↔ (A↑(𝑀 · (𝑘 + 1))) = ((A↑𝑀)↑(𝑘 + 1)))) |
15 | 14 | imbi2d 219 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗)) ↔ ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · (𝑘 + 1))) = ((A↑𝑀)↑(𝑘 + 1))))) |
16 | | oveq2 5463 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑀 · 𝑗) = (𝑀 · 𝑁)) |
17 | 16 | oveq2d 5471 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (A↑(𝑀 · 𝑗)) = (A↑(𝑀 · 𝑁))) |
18 | | oveq2 5463 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((A↑𝑀)↑𝑗) = ((A↑𝑀)↑𝑁)) |
19 | 17, 18 | eqeq12d 2051 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗) ↔ (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁))) |
20 | 19 | imbi2d 219 |
. . . 4
⊢ (𝑗 = 𝑁 → (((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑗)) = ((A↑𝑀)↑𝑗)) ↔ ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁)))) |
21 | | nn0cn 7967 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈
ℂ) |
22 | 21 | mul01d 7186 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0 → (𝑀 · 0) = 0) |
23 | 22 | oveq2d 5471 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0 → (A↑(𝑀 · 0)) = (A↑0)) |
24 | | exp0 8913 |
. . . . . 6
⊢ (A ∈ ℂ →
(A↑0) = 1) |
25 | 23, 24 | sylan9eqr 2091 |
. . . . 5
⊢
((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (A↑(𝑀 · 0)) = 1) |
26 | | expcl 8927 |
. . . . . 6
⊢
((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (A↑𝑀) ∈
ℂ) |
27 | | exp0 8913 |
. . . . . 6
⊢
((A↑𝑀) ∈
ℂ → ((A↑𝑀)↑0) = 1) |
28 | 26, 27 | syl 14 |
. . . . 5
⊢
((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) → ((A↑𝑀)↑0) = 1) |
29 | 25, 28 | eqtr4d 2072 |
. . . 4
⊢
((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (A↑(𝑀 · 0)) = ((A↑𝑀)↑0)) |
30 | | oveq1 5462 |
. . . . . . 7
⊢
((A↑(𝑀 · 𝑘)) = ((A↑𝑀)↑𝑘) → ((A↑(𝑀 · 𝑘)) · (A↑𝑀)) = (((A↑𝑀)↑𝑘) · (A↑𝑀))) |
31 | | nn0cn 7967 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈
ℂ) |
32 | | ax-1cn 6776 |
. . . . . . . . . . . . . 14
⊢ 1 ∈ ℂ |
33 | | adddi 6811 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1
∈ ℂ) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + (𝑀 · 1))) |
34 | 32, 33 | mp3an3 1220 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + (𝑀 · 1))) |
35 | | mulid1 6822 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℂ → (𝑀 · 1) = 𝑀) |
36 | 35 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 · 1) = 𝑀) |
37 | 36 | oveq2d 5471 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑀 · 𝑘) + (𝑀 · 1)) = ((𝑀 · 𝑘) + 𝑀)) |
38 | 34, 37 | eqtrd 2069 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + 𝑀)) |
39 | 21, 31, 38 | syl2an 273 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘
∈ ℕ0) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + 𝑀)) |
40 | 39 | adantll 445 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + 𝑀)) |
41 | 40 | oveq2d 5471 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → (A↑(𝑀 · (𝑘 + 1))) = (A↑((𝑀 · 𝑘) + 𝑀))) |
42 | | simpll 481 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → A ∈
ℂ) |
43 | | nn0mulcl 7994 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘
∈ ℕ0) → (𝑀 · 𝑘) ∈
ℕ0) |
44 | 43 | adantll 445 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → (𝑀 · 𝑘) ∈
ℕ0) |
45 | | simplr 482 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → 𝑀 ∈ ℕ0) |
46 | | expadd 8951 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧ (𝑀 · 𝑘) ∈
ℕ0 ∧ 𝑀 ∈
ℕ0) → (A↑((𝑀 · 𝑘) + 𝑀)) = ((A↑(𝑀 · 𝑘)) · (A↑𝑀))) |
47 | 42, 44, 45, 46 | syl3anc 1134 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → (A↑((𝑀 · 𝑘) + 𝑀)) = ((A↑(𝑀 · 𝑘)) · (A↑𝑀))) |
48 | 41, 47 | eqtrd 2069 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → (A↑(𝑀 · (𝑘 + 1))) = ((A↑(𝑀 · 𝑘)) · (A↑𝑀))) |
49 | | expp1 8916 |
. . . . . . . . 9
⊢
(((A↑𝑀) ∈
ℂ ∧ 𝑘 ∈
ℕ0) → ((A↑𝑀)↑(𝑘 + 1)) = (((A↑𝑀)↑𝑘) · (A↑𝑀))) |
50 | 26, 49 | sylan 267 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → ((A↑𝑀)↑(𝑘 + 1)) = (((A↑𝑀)↑𝑘) · (A↑𝑀))) |
51 | 48, 50 | eqeq12d 2051 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → ((A↑(𝑀 · (𝑘 + 1))) = ((A↑𝑀)↑(𝑘 + 1)) ↔ ((A↑(𝑀 · 𝑘)) · (A↑𝑀)) = (((A↑𝑀)↑𝑘) · (A↑𝑀)))) |
52 | 30, 51 | syl5ibr 145 |
. . . . . 6
⊢
(((A ∈ ℂ ∧ 𝑀 ∈ ℕ0) ∧ 𝑘
∈ ℕ0) → ((A↑(𝑀 · 𝑘)) = ((A↑𝑀)↑𝑘) → (A↑(𝑀 · (𝑘 + 1))) = ((A↑𝑀)↑(𝑘 + 1)))) |
53 | 52 | expcom 109 |
. . . . 5
⊢ (𝑘 ∈ ℕ0 → ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → ((A↑(𝑀 · 𝑘)) = ((A↑𝑀)↑𝑘) → (A↑(𝑀 · (𝑘 + 1))) = ((A↑𝑀)↑(𝑘 + 1))))) |
54 | 53 | a2d 23 |
. . . 4
⊢ (𝑘 ∈ ℕ0 → (((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑘)) = ((A↑𝑀)↑𝑘)) → ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · (𝑘 + 1))) = ((A↑𝑀)↑(𝑘 + 1))))) |
55 | 5, 10, 15, 20, 29, 54 | nn0ind 8128 |
. . 3
⊢ (𝑁 ∈ ℕ0 → ((A ∈ ℂ ∧ 𝑀 ∈
ℕ0) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁))) |
56 | 55 | expdcom 1328 |
. 2
⊢ (A ∈ ℂ →
(𝑀 ∈ ℕ0 → (𝑁 ∈
ℕ0 → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁)))) |
57 | 56 | 3imp 1097 |
1
⊢
((A ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁)) |