Theorem immul

Description: Imaginary part of a product. (Contributed by NM, 28-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	immul	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \Im \left(AB\right)=\Re \left(A\right)\Im \left(B\right)+\Im \left(A\right)\Re \left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		remullem	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\Re \left(AB\right)=\Re \left(A\right)\Re \left(B\right)-\Im \left(A\right)\Im \left(B\right)\wedge \Im \left(AB\right)=\Re \left(A\right)\Im \left(B\right)+\Im \left(A\right)\Re \left(B\right)\wedge \overline{AB}=\bar{A}\bar{B}\right)$$
2	1	simp2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \Im \left(AB\right)=\Re \left(A\right)\Im \left(B\right)+\Im \left(A\right)\Re \left(B\right)$$