This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem immul2

Description: Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion immul2 
|- ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 immul 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
3 1 2 sylan 
 |-  ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
4 rere 
 |-  ( A e. RR -> ( Re ` A ) = A )
5 4 adantr 
 |-  ( ( A e. RR /\ B e. CC ) -> ( Re ` A ) = A )
6 5 oveq1d 
 |-  ( ( A e. RR /\ B e. CC ) -> ( ( Re ` A ) x. ( Im ` B ) ) = ( A x. ( Im ` B ) ) )
7 reim0 
 |-  ( A e. RR -> ( Im ` A ) = 0 )
8 7 oveq1d 
 |-  ( A e. RR -> ( ( Im ` A ) x. ( Re ` B ) ) = ( 0 x. ( Re ` B ) ) )
9 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
10 9 recnd 
 |-  ( B e. CC -> ( Re ` B ) e. CC )
11 10 mul02d 
 |-  ( B e. CC -> ( 0 x. ( Re ` B ) ) = 0 )
12 8 11 sylan9eq 
 |-  ( ( A e. RR /\ B e. CC ) -> ( ( Im ` A ) x. ( Re ` B ) ) = 0 )
13 6 12 oveq12d 
 |-  ( ( A e. RR /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) = ( ( A x. ( Im ` B ) ) + 0 ) )
14 imcl 
 |-  ( B e. CC -> ( Im ` B ) e. RR )
15 14 recnd 
 |-  ( B e. CC -> ( Im ` B ) e. CC )
16 mulcl 
 |-  ( ( A e. CC /\ ( Im ` B ) e. CC ) -> ( A x. ( Im ` B ) ) e. CC )
17 1 15 16 syl2an 
 |-  ( ( A e. RR /\ B e. CC ) -> ( A x. ( Im ` B ) ) e. CC )
18 17 addridd 
 |-  ( ( A e. RR /\ B e. CC ) -> ( ( A x. ( Im ` B ) ) + 0 ) = ( A x. ( Im ` B ) ) )
19 3 13 18 3eqtrd 
 |-  ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )