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 ) )