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 eqtrid ⊢ 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 ‾