Metamath Proof Explorer


Theorem remullem

Description: Lemma for remul , immul , and cjmul . (Contributed by NM, 28-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion remullem ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∧ ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∧ ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 replim ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
2 replim ( 𝐵 ∈ ℂ → 𝐵 = ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) )
3 1 2 oveqan12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
4 recl ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
5 4 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
6 5 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
7 ax-icn i ∈ ℂ
8 imcl ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
9 8 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
10 9 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
11 mulcl ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
12 7 10 11 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
13 6 12 addcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
14 recl ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
15 14 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
16 15 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
17 imcl ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) ∈ ℝ )
18 17 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
19 18 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
20 mulcl ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐵 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
21 7 19 20 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
22 13 16 21 adddid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
23 6 12 16 adddird ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ℜ ‘ 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) )
24 6 12 21 adddird ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
25 23 24 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) + ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) )
26 5 15 remulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
27 26 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
28 12 21 mulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ∈ ℂ )
29 12 16 mulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
30 6 21 mulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ∈ ℂ )
31 27 28 29 30 add42d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) + ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) + ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) )
32 7 a1i ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → i ∈ ℂ )
33 32 10 32 19 mul4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) = ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
34 ixi ( i · i ) = - 1
35 34 oveq1i ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) = ( - 1 · ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) )
36 9 18 remulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℝ )
37 36 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
38 37 mulm1d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 1 · ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) = - ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) )
39 35 38 eqtrid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) = - ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) )
40 33 39 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) = - ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) )
41 40 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
42 27 37 negsubd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
43 41 42 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
44 9 15 remulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
45 44 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
46 mulcl ( ( i ∈ ℂ ∧ ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ ) → ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ ℂ )
47 7 45 46 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ ℂ )
48 5 18 remulcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℝ )
49 48 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
50 mulcl ( ( i ∈ ℂ ∧ ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ ) → ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ ℂ )
51 7 49 50 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ ℂ )
52 47 51 addcomd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) + ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
53 32 10 16 mulassd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) = ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
54 6 32 19 mul12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) = ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
55 53 54 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) + ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
56 32 49 45 adddid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) = ( ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
57 52 55 56 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
58 43 57 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) + ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) )
59 25 31 58 3eqtr2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ℜ ‘ 𝐵 ) ) + ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) )
60 3 22 59 3eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) )
61 60 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ℜ ‘ ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) ) )
62 26 36 resubcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ ℝ )
63 48 44 readdcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ ℝ )
64 crre ( ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ ℝ ∧ ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ ℝ ) → ( ℜ ‘ ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
65 62 63 64 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
66 61 65 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
67 60 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ℑ ‘ ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) ) )
68 crim ( ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ ℝ ∧ ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ ℝ ) → ( ℑ ‘ ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
69 62 63 68 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
70 67 69 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
71 mulcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
72 remim ( ( 𝐴 · 𝐵 ) ∈ ℂ → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) ) )
73 71 72 syl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) ) )
74 remim ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )
75 remim ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) = ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) )
76 74 75 oveqan12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
77 16 21 subcld ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ∈ ℂ )
78 6 12 77 subdird ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) )
79 27 30 29 28 subadd4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) ) )
80 6 16 21 subdid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
81 12 16 21 subdid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
82 80 81 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) )
83 65 61 43 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
84 70 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) = ( i · ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
85 54 53 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) = ( ( i · ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) + ( i · ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
86 56 84 85 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) )
87 83 86 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( ( ℜ ‘ 𝐴 ) · ( i · ( ℑ ‘ 𝐵 ) ) ) + ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ℜ ‘ 𝐵 ) ) ) ) )
88 79 82 87 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) · ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) ) = ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) ) )
89 76 78 88 3eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) = ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ) ) )
90 73 89 eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) )
91 66 70 90 3jca ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∧ ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∧ ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) )