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 addid1d
 |-  ( 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 ) )