Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-cxp | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
df-cxp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccxp 24302 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cc 9934 | . . 3 | |
5 | 2 | cv 1482 | . . . . 5 |
6 | cc0 9936 | . . . . 5 | |
7 | 5, 6 | wceq 1483 | . . . 4 |
8 | 3 | cv 1482 | . . . . . 6 |
9 | 8, 6 | wceq 1483 | . . . . 5 |
10 | c1 9937 | . . . . 5 | |
11 | 9, 10, 6 | cif 4086 | . . . 4 |
12 | clog 24301 | . . . . . . 7 | |
13 | 5, 12 | cfv 5888 | . . . . . 6 |
14 | cmul 9941 | . . . . . 6 | |
15 | 8, 13, 14 | co 6650 | . . . . 5 |
16 | ce 14792 | . . . . 5 | |
17 | 15, 16 | cfv 5888 | . . . 4 |
18 | 7, 11, 17 | cif 4086 | . . 3 |
19 | 2, 3, 4, 4, 18 | cmpt2 6652 | . 2 |
20 | 1, 19 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: cxpval 24410 |
Copyright terms: Public domain | W3C validator |