Metamath Proof Explorer

Theorem immul2

Description: Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion immul2 ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = A ⁢ ℑ ⁡ B

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 immul ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B
3 1 2 sylan ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B
4 rere ⊢ A ∈ ℝ → ℜ ⁡ A = A
5 4 adantr ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℜ ⁡ A = A
6 5 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ ℑ ⁡ B = A ⁢ ℑ ⁡ B
7 reim0 ⊢ A ∈ ℝ → ℑ ⁡ A = 0
8 7 oveq1d ⊢ A ∈ ℝ → ℑ ⁡ A ⁢ ℜ ⁡ B = 0 ⋅ ℜ ⁡ B
9 recl ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℝ
10 9 recnd ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℂ
11 10 mul02d ⊢ B ∈ ℂ → 0 ⋅ ℜ ⁡ B = 0
12 8 11 sylan9eq ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ ℜ ⁡ B = 0
13 6 12 oveq12d ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B = A ⁢ ℑ ⁡ B + 0
14 imcl ⊢ B ∈ ℂ → ℑ ⁡ B ∈ ℝ
15 14 recnd ⊢ B ∈ ℂ → ℑ ⁡ B ∈ ℂ
16 mulcl ⊢ A ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → A ⁢ ℑ ⁡ B ∈ ℂ
17 1 15 16 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℂ → A ⁢ ℑ ⁡ B ∈ ℂ
18 17 addridd ⊢ A ∈ ℝ ∧ B ∈ ℂ → A ⁢ ℑ ⁡ B + 0 = A ⁢ ℑ ⁡ B
19 3 13 18 3eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = A ⁢ ℑ ⁡ B