Description: The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | reim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-icn | |
|
2 | mulcl | |
|
3 | 1 2 | mpan | |
4 | imval | |
|
5 | 3 4 | syl | |
6 | ine0 | |
|
7 | divcan3 | |
|
8 | 1 6 7 | mp3an23 | |
9 | 8 | fveq2d | |
10 | 5 9 | eqtr2d | |