This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 · ( ℑ ‘ 𝐴 ) ) ) )