# 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 $⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B ∧ ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B ∧ A ⁢ B ‾ = A ‾ ⁢ B ‾$

### Proof

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