Metamath Proof Explorer

Theorem remul2

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

Ref Expression
Assertion remul2 ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B = A ⁢ ℜ ⁡ B

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 remul ⊢ 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 imcl ⊢ 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 recl ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℝ
15 14 recnd ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℂ
16 mulcl ⊢ A ∈ ℂ ∧ ℜ ⁡ B ∈ ℂ → A ⁢ ℜ ⁡ B ∈ ℂ
17 1 15 16 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℂ → A ⁢ ℜ ⁡ B ∈ ℂ
18 17 subid1d ⊢ A ∈ ℝ ∧ B ∈ ℂ → A ⁢ ℜ ⁡ B − 0 = A ⁢ ℜ ⁡ B
19 3 13 18 3eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B = A ⁢ ℜ ⁡ B