Step |
Hyp |
Ref |
Expression |
1 |
|
cxpef |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) |
2 |
|
id |
⊢ ( 𝐵 ∈ ℂ → 𝐵 ∈ ℂ ) |
3 |
|
logcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ ) |
4 |
|
mulcl |
⊢ ( ( 𝐵 ∈ ℂ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ ) |
5 |
2 3 4
|
syl2anr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ ) |
6 |
5
|
3impa |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ ) |
7 |
|
efne0 |
⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ≠ 0 ) |
8 |
6 7
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ≠ 0 ) |
9 |
1 8
|
eqnetrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ≠ 0 ) |