# Metamath Proof Explorer

## Theorem int-rightdistd

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

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

### Proof

Step Hyp Ref Expression
1 int-rightdistd.1 ${⊢}{\phi }\to {B}\in ℝ$
2 int-rightdistd.2 ${⊢}{\phi }\to {C}\in ℝ$
3 int-rightdistd.3 ${⊢}{\phi }\to {D}\in ℝ$
4 int-rightdistd.4 ${⊢}{\phi }\to {A}={B}$
5 1 recnd ${⊢}{\phi }\to {B}\in ℂ$
6 2 recnd ${⊢}{\phi }\to {C}\in ℂ$
7 3 recnd ${⊢}{\phi }\to {D}\in ℂ$
8 6 7 addcld ${⊢}{\phi }\to {C}+{D}\in ℂ$
9 5 8 mulcomd ${⊢}{\phi }\to {B}\left({C}+{D}\right)=\left({C}+{D}\right){B}$
10 6 5 mulcomd ${⊢}{\phi }\to {C}{B}={B}{C}$
11 4 eqcomd ${⊢}{\phi }\to {B}={A}$
12 11 oveq1d ${⊢}{\phi }\to {B}{C}={A}{C}$
13 10 12 eqtrd ${⊢}{\phi }\to {C}{B}={A}{C}$
14 7 5 mulcomd ${⊢}{\phi }\to {D}{B}={B}{D}$
15 11 oveq1d ${⊢}{\phi }\to {B}{D}={A}{D}$
16 14 15 eqtrd ${⊢}{\phi }\to {D}{B}={A}{D}$
17 13 16 oveq12d ${⊢}{\phi }\to {C}{B}+{D}{B}={A}{C}+{A}{D}$
18 6 5 7 17 joinlmuladdmuld ${⊢}{\phi }\to \left({C}+{D}\right){B}={A}{C}+{A}{D}$
19 9 18 eqtrd ${⊢}{\phi }\to {B}\left({C}+{D}\right)={A}{C}+{A}{D}$