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	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		replim	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
3		reim0	⊢ ( 𝐴 ∈ ℝ → ( ℑ ‘ 𝐴 ) = 0 )
4	3	oveq2d	⊢ ( 𝐴 ∈ ℝ → ( i · ( ℑ ‘ 𝐴 ) ) = ( i · 0 ) )
5		it0e0	⊢ ( i · 0 ) = 0
6	4 5	eqtrdi	⊢ ( 𝐴 ∈ ℝ → ( i · ( ℑ ‘ 𝐴 ) ) = 0 )
7	6	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → ( i · ( ℑ ‘ 𝐴 ) ) = 0 )
8	7	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) = ( ( ℜ ‘ 𝐴 ) + 0 ) )
9		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
10	9	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
11	10	addridd	⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) + 0 ) = ( ℜ ‘ 𝐴 ) )
12	11	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) + 0 ) = ( ℜ ‘ 𝐴 ) )
13	2 8 12	3eqtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
14		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 𝐴 ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
15	9	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 𝐴 ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
16	14 15	eqeltrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 𝐴 ) → 𝐴 ∈ ℝ )
17	13 16	impbida	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )