Theorem reim

Description: The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015)

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

Proof

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