Metamath Proof Explorer

Theorem mulre

Description: A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008)

Ref Expression
Assertion mulre 
|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( A e. RR <-> ( B x. A ) e. RR ) )

Proof

Step Hyp Ref Expression
1 rereb 
 |-  ( A e. CC -> ( A e. RR <-> ( Re ` A ) = A ) )
2 1 3ad2ant1 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( A e. RR <-> ( Re ` A ) = A ) )
3 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
4 3 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
5 4 3ad2ant1 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Re ` A ) e. CC )
6 simp1 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> A e. CC )
7 recn 
 |-  ( B e. RR -> B e. CC )
8 7 anim1i 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
9 8 3adant1 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
10 mulcan 
 |-  ( ( ( Re ` A ) e. CC /\ A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( B x. ( Re ` A ) ) = ( B x. A ) <-> ( Re ` A ) = A ) )
11 5 6 9 10 syl3anc 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( ( B x. ( Re ` A ) ) = ( B x. A ) <-> ( Re ` A ) = A ) )
12 7 adantr 
 |-  ( ( B e. RR /\ A e. CC ) -> B e. CC )
13 4 adantl 
 |-  ( ( B e. RR /\ A e. CC ) -> ( Re ` A ) e. CC )
14 ax-icn 
 |-  _i e. CC
15 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
16 15 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
17 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
18 14 16 17 sylancr 
 |-  ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
19 18 adantl 
 |-  ( ( B e. RR /\ A e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
20 12 13 19 adddid 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) = ( ( B x. ( Re ` A ) ) + ( B x. ( _i x. ( Im ` A ) ) ) ) )
21 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
22 21 adantl 
 |-  ( ( B e. RR /\ A e. CC ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
23 22 oveq2d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. A ) = ( B x. ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) )
24 mul12 
 |-  ( ( _i e. CC /\ B e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( B x. ( Im ` A ) ) ) = ( B x. ( _i x. ( Im ` A ) ) ) )
25 14 7 16 24 mp3an3an 
 |-  ( ( B e. RR /\ A e. CC ) -> ( _i x. ( B x. ( Im ` A ) ) ) = ( B x. ( _i x. ( Im ` A ) ) ) )
26 25 oveq2d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( ( B x. ( Re ` A ) ) + ( _i x. ( B x. ( Im ` A ) ) ) ) = ( ( B x. ( Re ` A ) ) + ( B x. ( _i x. ( Im ` A ) ) ) ) )
27 20 23 26 3eqtr4d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. A ) = ( ( B x. ( Re ` A ) ) + ( _i x. ( B x. ( Im ` A ) ) ) ) )
28 27 fveq2d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( Re ` ( B x. A ) ) = ( Re ` ( ( B x. ( Re ` A ) ) + ( _i x. ( B x. ( Im ` A ) ) ) ) ) )
29 remulcl 
 |-  ( ( B e. RR /\ ( Re ` A ) e. RR ) -> ( B x. ( Re ` A ) ) e. RR )
30 3 29 sylan2 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. ( Re ` A ) ) e. RR )
31 remulcl 
 |-  ( ( B e. RR /\ ( Im ` A ) e. RR ) -> ( B x. ( Im ` A ) ) e. RR )
32 15 31 sylan2 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. ( Im ` A ) ) e. RR )
33 crre 
 |-  ( ( ( B x. ( Re ` A ) ) e. RR /\ ( B x. ( Im ` A ) ) e. RR ) -> ( Re ` ( ( B x. ( Re ` A ) ) + ( _i x. ( B x. ( Im ` A ) ) ) ) ) = ( B x. ( Re ` A ) ) )
34 30 32 33 syl2anc 
 |-  ( ( B e. RR /\ A e. CC ) -> ( Re ` ( ( B x. ( Re ` A ) ) + ( _i x. ( B x. ( Im ` A ) ) ) ) ) = ( B x. ( Re ` A ) ) )
35 28 34 eqtr2d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. ( Re ` A ) ) = ( Re ` ( B x. A ) ) )
36 35 eqeq1d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( ( B x. ( Re ` A ) ) = ( B x. A ) <-> ( Re ` ( B x. A ) ) = ( B x. A ) ) )
37 mulcl 
 |-  ( ( B e. CC /\ A e. CC ) -> ( B x. A ) e. CC )
38 7 37 sylan 
 |-  ( ( B e. RR /\ A e. CC ) -> ( B x. A ) e. CC )
39 rereb 
 |-  ( ( B x. A ) e. CC -> ( ( B x. A ) e. RR <-> ( Re ` ( B x. A ) ) = ( B x. A ) ) )
40 38 39 syl 
 |-  ( ( B e. RR /\ A e. CC ) -> ( ( B x. A ) e. RR <-> ( Re ` ( B x. A ) ) = ( B x. A ) ) )
41 36 40 bitr4d 
 |-  ( ( B e. RR /\ A e. CC ) -> ( ( B x. ( Re ` A ) ) = ( B x. A ) <-> ( B x. A ) e. RR ) )
42 41 ancoms 
 |-  ( ( A e. CC /\ B e. RR ) -> ( ( B x. ( Re ` A ) ) = ( B x. A ) <-> ( B x. A ) e. RR ) )
43 42 3adant3 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( ( B x. ( Re ` A ) ) = ( B x. A ) <-> ( B x. A ) e. RR ) )
44 2 11 43 3bitr2d 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( A e. RR <-> ( B x. A ) e. RR ) )