Step |
Hyp |
Ref |
Expression |
1 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
2 |
|
cxpadd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 1 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 1 ) ) ) |
3 |
1 2
|
mp3an3 |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 1 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 1 ) ) ) |
4 |
3
|
3impa |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 1 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 1 ) ) ) |
5 |
|
cxp1 |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 1 ) = 𝐴 ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 1 ) = 𝐴 ) |
7 |
6
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 1 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · 𝐴 ) ) |
8 |
4 7
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + 1 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · 𝐴 ) ) |