Theorem reim0

Description: The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 7-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
3	2	oveq2i	$$⊢A+\mathrm{i}\cdot 0=A+0$$
4		addid1	$$⊢A\in ℂ\to A+0=A$$
5	3 4	syl5eq	$$⊢A\in ℂ\to A+\mathrm{i}\cdot 0=A$$
6	1 5	syl	$$⊢A\in ℝ\to A+\mathrm{i}\cdot 0=A$$
7	6	fveq2d	$$⊢A\in ℝ\to \Im \left(A+\mathrm{i}\cdot 0\right)=\Im \left(A\right)$$
8		0re	$$⊢0\in ℝ$$
9		crim	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to \Im \left(A+\mathrm{i}\cdot 0\right)=0$$
10	8 9	mpan2	$$⊢A\in ℝ\to \Im \left(A+\mathrm{i}\cdot 0\right)=0$$
11	7 10	eqtr3d	$$⊢A\in ℝ\to \Im \left(A\right)=0$$