Theorem redivd

Description: Real 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	redivd	$$⊢\phi \to \Re \left(\frac{B}{A}\right)=\frac{\Re \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		rediv	$$⊢\left(B\in ℂ\wedge A\in ℝ\wedge A\ne 0\right)\to \Re \left(\frac{B}{A}\right)=\frac{\Re \left(B\right)}{A}$$
5	2 1 3 4	syl3anc	$$⊢\phi \to \Re \left(\frac{B}{A}\right)=\frac{\Re \left(B\right)}{A}$$