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