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	⊢ ↑𝑐 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccxp	⊢ ↑𝑐
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		cc0	⊢ 0
6	4 5	wceq	⊢ 𝑥 = 0
7	3	cv	⊢ 𝑦
8	7 5	wceq	⊢ 𝑦 = 0
9		c1	⊢ 1
10	8 9 5	cif	⊢ if ( 𝑦 = 0 , 1 , 0 )
11		ce	⊢ exp
12		cmul	⊢ ·
13		clog	⊢ log
14	4 13	cfv	⊢ ( log ‘ 𝑥 )
15	7 14 12	co	⊢ ( 𝑦 · ( log ‘ 𝑥 ) )
16	15 11	cfv	⊢ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) )
17	6 10 16	cif	⊢ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) )
18	1 3 2 2 17	cmpo	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )
19	0 18	wceq	⊢ ↑𝑐 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )