immul2

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

		Ref	Expression
	Assertion	immul2	$⊢ (A \in ℝ \land B \in ℂ) \to ℑ (A B) = A ℑ (B)$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		immul	$⊢ (A \in ℂ \land B \in ℂ) \to ℑ (A B) = ℜ (A) ℑ (B) + ℑ (A) ℜ (B)$
3	1 2	sylan	$⊢ (A \in ℝ \land B \in ℂ) \to ℑ (A B) = ℜ (A) ℑ (B) + ℑ (A) ℜ (B)$
4		rere	$⊢ A \in ℝ \to ℜ (A) = A$
5	4	adantr	$⊢ (A \in ℝ \land B \in ℂ) \to ℜ (A) = A$
6	5	oveq1d	$⊢ (A \in ℝ \land B \in ℂ) \to ℜ (A) ℑ (B) = A ℑ (B)$
7		reim0	$⊢ A \in ℝ \to ℑ (A) = 0$
8	7	oveq1d	$⊢ A \in ℝ \to ℑ (A) ℜ (B) = 0 \cdot ℜ (B)$
9		recl	$⊢ B \in ℂ \to ℜ (B) \in ℝ$
10	9	recnd	$⊢ B \in ℂ \to ℜ (B) \in ℂ$
11	10	mul02d	$⊢ B \in ℂ \to 0 \cdot ℜ (B) = 0$
12	8 11	sylan9eq	$⊢ (A \in ℝ \land B \in ℂ) \to ℑ (A) ℜ (B) = 0$
13	6 12	oveq12d	$⊢ (A \in ℝ \land B \in ℂ) \to ℜ (A) ℑ (B) + ℑ (A) ℜ (B) = A ℑ (B) + 0$
14		imcl	$⊢ B \in ℂ \to ℑ (B) \in ℝ$
15	14	recnd	$⊢ B \in ℂ \to ℑ (B) \in ℂ$
16		mulcl	$⊢ (A \in ℂ \land ℑ (B) \in ℂ) \to A ℑ (B) \in ℂ$
17	1 15 16	syl2an	$⊢ (A \in ℝ \land B \in ℂ) \to A ℑ (B) \in ℂ$
18	17	addridd	$⊢ (A \in ℝ \land B \in ℂ) \to A ℑ (B) + 0 = A ℑ (B)$
19	3 13 18	3eqtrd	$⊢ (A \in ℝ \land B \in ℂ) \to ℑ (A B) = A ℑ (B)$

Metamath Proof Explorer