# 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 ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )

### Proof

Step Hyp Ref Expression
1 cnre ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2 crre ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑥 )
3 crim ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑦 )
4 3 oveq2d ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) = ( i · 𝑦 ) )
5 2 4 oveq12d ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) + ( i · ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
6 5 eqcomd ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( i · 𝑦 ) ) = ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) + ( i · ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) ) )
7 id ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
8 fveq2 ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) )
9 fveq2 ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ℑ ‘ 𝐴 ) = ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) )
10 9 oveq2d ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( i · ( ℑ ‘ 𝐴 ) ) = ( i · ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) )
11 8 10 oveq12d ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) = ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) + ( i · ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) ) )
12 7 11 eqeq12d ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ↔ ( 𝑥 + ( i · 𝑦 ) ) = ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) + ( i · ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) ) ) )
13 6 12 syl5ibrcom ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
14 13 rexlimivv ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
15 1 14 syl ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )