Theorem int-leftdistd

Description: AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

	Ref	Expression
Hypotheses	int-leftdistd.1	$$⊢\phi \to B\in ℝ$$
	int-leftdistd.2	$$⊢\phi \to C\in ℝ$$
	int-leftdistd.3	$$⊢\phi \to D\in ℝ$$
	int-leftdistd.4	$$⊢\phi \to A=B$$
Assertion	int-leftdistd	$$⊢\phi \to \left(C+D\right)B=CA+DA$$

Proof

Step	Hyp	Ref	Expression
1		int-leftdistd.1	$$⊢\phi \to B\in ℝ$$
2		int-leftdistd.2	$$⊢\phi \to C\in ℝ$$
3		int-leftdistd.3	$$⊢\phi \to D\in ℝ$$
4		int-leftdistd.4	$$⊢\phi \to A=B$$
5	2	recnd	$$⊢\phi \to C\in ℂ$$
6	3	recnd	$$⊢\phi \to D\in ℂ$$
7	1	recnd	$$⊢\phi \to B\in ℂ$$
8	5 6 7	adddird	$$⊢\phi \to \left(C+D\right)B=CB+DB$$
9	5 7	mulcld	$$⊢\phi \to CB\in ℂ$$
10	6 7	mulcld	$$⊢\phi \to DB\in ℂ$$
11	9 10	addcomd	$$⊢\phi \to CB+DB=DB+CB$$
12	10 9	addcomd	$$⊢\phi \to DB+CB=CB+DB$$
13	4	eqcomd	$$⊢\phi \to B=A$$
14	13	oveq2d	$$⊢\phi \to CB=CA$$
15	13	oveq2d	$$⊢\phi \to DB=DA$$
16	14 15	oveq12d	$$⊢\phi \to CB+DB=CA+DA$$
17	12 16	eqtrd	$$⊢\phi \to DB+CB=CA+DA$$
18	8 11 17	3eqtrd	$$⊢\phi \to \left(C+D\right)B=CA+DA$$