This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reim0b

Description: A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005)

Ref Expression
Assertion reim0b ⊢ A ∈ ℂ → A ∈ ℝ ↔ ℑ ⁡ A = 0

Proof

Step Hyp Ref Expression
1 reim0 ⊢ A ∈ ℝ → ℑ ⁡ A = 0
2 replim ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
3 2 adantr ⊢ A ∈ ℂ ∧ ℑ ⁡ A = 0 → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
4 oveq2 ⊢ ℑ ⁡ A = 0 → i ⁢ ℑ ⁡ A = i ⋅ 0
5 it0e0 ⊢ i ⋅ 0 = 0
6 4 5 eqtrdi ⊢ ℑ ⁡ A = 0 → i ⁢ ℑ ⁡ A = 0
7 6 oveq2d ⊢ ℑ ⁡ A = 0 → ℜ ⁡ A + i ⁢ ℑ ⁡ A = ℜ ⁡ A + 0
8 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
9 8 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
10 9 addridd ⊢ A ∈ ℂ → ℜ ⁡ A + 0 = ℜ ⁡ A
11 7 10 sylan9eqr ⊢ A ∈ ℂ ∧ ℑ ⁡ A = 0 → ℜ ⁡ A + i ⁢ ℑ ⁡ A = ℜ ⁡ A
12 3 11 eqtrd ⊢ A ∈ ℂ ∧ ℑ ⁡ A = 0 → A = ℜ ⁡ A
13 8 adantr ⊢ A ∈ ℂ ∧ ℑ ⁡ A = 0 → ℜ ⁡ A ∈ ℝ
14 12 13 eqeltrd ⊢ A ∈ ℂ ∧ ℑ ⁡ A = 0 → A ∈ ℝ
15 14 ex ⊢ A ∈ ℂ → ℑ ⁡ A = 0 → A ∈ ℝ
16 1 15 impbid2 ⊢ A ∈ ℂ → A ∈ ℝ ↔ ℑ ⁡ A = 0