Theorem cxpne0

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

	Ref	Expression
Assertion	cxpne0	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		cxpef	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B={\mathrm{e}}^{B\log A}$$
2		id	$$⊢B\in ℂ\to B\in ℂ$$
3		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
4		mulcl	$$⊢\left(B\in ℂ\wedge \log A\in ℂ\right)\to B\log A\in ℂ$$
5	2 3 4	syl2anr	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in ℂ\right)\to B\log A\in ℂ$$
6	5	3impa	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to B\log A\in ℂ$$
7		efne0	$$⊢B\log A\in ℂ\to {\mathrm{e}}^{B\log A}\ne 0$$
8	6 7	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to {\mathrm{e}}^{B\log A}\ne 0$$
9	1 8	eqnetrd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B\ne 0$$