# Metamath Proof Explorer

## Theorem replim

Description: Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 7-Nov-2013)

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

### Proof

Step Hyp Ref Expression
1 cnre ${⊢}{A}\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}$
2 crre ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \Re \left({x}+\mathrm{i}{y}\right)={x}$
3 crim ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \Im \left({x}+\mathrm{i}{y}\right)={y}$
4 3 oveq2d ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \mathrm{i}\Im \left({x}+\mathrm{i}{y}\right)=\mathrm{i}{y}$
5 2 4 oveq12d ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \Re \left({x}+\mathrm{i}{y}\right)+\mathrm{i}\Im \left({x}+\mathrm{i}{y}\right)={x}+\mathrm{i}{y}$
6 5 eqcomd ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}+\mathrm{i}{y}=\Re \left({x}+\mathrm{i}{y}\right)+\mathrm{i}\Im \left({x}+\mathrm{i}{y}\right)$
7 id ${⊢}{A}={x}+\mathrm{i}{y}\to {A}={x}+\mathrm{i}{y}$
8 fveq2 ${⊢}{A}={x}+\mathrm{i}{y}\to \Re \left({A}\right)=\Re \left({x}+\mathrm{i}{y}\right)$
9 fveq2 ${⊢}{A}={x}+\mathrm{i}{y}\to \Im \left({A}\right)=\Im \left({x}+\mathrm{i}{y}\right)$
10 9 oveq2d ${⊢}{A}={x}+\mathrm{i}{y}\to \mathrm{i}\Im \left({A}\right)=\mathrm{i}\Im \left({x}+\mathrm{i}{y}\right)$
11 8 10 oveq12d ${⊢}{A}={x}+\mathrm{i}{y}\to \Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)=\Re \left({x}+\mathrm{i}{y}\right)+\mathrm{i}\Im \left({x}+\mathrm{i}{y}\right)$
12 7 11 eqeq12d ${⊢}{A}={x}+\mathrm{i}{y}\to \left({A}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)↔{x}+\mathrm{i}{y}=\Re \left({x}+\mathrm{i}{y}\right)+\mathrm{i}\Im \left({x}+\mathrm{i}{y}\right)\right)$
13 6 12 syl5ibrcom ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}={x}+\mathrm{i}{y}\to {A}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)\right)$
14 13 rexlimivv ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}\to {A}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)$
15 1 14 syl ${⊢}{A}\in ℂ\to {A}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)$