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

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