Step |
Hyp |
Ref |
Expression |
1 |
|
1z |
⊢ 1 ∈ ℤ |
2 |
|
expaddz |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐴 ↑ 1 ) ) ) |
3 |
1 2
|
mpanr2 |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐴 ↑ 1 ) ) ) |
4 |
3
|
3impa |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐴 ↑ 1 ) ) ) |
5 |
|
exp1 |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 1 ) = 𝐴 ) |
7 |
6
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑁 ) · ( 𝐴 ↑ 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) ) |
8 |
4 7
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) ) |