Metamath Proof Explorer


Theorem rereb

Description: A number is real iff it equals its real part. Proposition 10-3.4(f) of Gleason p. 133. (Contributed by NM, 20-Aug-2008)

Ref Expression
Assertion rereb
|- ( A e. CC -> ( A e. RR <-> ( Re ` A ) = A ) )

Proof

Step Hyp Ref Expression
1 replim
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
2 1 adantr
 |-  ( ( A e. CC /\ A e. RR ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
3 reim0
 |-  ( A e. RR -> ( Im ` A ) = 0 )
4 3 oveq2d
 |-  ( A e. RR -> ( _i x. ( Im ` A ) ) = ( _i x. 0 ) )
5 it0e0
 |-  ( _i x. 0 ) = 0
6 4 5 eqtrdi
 |-  ( A e. RR -> ( _i x. ( Im ` A ) ) = 0 )
7 6 adantl
 |-  ( ( A e. CC /\ A e. RR ) -> ( _i x. ( Im ` A ) ) = 0 )
8 7 oveq2d
 |-  ( ( A e. CC /\ A e. RR ) -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( ( Re ` A ) + 0 ) )
9 recl
 |-  ( A e. CC -> ( Re ` A ) e. RR )
10 9 recnd
 |-  ( A e. CC -> ( Re ` A ) e. CC )
11 10 addid1d
 |-  ( A e. CC -> ( ( Re ` A ) + 0 ) = ( Re ` A ) )
12 11 adantr
 |-  ( ( A e. CC /\ A e. RR ) -> ( ( Re ` A ) + 0 ) = ( Re ` A ) )
13 2 8 12 3eqtrrd
 |-  ( ( A e. CC /\ A e. RR ) -> ( Re ` A ) = A )
14 simpr
 |-  ( ( A e. CC /\ ( Re ` A ) = A ) -> ( Re ` A ) = A )
15 9 adantr
 |-  ( ( A e. CC /\ ( Re ` A ) = A ) -> ( Re ` A ) e. RR )
16 14 15 eqeltrrd
 |-  ( ( A e. CC /\ ( Re ` A ) = A ) -> A e. RR )
17 13 16 impbida
 |-  ( A e. CC -> ( A e. RR <-> ( Re ` A ) = A ) )