Theorem imdivd

Description: Imaginary part of a division. Related to remul2 . (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypotheses	crred.1	$$⊢\phi \to A\in ℝ$$
	remul2d.2	$$⊢\phi \to B\in ℂ$$
	redivd.2	$$⊢\phi \to A\ne 0$$
Assertion	imdivd	$$⊢\phi \to \Im \left(\frac{B}{A}\right)=\frac{\Im \left(B\right)}{A}$$

Proof

Step	Hyp	Ref	Expression
1		crred.1	$$⊢\phi \to A\in ℝ$$
2		remul2d.2	$$⊢\phi \to B\in ℂ$$
3		redivd.2	$$⊢\phi \to A\ne 0$$
4		imdiv	$$⊢\left(B\in ℂ\wedge A\in ℝ\wedge A\ne 0\right)\to \Im \left(\frac{B}{A}\right)=\frac{\Im \left(B\right)}{A}$$
5	2 1 3 4	syl3anc	$$⊢\phi \to \Im \left(\frac{B}{A}\right)=\frac{\Im \left(B\right)}{A}$$