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 ℑ (A) = 0$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		it0e0	$⊢ i \cdot 0 = 0$
3	2	oveq2i	$⊢ A + i \cdot 0 = A + 0$
4		addrid	$⊢ A \in ℂ \to A + 0 = A$
5	3 4	eqtrid	$⊢ A \in ℂ \to A + i \cdot 0 = A$
6	1 5	syl	$⊢ A \in ℝ \to A + i \cdot 0 = A$
7	6	fveq2d	$⊢ A \in ℝ \to ℑ (A + i \cdot 0) = ℑ (A)$
8		0re	$⊢ 0 \in ℝ$
9		crim	$⊢ (A \in ℝ \land 0 \in ℝ) \to ℑ (A + i \cdot 0) = 0$
10	8 9	mpan2	$⊢ A \in ℝ \to ℑ (A + i \cdot 0) = 0$
11	7 10	eqtr3d	$⊢ A \in ℝ \to ℑ (A) = 0$

Metamath Proof Explorer