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 ℝ\exists y\in ℝ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)\leftrightarrow 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 ℝ\exists y\in ℝ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)$$