Description: Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | adddirp1d.a | |- ( ph -> A e. CC ) |
|
adddirp1d.b | |- ( ph -> B e. CC ) |
||
Assertion | adddirp1d | |- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adddirp1d.a | |- ( ph -> A e. CC ) |
|
2 | adddirp1d.b | |- ( ph -> B e. CC ) |
|
3 | 1cnd | |- ( ph -> 1 e. CC ) |
|
4 | 1 3 2 | adddird | |- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + ( 1 x. B ) ) ) |
5 | 2 | mulid2d | |- ( ph -> ( 1 x. B ) = B ) |
6 | 5 | oveq2d | |- ( ph -> ( ( A x. B ) + ( 1 x. B ) ) = ( ( A x. B ) + B ) ) |
7 | 4 6 | eqtrd | |- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + B ) ) |