MPE Home 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  x  =  0 and  ( Re `  y )  <_  0 ,  y  =/=  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  |-  ^ c  =  ( x  e.  CC ,  y  e.  CC  |->  if ( x  =  0 ,  if ( y  =  0 ,  1 ,  0 ) ,  ( exp `  ( y  x.  ( log `  x ) ) ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-cxp
StepHypRef Expression
1 ccxp 19913 . 2  class  ^ c
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cc 8735 . . 3  class  CC
52cv 1622 . . . . 5  class  x
6 cc0 8737 . . . . 5  class  0
75, 6wceq 1623 . . . 4  wff  x  =  0
83cv 1622 . . . . . 6  class  y
98, 6wceq 1623 . . . . 5  wff  y  =  0
10 c1 8738 . . . . 5  class  1
119, 10, 6cif 3565 . . . 4  class  if ( y  =  0 ,  1 ,  0 )
12 clog 19912 . . . . . . 7  class  log
135, 12cfv 5255 . . . . . 6  class  ( log `  x )
14 cmul 8742 . . . . . 6  class  x.
158, 13, 14co 5858 . . . . 5  class  ( y  x.  ( log `  x
) )
16 ce 12343 . . . . 5  class  exp
1715, 16cfv 5255 . . . 4  class  ( exp `  ( y  x.  ( log `  x ) ) )
187, 11, 17cif 3565 . . 3  class  if ( x  =  0 ,  if ( y  =  0 ,  1 ,  0 ) ,  ( exp `  ( y  x.  ( log `  x
) ) ) )
192, 3, 4, 4, 18cmpt2 5860 . 2  class  ( x  e.  CC ,  y  e.  CC  |->  if ( x  =  0 ,  if ( y  =  0 ,  1 ,  0 ) ,  ( exp `  ( y  x.  ( log `  x
) ) ) ) )
201, 19wceq 1623 1  wff  ^ c  =  ( x  e.  CC ,  y  e.  CC  |->  if ( x  =  0 ,  if ( y  =  0 ,  1 ,  0 ) ,  ( exp `  ( y  x.  ( log `  x ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  cxpval  20011
  Copyright terms: Public domain W3C validator