# 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 e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )`

### Proof

Step Hyp Ref Expression
1 cnre
` |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )`
2 crre
` |-  ( ( x e. RR /\ y e. RR ) -> ( Re ` ( x + ( _i x. y ) ) ) = x )`
3 crim
` |-  ( ( x e. RR /\ y e. RR ) -> ( Im ` ( x + ( _i x. y ) ) ) = y )`
4 3 oveq2d
` |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) = ( _i x. y ) )`
5 2 4 oveq12d
` |-  ( ( x e. RR /\ y e. RR ) -> ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) = ( x + ( _i x. y ) ) )`
6 5 eqcomd
` |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( _i x. y ) ) = ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) )`
7 id
` |-  ( A = ( x + ( _i x. y ) ) -> A = ( x + ( _i x. y ) ) )`
8 fveq2
` |-  ( A = ( x + ( _i x. y ) ) -> ( Re ` A ) = ( Re ` ( x + ( _i x. y ) ) ) )`
9 fveq2
` |-  ( A = ( x + ( _i x. y ) ) -> ( Im ` A ) = ( Im ` ( x + ( _i x. y ) ) ) )`
10 9 oveq2d
` |-  ( A = ( x + ( _i x. y ) ) -> ( _i x. ( Im ` A ) ) = ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) )`
11 8 10 oveq12d
` |-  ( A = ( x + ( _i x. y ) ) -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) )`
12 7 11 eqeq12d
` |-  ( A = ( x + ( _i x. y ) ) -> ( A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) <-> ( x + ( _i x. y ) ) = ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) ) )`
13 6 12 syl5ibrcom
` |-  ( ( x e. RR /\ y e. RR ) -> ( A = ( x + ( _i x. y ) ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) )`
14 13 rexlimivv
` |-  ( E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )`
15 1 14 syl
` |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )`