Theorem imre

Description: The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	imre	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$

Proof

Step	Hyp	Ref	Expression
1		imval	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\frac{A}{\mathrm{i}}\right)$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		ine0	$$⊢\mathrm{i}\ne 0$$
4		divrec2	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \frac{A}{\mathrm{i}}=\left(\frac{1}{\mathrm{i}}\right)A$$
5	2 3 4	mp3an23	$$⊢A\in ℂ\to \frac{A}{\mathrm{i}}=\left(\frac{1}{\mathrm{i}}\right)A$$
6		irec	$$⊢\frac{1}{\mathrm{i}}=-\mathrm{i}$$
7	6	oveq1i	$$⊢\left(\frac{1}{\mathrm{i}}\right)A=\left(-\mathrm{i}\right)A$$
8	5 7	eqtrdi	$$⊢A\in ℂ\to \frac{A}{\mathrm{i}}=\left(-\mathrm{i}\right)A$$
9	8	fveq2d	$$⊢A\in ℂ\to \Re \left(\frac{A}{\mathrm{i}}\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$
10	1 9	eqtrd	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$