Definition df-rpcxp 15095

Description: Define the power function on complex numbers. Because df-relog 15094 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	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-rpcxp

Step	Hyp	Ref	Expression
1		ccxp 15093	. 2 class ^c
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		crp 9728	. . 3 class RR+
5		cc 7877	. . 3 class CC
6	3	cv 1363	. . . . 5 class y
7	2	cv 1363	. . . . . 6 class x
8		clog 15092	. . . . . 6 class log
9	7, 8	cfv 5258	. . . . 5 class ( log ` x )
10		cmul 7884	. . . . 5 class x.
11	6, 9, 10	co 5922	. . . 4 class ( y x. ( log ` x ) )
12		ce 11807	. . . 4 class exp
13	11, 12	cfv 5258	. . 3 class ( exp ` ( y x. ( log ` x ) ) )
14	2, 3, 4, 5, 13	cmpo 5924	. 2 class ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
15	1, 14	wceq 1364	1 wff ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )

This definition is referenced by:  rpcxpef  15130