Theorem cxpcl

Description: Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		cxpval	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^B=if\left(A=0,if\left(B=0,1,0\right),{\mathrm{e}}^{B\log A}\right)$$
2		ax-1cn	$$⊢1\in ℂ$$
3		0cn	$$⊢0\in ℂ$$
4	2 3	ifcli	$$⊢if\left(B=0,1,0\right)\in ℂ$$
5	4	a1i	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge A=0\right)\to if\left(B=0,1,0\right)\in ℂ$$
6		df-ne	$$⊢A\ne 0\leftrightarrow \neg A=0$$
7		id	$$⊢B\in ℂ\to B\in ℂ$$
8		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
9		mulcl	$$⊢\left(B\in ℂ\wedge \log A\in ℂ\right)\to B\log A\in ℂ$$
10	7 8 9	syl2anr	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in ℂ\right)\to B\log A\in ℂ$$
11	10	an32s	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge A\ne 0\right)\to B\log A\in ℂ$$
12		efcl	$$⊢B\log A\in ℂ\to {\mathrm{e}}^{B\log A}\in ℂ$$
13	11 12	syl	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge A\ne 0\right)\to {\mathrm{e}}^{B\log A}\in ℂ$$
14	6 13	sylan2br	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \neg A=0\right)\to {\mathrm{e}}^{B\log A}\in ℂ$$
15	5 14	ifclda	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to if\left(A=0,if\left(B=0,1,0\right),{\mathrm{e}}^{B\log A}\right)\in ℂ$$
16	1 15	eqeltrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^B\in ℂ$$