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

Metamath Proof Explorer

Theorem immul2

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

Ref Expression
Assertion immul2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( ℑ ‘ 𝐵 ) ) )

Proof

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