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

Definition df-cxp 19915
 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 19913 . 2
2 vx . . 3
3 vy . . 3
4 cc 8735 . . 3
52cv 1622 . . . . 5
6 cc0 8737 . . . . 5
75, 6wceq 1623 . . . 4
83cv 1622 . . . . . 6
98, 6wceq 1623 . . . . 5
10 c1 8738 . . . . 5
119, 10, 6cif 3565 . . . 4
12 clog 19912 . . . . . . 7
135, 12cfv 5255 . . . . . 6
14 cmul 8742 . . . . . 6
158, 13, 14co 5858 . . . . 5
16 ce 12343 . . . . 5
1715, 16cfv 5255 . . . 4
187, 11, 17cif 3565 . . 3
192, 3, 4, 4, 18cmpt2 5860 . 2
201, 19wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  cxpval  20011
 Copyright terms: Public domain W3C validator