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 
|- ( ( A e. RR /\ B e. RR ) -> ( * ` ( A - ( _i x. B ) ) ) = ( A + ( _i x. B ) ) )

Proof

Step Hyp Ref Expression
1 cjreim 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) = ( A - ( _i x. B ) ) )
2 1 fveq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( * ` ( A + ( _i x. B ) ) ) ) = ( * ` ( A - ( _i x. B ) ) ) )
3 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
4 3 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
5 ax-icn 
 |-  _i e. CC
6 5 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> _i e. CC )
7 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
8 7 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
9 6 8 mulcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. B ) e. CC )
10 4 9 addcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( _i x. B ) ) e. CC )
11 cjcj 
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( * ` ( * ` ( A + ( _i x. B ) ) ) ) = ( A + ( _i x. B ) ) )
12 10 11 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( * ` ( A + ( _i x. B ) ) ) ) = ( A + ( _i x. B ) ) )
13 2 12 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( A - ( _i x. B ) ) ) = ( A + ( _i x. B ) ) )