Metamath Proof Explorer


Theorem replimd

Description: Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypothesis recld.1 ( 𝜑𝐴 ∈ ℂ )
Assertion replimd ( 𝜑𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 recld.1 ( 𝜑𝐴 ∈ ℂ )
2 replim ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
3 1 2 syl ( 𝜑𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )