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 ) )