# Metamath Proof Explorer

## 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}={C}{A}+{D}{A}$

### 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}={C}{B}+{D}{B}$
9 5 7 mulcld ${⊢}{\phi }\to {C}{B}\in ℂ$
10 6 7 mulcld ${⊢}{\phi }\to {D}{B}\in ℂ$
11 9 10 addcomd ${⊢}{\phi }\to {C}{B}+{D}{B}={D}{B}+{C}{B}$
12 10 9 addcomd ${⊢}{\phi }\to {D}{B}+{C}{B}={C}{B}+{D}{B}$
13 4 eqcomd ${⊢}{\phi }\to {B}={A}$
14 13 oveq2d ${⊢}{\phi }\to {C}{B}={C}{A}$
15 13 oveq2d ${⊢}{\phi }\to {D}{B}={D}{A}$
16 14 15 oveq12d ${⊢}{\phi }\to {C}{B}+{D}{B}={C}{A}+{D}{A}$
17 12 16 eqtrd ${⊢}{\phi }\to {D}{B}+{C}{B}={C}{A}+{D}{A}$
18 8 11 17 3eqtrd ${⊢}{\phi }\to \left({C}+{D}\right){B}={C}{A}+{D}{A}$