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