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 ∈ ℂ → A ∈ ℝ ↔ ℜ ⁡ A = A

Proof

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