# Metamath Proof Explorer

## 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 syl6eq ${⊢}{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)$