| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 0 → (𝑀 · 𝑗) = (𝑀 · 0)) | 
| 2 | 1 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = 0 → (𝐴↑(𝑀 · 𝑗)) = (𝐴↑(𝑀 · 0))) | 
| 3 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 0 → ((𝐴↑𝑀)↑𝑗) = ((𝐴↑𝑀)↑0)) | 
| 4 | 2, 3 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = 0 → ((𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗) ↔ (𝐴↑(𝑀 · 0)) = ((𝐴↑𝑀)↑0))) | 
| 5 | 4 | imbi2d 340 | . . . 4
⊢ (𝑗 = 0 → (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗)) ↔ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 0)) = ((𝐴↑𝑀)↑0)))) | 
| 6 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑀 · 𝑗) = (𝑀 · 𝑘)) | 
| 7 | 6 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = 𝑘 → (𝐴↑(𝑀 · 𝑗)) = (𝐴↑(𝑀 · 𝑘))) | 
| 8 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑀)↑𝑗) = ((𝐴↑𝑀)↑𝑘)) | 
| 9 | 7, 8 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = 𝑘 → ((𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗) ↔ (𝐴↑(𝑀 · 𝑘)) = ((𝐴↑𝑀)↑𝑘))) | 
| 10 | 9 | imbi2d 340 | . . . 4
⊢ (𝑗 = 𝑘 → (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗)) ↔ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑘)) = ((𝐴↑𝑀)↑𝑘)))) | 
| 11 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑀 · 𝑗) = (𝑀 · (𝑘 + 1))) | 
| 12 | 11 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑(𝑀 · 𝑗)) = (𝐴↑(𝑀 · (𝑘 + 1)))) | 
| 13 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑀)↑𝑗) = ((𝐴↑𝑀)↑(𝑘 + 1))) | 
| 14 | 12, 13 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗) ↔ (𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑𝑀)↑(𝑘 + 1)))) | 
| 15 | 14 | imbi2d 340 | . . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗)) ↔ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑𝑀)↑(𝑘 + 1))))) | 
| 16 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑀 · 𝑗) = (𝑀 · 𝑁)) | 
| 17 | 16 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝐴↑(𝑀 · 𝑗)) = (𝐴↑(𝑀 · 𝑁))) | 
| 18 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑀)↑𝑗) = ((𝐴↑𝑀)↑𝑁)) | 
| 19 | 17, 18 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = 𝑁 → ((𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗) ↔ (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁))) | 
| 20 | 19 | imbi2d 340 | . . . 4
⊢ (𝑗 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑗)) = ((𝐴↑𝑀)↑𝑗)) ↔ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)))) | 
| 21 |  | nn0cn 12538 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) | 
| 22 | 21 | mul01d 11461 | . . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 · 0) =
0) | 
| 23 | 22 | oveq2d 7448 | . . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝐴↑(𝑀 · 0)) = (𝐴↑0)) | 
| 24 |  | exp0 14107 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) | 
| 25 | 23, 24 | sylan9eqr 2798 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑(𝑀 · 0)) =
1) | 
| 26 |  | expcl 14121 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑𝑀) ∈
ℂ) | 
| 27 |  | exp0 14107 | . . . . . 6
⊢ ((𝐴↑𝑀) ∈ ℂ → ((𝐴↑𝑀)↑0) = 1) | 
| 28 | 26, 27 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ ((𝐴↑𝑀)↑0) = 1) | 
| 29 | 25, 28 | eqtr4d 2779 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑(𝑀 · 0)) = ((𝐴↑𝑀)↑0)) | 
| 30 |  | oveq1 7439 | . . . . . . 7
⊢ ((𝐴↑(𝑀 · 𝑘)) = ((𝐴↑𝑀)↑𝑘) → ((𝐴↑(𝑀 · 𝑘)) · (𝐴↑𝑀)) = (((𝐴↑𝑀)↑𝑘) · (𝐴↑𝑀))) | 
| 31 |  | nn0cn 12538 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 32 |  | ax-1cn 11214 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ | 
| 33 |  | adddi 11245 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 ·
(𝑘 + 1)) = ((𝑀 · 𝑘) + (𝑀 · 1))) | 
| 34 | 32, 33 | mp3an3 1451 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + (𝑀 · 1))) | 
| 35 |  | mulrid 11260 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℂ → (𝑀 · 1) = 𝑀) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 · 1) = 𝑀) | 
| 37 | 36 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑀 · 𝑘) + (𝑀 · 1)) = ((𝑀 · 𝑘) + 𝑀)) | 
| 38 | 34, 37 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + 𝑀)) | 
| 39 | 21, 31, 38 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + 𝑀)) | 
| 40 | 39 | adantll 714 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (𝑀 · (𝑘 + 1)) = ((𝑀 · 𝑘) + 𝑀)) | 
| 41 | 40 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (𝐴↑(𝑀 · (𝑘 + 1))) = (𝐴↑((𝑀 · 𝑘) + 𝑀))) | 
| 42 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → 𝐴 ∈ ℂ) | 
| 43 |  | nn0mulcl 12564 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 · 𝑘) ∈
ℕ0) | 
| 44 | 43 | adantll 714 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (𝑀 · 𝑘) ∈
ℕ0) | 
| 45 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → 𝑀 ∈
ℕ0) | 
| 46 |  | expadd 14146 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 · 𝑘) ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑((𝑀 · 𝑘) + 𝑀)) = ((𝐴↑(𝑀 · 𝑘)) · (𝐴↑𝑀))) | 
| 47 | 42, 44, 45, 46 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (𝐴↑((𝑀 · 𝑘) + 𝑀)) = ((𝐴↑(𝑀 · 𝑘)) · (𝐴↑𝑀))) | 
| 48 | 41, 47 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑(𝑀 · 𝑘)) · (𝐴↑𝑀))) | 
| 49 |  | expp1 14110 | . . . . . . . . 9
⊢ (((𝐴↑𝑀) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴↑𝑀)↑(𝑘 + 1)) = (((𝐴↑𝑀)↑𝑘) · (𝐴↑𝑀))) | 
| 50 | 26, 49 | sylan 580 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → ((𝐴↑𝑀)↑(𝑘 + 1)) = (((𝐴↑𝑀)↑𝑘) · (𝐴↑𝑀))) | 
| 51 | 48, 50 | eqeq12d 2752 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → ((𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑𝑀)↑(𝑘 + 1)) ↔ ((𝐴↑(𝑀 · 𝑘)) · (𝐴↑𝑀)) = (((𝐴↑𝑀)↑𝑘) · (𝐴↑𝑀)))) | 
| 52 | 30, 51 | imbitrrid 246 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → ((𝐴↑(𝑀 · 𝑘)) = ((𝐴↑𝑀)↑𝑘) → (𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑𝑀)↑(𝑘 + 1)))) | 
| 53 | 52 | expcom 413 | . . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝑀 ∈
ℕ0) → ((𝐴↑(𝑀 · 𝑘)) = ((𝐴↑𝑀)↑𝑘) → (𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑𝑀)↑(𝑘 + 1))))) | 
| 54 | 53 | a2d 29 | . . . 4
⊢ (𝑘 ∈ ℕ0
→ (((𝐴 ∈ ℂ
∧ 𝑀 ∈
ℕ0) → (𝐴↑(𝑀 · 𝑘)) = ((𝐴↑𝑀)↑𝑘)) → ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝐴↑(𝑀 · (𝑘 + 1))) = ((𝐴↑𝑀)↑(𝑘 + 1))))) | 
| 55 | 5, 10, 15, 20, 29, 54 | nn0ind 12715 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝑀 ∈
ℕ0) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁))) | 
| 56 | 55 | expdcom 414 | . 2
⊢ (𝐴 ∈ ℂ → (𝑀 ∈ ℕ0
→ (𝑁 ∈
ℕ0 → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)))) | 
| 57 | 56 | 3imp 1110 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)) |