Theorem cxpval

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(x=A\wedge y=B\right)\to x=A$$
2	1	eqeq1d	$$⊢\left(x=A\wedge y=B\right)\to \left(x=0\leftrightarrow A=0\right)$$
3		simpr	$$⊢\left(x=A\wedge y=B\right)\to y=B$$
4	3	eqeq1d	$$⊢\left(x=A\wedge y=B\right)\to \left(y=0\leftrightarrow B=0\right)$$
5	4	ifbid	$$⊢\left(x=A\wedge y=B\right)\to if\left(y=0,1,0\right)=if\left(B=0,1,0\right)$$
6	1	fveq2d	$$⊢\left(x=A\wedge y=B\right)\to \log x=\log A$$
7	3 6	oveq12d	$$⊢\left(x=A\wedge y=B\right)\to y\log x=B\log A$$
8	7	fveq2d	$$⊢\left(x=A\wedge y=B\right)\to {\mathrm{e}}^{y\log x}={\mathrm{e}}^{B\log A}$$
9	2 5 8	ifbieq12d	$$⊢\left(x=A\wedge y=B\right)\to if\left(x=0,if\left(y=0,1,0\right),{\mathrm{e}}^{y\log x}\right)=if\left(A=0,if\left(B=0,1,0\right),{\mathrm{e}}^{B\log A}\right)$$
10		df-cxp	$$⊢{\uparrow }_c=\left(x\in ℂ,y\in ℂ⟼if\left(x=0,if\left(y=0,1,0\right),{\mathrm{e}}^{y\log x}\right)\right)$$
11		ax-1cn	$$⊢1\in ℂ$$
12		0cn	$$⊢0\in ℂ$$
13	11 12	ifcli	$$⊢if\left(B=0,1,0\right)\in ℂ$$
14	13	elexi	$$⊢if\left(B=0,1,0\right)\in \mathrm{V}$$
15		fvex	$$⊢{\mathrm{e}}^{B\log A}\in \mathrm{V}$$
16	14 15	ifex	$$⊢if\left(A=0,if\left(B=0,1,0\right),{\mathrm{e}}^{B\log A}\right)\in \mathrm{V}$$
17	9 10 16	ovmpoa	$$⊢\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)$$