Theorem imval

Description: The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	$$⊢x=A\to \Re \left(\frac{x}{\mathrm{i}}\right)=\Re \left(\frac{A}{\mathrm{i}}\right)$$
2		df-im	$$⊢\Im =\left(x\in ℂ⟼\Re \left(\frac{x}{\mathrm{i}}\right)\right)$$
3		fvex	$$⊢\Re \left(\frac{A}{\mathrm{i}}\right)\in \mathrm{V}$$
4	1 2 3	fvmpt	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\frac{A}{\mathrm{i}}\right)$$