Metamath Proof Explorer

Theorem reim0b

Description: A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005)

Ref Expression
Assertion reim0b 
|- ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )

Proof

Step Hyp Ref Expression
1 reim0 
 |-  ( A e. RR -> ( Im ` A ) = 0 )
2 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
3 2 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) = 0 ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
4 oveq2 
 |-  ( ( Im ` A ) = 0 -> ( _i x. ( Im ` A ) ) = ( _i x. 0 ) )
5 it0e0 
 |-  ( _i x. 0 ) = 0
6 4 5 eqtrdi 
 |-  ( ( Im ` A ) = 0 -> ( _i x. ( Im ` A ) ) = 0 )
7 6 oveq2d 
 |-  ( ( Im ` A ) = 0 -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( ( Re ` A ) + 0 ) )
8 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
9 8 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
10 9 addridd 
 |-  ( A e. CC -> ( ( Re ` A ) + 0 ) = ( Re ` A ) )
11 7 10 sylan9eqr 
 |-  ( ( A e. CC /\ ( Im ` A ) = 0 ) -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( Re ` A ) )
12 3 11 eqtrd 
 |-  ( ( A e. CC /\ ( Im ` A ) = 0 ) -> A = ( Re ` A ) )
13 8 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) = 0 ) -> ( Re ` A ) e. RR )
14 12 13 eqeltrd 
 |-  ( ( A e. CC /\ ( Im ` A ) = 0 ) -> A e. RR )
15 14 ex 
 |-  ( A e. CC -> ( ( Im ` A ) = 0 -> A e. RR ) )
16 1 15 impbid2 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )