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