Definition df-cxp

Description: Define the power function on complex numbers. Note that the value of this function when x = 0 and ( Rey ) <_ 0 , y =/= 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccxp	$$class{\uparrow }_c$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cc0	$$class0$$
6	4 5	wceq	$$wffx=0$$
7	3	cv	$$setvary$$
8	7 5	wceq	$$wffy=0$$
9		c1	$$class1$$
10	8 9 5	cif	$$classif\left(y=0,1,0\right)$$
11		ce	$$class\exp$$
12		cmul	$$class\times$$
13		clog	$$classlog$$
14	4 13	cfv	$$class\log x$$
15	7 14 12	co	$$classy\log x$$
16	15 11	cfv	$$class{\mathrm{e}}^{y\log x}$$
17	6 10 16	cif	$$classif\left(x=0,if\left(y=0,1,0\right),{\mathrm{e}}^{y\log x}\right)$$
18	1 3 2 2 17	cmpo	$$class\left(x\in ℂ,y\in ℂ⟼if\left(x=0,if\left(y=0,1,0\right),{\mathrm{e}}^{y\log x}\right)\right)$$
19	0 18	wceq	$$wff{\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)$$