Metamath Proof Explorer


Theorem reim0

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 AA=0

Proof

Step Hyp Ref Expression
1 recn AA
2 it0e0 i0=0
3 2 oveq2i A+i0=A+0
4 addid1 AA+0=A
5 3 4 eqtrid AA+i0=A
6 1 5 syl AA+i0=A
7 6 fveq2d AA+i0=A
8 0re 0
9 crim A0A+i0=0
10 8 9 mpan2 AA+i0=0
11 7 10 eqtr3d AA=0