Description: Define the power function on complex numbers. Note that the value of this function when x = 0 and ( Rey ) <_ 0 , y =/= 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-cxp | |- ^c = ( x e. CC , y e. CC |-> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccxp | |- ^c |
|
| 1 | vx | |- x |
|
| 2 | cc | |- CC |
|
| 3 | vy | |- y |
|
| 4 | 1 | cv | |- x |
| 5 | cc0 | |- 0 |
|
| 6 | 4 5 | wceq | |- x = 0 |
| 7 | 3 | cv | |- y |
| 8 | 7 5 | wceq | |- y = 0 |
| 9 | c1 | |- 1 |
|
| 10 | 8 9 5 | cif | |- if ( y = 0 , 1 , 0 ) |
| 11 | ce | |- exp |
|
| 12 | cmul | |- x. |
|
| 13 | clog | |- log |
|
| 14 | 4 13 | cfv | |- ( log ` x ) |
| 15 | 7 14 12 | co | |- ( y x. ( log ` x ) ) |
| 16 | 15 11 | cfv | |- ( exp ` ( y x. ( log ` x ) ) ) |
| 17 | 6 10 16 | cif | |- if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) |
| 18 | 1 3 2 2 17 | cmpo | |- ( x e. CC , y e. CC |-> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) ) |
| 19 | 0 18 | wceq | |- ^c = ( x e. CC , y e. CC |-> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) ) |