Theorem reim0b

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

	Ref	Expression
Assertion	reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		reim0	$$⊢A\in ℝ\to \Im \left(A\right)=0$$
2		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
3	2	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)=0\right)\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
4		oveq2	$$⊢\Im \left(A\right)=0\to \mathrm{i}\Im \left(A\right)=\mathrm{i}\cdot 0$$
5		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
6	4 5	eqtrdi	$$⊢\Im \left(A\right)=0\to \mathrm{i}\Im \left(A\right)=0$$
7	6	oveq2d	$$⊢\Im \left(A\right)=0\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)=\Re \left(A\right)+0$$
8		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
9	8	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
10	9	addridd	$$⊢A\in ℂ\to \Re \left(A\right)+0=\Re \left(A\right)$$
11	7 10	sylan9eqr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)=0\right)\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)=\Re \left(A\right)$$
12	3 11	eqtrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)=0\right)\to A=\Re \left(A\right)$$
13	8	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)=0\right)\to \Re \left(A\right)\in ℝ$$
14	12 13	eqeltrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)=0\right)\to A\in ℝ$$
15	14	ex	$$⊢A\in ℂ\to \left(\Im \left(A\right)=0\to A\in ℝ\right)$$
16	1 15	impbid2	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$