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\in ℂ\to \left(A\in ℝ\leftrightarrow \Re \left(A\right)=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge A\in ℝ\right)\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
3		reim0	$$⊢A\in ℝ\to \Im \left(A\right)=0$$
4	3	oveq2d	$$⊢A\in ℝ\to \mathrm{i}\Im \left(A\right)=\mathrm{i}\cdot 0$$
5		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
6	4 5	eqtrdi	$$⊢A\in ℝ\to \mathrm{i}\Im \left(A\right)=0$$
7	6	adantl	$$⊢\left(A\in ℂ\wedge A\in ℝ\right)\to \mathrm{i}\Im \left(A\right)=0$$
8	7	oveq2d	$$⊢\left(A\in ℂ\wedge A\in ℝ\right)\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)=\Re \left(A\right)+0$$
9		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
10	9	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
11	10	addid1d	$$⊢A\in ℂ\to \Re \left(A\right)+0=\Re \left(A\right)$$
12	11	adantr	$$⊢\left(A\in ℂ\wedge A\in ℝ\right)\to \Re \left(A\right)+0=\Re \left(A\right)$$
13	2 8 12	3eqtrrd	$$⊢\left(A\in ℂ\wedge A\in ℝ\right)\to \Re \left(A\right)=A$$
14		simpr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)=A\right)\to \Re \left(A\right)=A$$
15	9	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)=A\right)\to \Re \left(A\right)\in ℝ$$
16	14 15	eqeltrrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)=A\right)\to A\in ℝ$$
17	13 16	impbida	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Re \left(A\right)=A\right)$$