Theorem remul2

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

	Ref	Expression
Assertion	remul2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( ℜ ‘ 𝐵 ) ) )

Proof

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