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 ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A

Proof

Step Hyp Ref Expression
1 cnre ⊢ A ∈ ℂ → ∃ x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y
2 crre ⊢ x ∈ ℝ ∧ y ∈ ℝ → ℜ ⁡ x + i ⁢ y = x
3 crim ⊢ x ∈ ℝ ∧ y ∈ ℝ → ℑ ⁡ x + i ⁢ y = y
4 3 oveq2d ⊢ x ∈ ℝ ∧ y ∈ ℝ → i ⁢ ℑ ⁡ x + i ⁢ y = i ⁢ y
5 2 4 oveq12d ⊢ x ∈ ℝ ∧ y ∈ ℝ → ℜ ⁡ x + i ⁢ y + i ⁢ ℑ ⁡ x + i ⁢ y = x + i ⁢ y
6 5 eqcomd ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + i ⁢ y = ℜ ⁡ x + i ⁢ y + i ⁢ ℑ ⁡ x + i ⁢ y
7 id ⊢ A = x + i ⁢ y → A = x + i ⁢ y
8 fveq2 ⊢ A = x + i ⁢ y → ℜ ⁡ A = ℜ ⁡ x + i ⁢ y
9 fveq2 ⊢ A = x + i ⁢ y → ℑ ⁡ A = ℑ ⁡ x + i ⁢ y
10 9 oveq2d ⊢ A = x + i ⁢ y → i ⁢ ℑ ⁡ A = i ⁢ ℑ ⁡ x + i ⁢ y
11 8 10 oveq12d ⊢ A = x + i ⁢ y → ℜ ⁡ A + i ⁢ ℑ ⁡ A = ℜ ⁡ x + i ⁢ y + i ⁢ ℑ ⁡ x + i ⁢ y
12 7 11 eqeq12d ⊢ A = x + i ⁢ y → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A ↔ x + i ⁢ y = ℜ ⁡ x + i ⁢ y + i ⁢ ℑ ⁡ x + i ⁢ y
13 6 12 syl5ibrcom ⊢ x ∈ ℝ ∧ y ∈ ℝ → A = x + i ⁢ y → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
14 13 rexlimivv ⊢ ∃ x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
15 1 14 syl ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A