Theorem addmuldir2d

Description: Distributive law with summands being products with a common factor. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Hypotheses	addmuldir2d.a	$$⊢\phi \to A\in ℂ$$
	addmuldir2d.b	$$⊢\phi \to B\in ℂ$$
	addmuldir2d.c	$$⊢\phi \to C\in ℂ$$
	addmuldir2d.d	$$⊢\phi \to D\in ℂ$$
	addmuldir2d.e	$$⊢\phi \to E\in ℂ$$
Assertion	addmuldir2d	$$⊢\phi \to \left(A+BC\right)\left(D+EC\right)=AD+\left(AE+DB\right)C+BE{C}^2$$

Proof

Step	Hyp	Ref	Expression
1		addmuldir2d.a	$$⊢\phi \to A\in ℂ$$
2		addmuldir2d.b	$$⊢\phi \to B\in ℂ$$
3		addmuldir2d.c	$$⊢\phi \to C\in ℂ$$
4		addmuldir2d.d	$$⊢\phi \to D\in ℂ$$
5		addmuldir2d.e	$$⊢\phi \to E\in ℂ$$
6	1 2 3 4 5 3	addmuldir1d	$$⊢\phi \to \left(A+BC\right)\left(D+EC\right)=AD+AEC+DBC+BCEC$$
7	1 4	mulcld	$$⊢\phi \to AD\in ℂ$$
8	5 3	mulcld	$$⊢\phi \to EC\in ℂ$$
9	1 8	mulcld	$$⊢\phi \to AEC\in ℂ$$
10	7 9	addcld	$$⊢\phi \to AD+AEC\in ℂ$$
11	2 3	mulcld	$$⊢\phi \to BC\in ℂ$$
12	4 11	mulcld	$$⊢\phi \to DBC\in ℂ$$
13	11 8	mulcld	$$⊢\phi \to BCEC\in ℂ$$
14	10 12 13	addassd	$$⊢\phi \to \left(AD+AEC\right)+DBC+BCEC=AD+AEC+DBC+BCEC$$
15	7 9 12	addassd	$$⊢\phi \to AD+AEC+DBC=AD+AEC+DBC$$
16	1 5	mulcld	$$⊢\phi \to AE\in ℂ$$
17	4 2	mulcld	$$⊢\phi \to DB\in ℂ$$
18	16 17 3	adddird	$$⊢\phi \to \left(AE+DB\right)C=AEC+DBC$$
19	1 5 3	mulassd	$$⊢\phi \to AEC=AEC$$
20	4 2 3	mulassd	$$⊢\phi \to DBC=DBC$$
21	19 20	oveq12d	$$⊢\phi \to AEC+DBC=AEC+DBC$$
22	18 21	eqtr2d	$$⊢\phi \to AEC+DBC=\left(AE+DB\right)C$$
23	22	oveq2d	$$⊢\phi \to AD+AEC+DBC=AD+\left(AE+DB\right)C$$
24	15 23	eqtrd	$$⊢\phi \to AD+AEC+DBC=AD+\left(AE+DB\right)C$$
25	2 3 5 3	mul4d	$$⊢\phi \to BCEC=BECC$$
26		sqval	$$⊢C\in ℂ\to C^2=CC$$
27	26	eqcomd	$$⊢C\in ℂ\to CC=C^2$$
28	3 27	syl	$$⊢\phi \to CC=C^2$$
29	28	oveq2d	$$⊢\phi \to BECC=BE{C}^2$$
30	25 29	eqtrd	$$⊢\phi \to BCEC=BE{C}^2$$
31	24 30	oveq12d	$$⊢\phi \to \left(AD+AEC\right)+DBC+BCEC=AD+\left(AE+DB\right)C+BE{C}^2$$
32	6 14 31	3eqtr2d	$$⊢\phi \to \left(A+BC\right)\left(D+EC\right)=AD+\left(AE+DB\right)C+BE{C}^2$$