Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cxp Structured version   Unicode version

Definition df-cxp 20457
 Description: Define the power function on complex numbers. Note that the value of this function when and 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-cxp
StepHypRef Expression
1 ccxp 20455 . 2
2 vx . . 3
3 vy . . 3
4 cc 8990 . . 3
52cv 1652 . . . . 5
6 cc0 8992 . . . . 5
75, 6wceq 1653 . . . 4
83cv 1652 . . . . . 6
98, 6wceq 1653 . . . . 5
10 c1 8993 . . . . 5
119, 10, 6cif 3741 . . . 4
12 clog 20454 . . . . . . 7
135, 12cfv 5456 . . . . . 6
14 cmul 8997 . . . . . 6
158, 13, 14co 6083 . . . . 5
16 ce 12666 . . . . 5
1715, 16cfv 5456 . . . 4
187, 11, 17cif 3741 . . 3
192, 3, 4, 4, 18cmpt2 6085 . 2
201, 19wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  cxpval  20557
 Copyright terms: Public domain W3C validator