Metamath Proof Explorer


Theorem cjreim2

Description: The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion cjreim2 ABAiB=A+iB

Proof

Step Hyp Ref Expression
1 cjreim ABA+iB=AiB
2 1 fveq2d ABA+iB=AiB
3 simpl ABA
4 3 recnd ABA
5 ax-icn i
6 5 a1i ABi
7 simpr ABB
8 7 recnd ABB
9 6 8 mulcld ABiB
10 4 9 addcld ABA+iB
11 cjcj A+iBA+iB=A+iB
12 10 11 syl ABA+iB=A+iB
13 2 12 eqtr3d ABAiB=A+iB