| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 0 → ((𝐴 · 𝐵)↑𝑗) = ((𝐴 · 𝐵)↑0)) | 
| 2 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 0 → (𝐴↑𝑗) = (𝐴↑0)) | 
| 3 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 0 → (𝐵↑𝑗) = (𝐵↑0)) | 
| 4 | 2, 3 | oveq12d 7450 | . . . . . 6
⊢ (𝑗 = 0 → ((𝐴↑𝑗) · (𝐵↑𝑗)) = ((𝐴↑0) · (𝐵↑0))) | 
| 5 | 1, 4 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = 0 → (((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗)) ↔ ((𝐴 · 𝐵)↑0) = ((𝐴↑0) · (𝐵↑0)))) | 
| 6 | 5 | imbi2d 340 | . . . 4
⊢ (𝑗 = 0 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑0) = ((𝐴↑0) · (𝐵↑0))))) | 
| 7 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝐴 · 𝐵)↑𝑗) = ((𝐴 · 𝐵)↑𝑘)) | 
| 8 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) | 
| 9 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐵↑𝑗) = (𝐵↑𝑘)) | 
| 10 | 8, 9 | oveq12d 7450 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) · (𝐵↑𝑗)) = ((𝐴↑𝑘) · (𝐵↑𝑘))) | 
| 11 | 7, 10 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = 𝑘 → (((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗)) ↔ ((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘)))) | 
| 12 | 11 | imbi2d 340 | . . . 4
⊢ (𝑗 = 𝑘 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘))))) | 
| 13 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝐴 · 𝐵)↑𝑗) = ((𝐴 · 𝐵)↑(𝑘 + 1))) | 
| 14 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) | 
| 15 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝐵↑𝑗) = (𝐵↑(𝑘 + 1))) | 
| 16 | 14, 15 | oveq12d 7450 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) · (𝐵↑𝑗)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))) | 
| 17 | 13, 16 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → (((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗)) ↔ ((𝐴 · 𝐵)↑(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1))))) | 
| 18 | 17 | imbi2d 340 | . . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))))) | 
| 19 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 𝑁 → ((𝐴 · 𝐵)↑𝑗) = ((𝐴 · 𝐵)↑𝑁)) | 
| 20 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) | 
| 21 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝐵↑𝑗) = (𝐵↑𝑁)) | 
| 22 | 20, 21 | oveq12d 7450 | . . . . . 6
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) · (𝐵↑𝑗)) = ((𝐴↑𝑁) · (𝐵↑𝑁))) | 
| 23 | 19, 22 | eqeq12d 2752 | . . . . 5
⊢ (𝑗 = 𝑁 → (((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗)) ↔ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))) | 
| 24 | 23 | imbi2d 340 | . . . 4
⊢ (𝑗 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑗) = ((𝐴↑𝑗) · (𝐵↑𝑗))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))))) | 
| 25 |  | mulcl 11240 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | 
| 26 |  | exp0 14107 | . . . . . 6
⊢ ((𝐴 · 𝐵) ∈ ℂ → ((𝐴 · 𝐵)↑0) = 1) | 
| 27 | 25, 26 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑0) = 1) | 
| 28 |  | exp0 14107 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) | 
| 29 |  | exp0 14107 | . . . . . . 7
⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1) | 
| 30 | 28, 29 | oveqan12d 7451 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑0)) = (1 ·
1)) | 
| 31 |  | 1t1e1 12429 | . . . . . 6
⊢ (1
· 1) = 1 | 
| 32 | 30, 31 | eqtrdi 2792 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑0)) = 1) | 
| 33 | 27, 32 | eqtr4d 2779 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑0) = ((𝐴↑0) · (𝐵↑0))) | 
| 34 |  | expp1 14110 | . . . . . . . . . 10
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = (((𝐴 · 𝐵)↑𝑘) · (𝐴 · 𝐵))) | 
| 35 | 25, 34 | sylan 580 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑(𝑘 + 1)) = (((𝐴 · 𝐵)↑𝑘) · (𝐴 · 𝐵))) | 
| 36 | 35 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
∧ ((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘))) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = (((𝐴 · 𝐵)↑𝑘) · (𝐴 · 𝐵))) | 
| 37 |  | oveq1 7439 | . . . . . . . . 9
⊢ (((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘)) → (((𝐴 · 𝐵)↑𝑘) · (𝐴 · 𝐵)) = (((𝐴↑𝑘) · (𝐵↑𝑘)) · (𝐴 · 𝐵))) | 
| 38 |  | expcl 14121 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) | 
| 39 |  | expcl 14121 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑𝑘) ∈
ℂ) | 
| 40 | 38, 39 | anim12i 613 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (𝐵 ∈ ℂ
∧ 𝑘 ∈
ℕ0)) → ((𝐴↑𝑘) ∈ ℂ ∧ (𝐵↑𝑘) ∈ ℂ)) | 
| 41 | 40 | anandirs 679 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑𝑘) ∈ ℂ ∧ (𝐵↑𝑘) ∈ ℂ)) | 
| 42 |  | simpl 482 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ (𝐴 ∈ ℂ
∧ 𝐵 ∈
ℂ)) | 
| 43 |  | mul4 11430 | . . . . . . . . . . 11
⊢ ((((𝐴↑𝑘) ∈ ℂ ∧ (𝐵↑𝑘) ∈ ℂ) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → (((𝐴↑𝑘) · (𝐵↑𝑘)) · (𝐴 · 𝐵)) = (((𝐴↑𝑘) · 𝐴) · ((𝐵↑𝑘) · 𝐵))) | 
| 44 | 41, 42, 43 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ (((𝐴↑𝑘) · (𝐵↑𝑘)) · (𝐴 · 𝐵)) = (((𝐴↑𝑘) · 𝐴) · ((𝐵↑𝑘) · 𝐵))) | 
| 45 |  | expp1 14110 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) | 
| 46 | 45 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) | 
| 47 |  | expp1 14110 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) | 
| 48 | 47 | adantll 714 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) | 
| 49 | 46, 48 | oveq12d 7450 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1))) = (((𝐴↑𝑘) · 𝐴) · ((𝐵↑𝑘) · 𝐵))) | 
| 50 | 44, 49 | eqtr4d 2779 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
→ (((𝐴↑𝑘) · (𝐵↑𝑘)) · (𝐴 · 𝐵)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))) | 
| 51 | 37, 50 | sylan9eqr 2798 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
∧ ((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘))) → (((𝐴 · 𝐵)↑𝑘) · (𝐴 · 𝐵)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))) | 
| 52 | 36, 51 | eqtrd 2776 | . . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑘 ∈ ℕ0)
∧ ((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘))) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))) | 
| 53 | 52 | exp31 419 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ ℕ0
→ (((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘)) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))))) | 
| 54 | 53 | com12 32 | . . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ (((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘)) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))))) | 
| 55 | 54 | a2d 29 | . . . 4
⊢ (𝑘 ∈ ℕ0
→ (((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐴 · 𝐵)↑𝑘) = ((𝐴↑𝑘) · (𝐵↑𝑘))) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) · (𝐵↑(𝑘 + 1)))))) | 
| 56 | 6, 12, 18, 24, 33, 55 | nn0ind 12715 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))) | 
| 57 | 56 | expdcom 414 | . 2
⊢ (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → (𝑁 ∈ ℕ0
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))))) | 
| 58 | 57 | 3imp 1110 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |