This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )