This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( A e. RR -> ( Im ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 it0e0 
 |-  ( _i x. 0 ) = 0
3 2 oveq2i 
 |-  ( A + ( _i x. 0 ) ) = ( A + 0 )
4 addrid 
 |-  ( A e. CC -> ( A + 0 ) = A )
5 3 4 eqtrid 
 |-  ( A e. CC -> ( A + ( _i x. 0 ) ) = A )
6 1 5 syl 
 |-  ( A e. RR -> ( A + ( _i x. 0 ) ) = A )
7 6 fveq2d 
 |-  ( A e. RR -> ( Im ` ( A + ( _i x. 0 ) ) ) = ( Im ` A ) )
8 0re 
 |-  0 e. RR
9 crim 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( Im ` ( A + ( _i x. 0 ) ) ) = 0 )
10 8 9 mpan2 
 |-  ( A e. RR -> ( Im ` ( A + ( _i x. 0 ) ) ) = 0 )
11 7 10 eqtr3d 
 |-  ( A e. RR -> ( Im ` A ) = 0 )