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

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