Metamath Proof Explorer
Description: Define the natural logarithm function on complex numbers. It is defined
as the principal value, that is, the inverse of the exponential whose
imaginary part lies in the interval (-pi, pi]. See
http://en.wikipedia.org/wiki/Natural_logarithm and
https://en.wikipedia.org/wiki/Complex_logarithm . (Contributed by Paul
Chapman, 21-Apr-2008)
|
|
Ref |
Expression |
|
Assertion |
df-log |
⊢ log = ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) |
Detailed syntax breakdown
| Step |
Hyp |
Ref |
Expression |
| 0 |
|
clog |
⊢ log |
| 1 |
|
ce |
⊢ exp |
| 2 |
|
cim |
⊢ ℑ |
| 3 |
2
|
ccnv |
⊢ ◡ ℑ |
| 4 |
|
cpi |
⊢ π |
| 5 |
4
|
cneg |
⊢ - π |
| 6 |
|
cioc |
⊢ (,] |
| 7 |
5 4 6
|
co |
⊢ ( - π (,] π ) |
| 8 |
3 7
|
cima |
⊢ ( ◡ ℑ “ ( - π (,] π ) ) |
| 9 |
1 8
|
cres |
⊢ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) |
| 10 |
9
|
ccnv |
⊢ ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) |
| 11 |
0 10
|
wceq |
⊢ log = ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) |