Theorem muldivdid

Description: Distribution of division over addition with a multiplication. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	muldivdid.1	$$⊢\phi \to A\in ℂ$$
	muldivdid.2	$$⊢\phi \to B\in ℂ$$
	muldivdid.3	$$⊢\phi \to C\in ℂ$$
	muldivdid.4	$$⊢\phi \to B\ne 0$$
Assertion	muldivdid	$$⊢\phi \to \frac{AB+C}{B}=A+\left(\frac{C}{B}\right)$$

Proof

Step	Hyp	Ref	Expression
1		muldivdid.1	$$⊢\phi \to A\in ℂ$$
2		muldivdid.2	$$⊢\phi \to B\in ℂ$$
3		muldivdid.3	$$⊢\phi \to C\in ℂ$$
4		muldivdid.4	$$⊢\phi \to B\ne 0$$
5	1 2	mulcomd	$$⊢\phi \to AB=BA$$
6	5	oveq1d	$$⊢\phi \to AB+C=BA+C$$
7	6	oveq1d	$$⊢\phi \to \frac{AB+C}{B}=\frac{BA+C}{B}$$
8		muldivdir	$$⊢\left(A\in ℂ\wedge C\in ℂ\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to \frac{BA+C}{B}=A+\left(\frac{C}{B}\right)$$
9	1 3 2 4 8	syl112anc	$$⊢\phi \to \frac{BA+C}{B}=A+\left(\frac{C}{B}\right)$$
10	7 9	eqtrd	$$⊢\phi \to \frac{AB+C}{B}=A+\left(\frac{C}{B}\right)$$