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

Proof

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