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

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 addid1d ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) + 0 ) = ( ℜ ‘ 𝐴 ) )
12 11 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) + 0 ) = ( ℜ ‘ 𝐴 ) )
13 2 8 12 3eqtrrd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℝ ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
14 simpr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 𝐴 ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
15 9 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 𝐴 ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
16 14 15 eqeltrrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 𝐴 ) → 𝐴 ∈ ℝ )
17 13 16 impbida ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )