Description: The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 7-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | reim0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn | |
|
2 | it0e0 | |
|
3 | 2 | oveq2i | |
4 | addid1 | |
|
5 | 3 4 | eqtrid | |
6 | 1 5 | syl | |
7 | 6 | fveq2d | |
8 | 0re | |
|
9 | crim | |
|
10 | 8 9 | mpan2 | |
11 | 7 10 | eqtr3d | |