Metamath Proof Explorer


Theorem cxpne0

Description: Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ≠ 0 )

Proof

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 )