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 addid1d ⊢A∈ℝ∧B∈ℂ→A⁢ℑ⁡B+0=A⁢ℑ⁡B
19 3 13 18 3eqtrd ⊢A∈ℝ∧B∈ℂ→ℑ⁡A⁢B=A⁢ℑ⁡B