Definition df-cxp 26058

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 26056	. 2 class ↑𝑐
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 11105	. . 3 class ℂ
5	2	cv 1541	. . . . 5 class 𝑥
6		cc0 11107	. . . . 5 class 0
7	5, 6	wceq 1542	. . . 4 wff 𝑥 = 0
8	3	cv 1541	. . . . . 6 class 𝑦
9	8, 6	wceq 1542	. . . . 5 wff 𝑦 = 0
10		c1 11108	. . . . 5 class 1
11	9, 10, 6	cif 4528	. . . 4 class if(𝑦 = 0, 1, 0)
12		clog 26055	. . . . . . 7 class log
13	5, 12	cfv 6541	. . . . . 6 class (log‘𝑥)
14		cmul 11112	. . . . . 6 class ·
15	8, 13, 14	co 7406	. . . . 5 class (𝑦 · (log‘𝑥))
16		ce 16002	. . . . 5 class exp
17	15, 16	cfv 6541	. . . 4 class (exp‘(𝑦 · (log‘𝑥)))
18	7, 11, 17	cif 4528	. . 3 class if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))
19	2, 3, 4, 4, 18	cmpo 7408	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))
20	1, 19	wceq 1542	1 wff ↑𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))

This definition is referenced by:  cxpval  26164