Definition df-rpcxp 13851

Description: Define the power function on complex numbers. Because df-relog 13850 is only defined on positive reals, this definition only allows for a base which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.)

Assertion

Ref	Expression
df-rpcxp	⊢ ↑𝑐 = (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (exp‘(𝑦 · (log‘𝑥))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-rpcxp

Step	Hyp	Ref	Expression
1		ccxp 13849	. 2 class ↑𝑐
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		crp 9624	. . 3 class ℝ+
5		cc 7784	. . 3 class ℂ
6	3	cv 1352	. . . . 5 class 𝑦
7	2	cv 1352	. . . . . 6 class 𝑥
8		clog 13848	. . . . . 6 class log
9	7, 8	cfv 5208	. . . . 5 class (log‘𝑥)
10		cmul 7791	. . . . 5 class ·
11	6, 9, 10	co 5865	. . . 4 class (𝑦 · (log‘𝑥))
12		ce 11618	. . . 4 class exp
13	11, 12	cfv 5208	. . 3 class (exp‘(𝑦 · (log‘𝑥)))
14	2, 3, 4, 5, 13	cmpo 5867	. 2 class (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (exp‘(𝑦 · (log‘𝑥))))
15	1, 14	wceq 1353	1 wff ↑𝑐 = (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (exp‘(𝑦 · (log‘𝑥))))

This definition is referenced by:  rpcxpef  13886