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

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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∧ ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∧ ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) )