Definition df-cxp 25143

Description: Define the power function on complex numbers. Note that the value of this function when 𝑥 = 0 and (ℜ‘𝑦) ≤ 0, 𝑦 ≠ 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014.)

Assertion

Ref	Expression
df-cxp	⊢ ↑𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-cxp

Step	Hyp	Ref	Expression
1		ccxp 25141	. 2 class ↑𝑐
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 10537	. . 3 class ℂ
5	2	cv 1536	. . . . 5 class 𝑥
6		cc0 10539	. . . . 5 class 0
7	5, 6	wceq 1537	. . . 4 wff 𝑥 = 0
8	3	cv 1536	. . . . . 6 class 𝑦
9	8, 6	wceq 1537	. . . . 5 wff 𝑦 = 0
10		c1 10540	. . . . 5 class 1
11	9, 10, 6	cif 4469	. . . 4 class if(𝑦 = 0, 1, 0)
12		clog 25140	. . . . . . 7 class log
13	5, 12	cfv 6357	. . . . . 6 class (log‘𝑥)
14		cmul 10544	. . . . . 6 class ·
15	8, 13, 14	co 7158	. . . . 5 class (𝑦 · (log‘𝑥))
16		ce 15417	. . . . 5 class exp
17	15, 16	cfv 6357	. . . 4 class (exp‘(𝑦 · (log‘𝑥)))
18	7, 11, 17	cif 4469	. . 3 class if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))
19	2, 3, 4, 4, 18	cmpo 7160	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))
20	1, 19	wceq 1537	1 wff ↑𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))

This definition is referenced by:  cxpval  25249