Description: Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | muls1d.1 | |- ( ph -> A e. CC ) |
|
muls1d.2 | |- ( ph -> B e. CC ) |
||
Assertion | mulsubfacd | |- ( ph -> ( ( A x. B ) - B ) = ( ( A - 1 ) x. B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muls1d.1 | |- ( ph -> A e. CC ) |
|
2 | muls1d.2 | |- ( ph -> B e. CC ) |
|
3 | 1cnd | |- ( ph -> 1 e. CC ) |
|
4 | 1 3 2 | subdird | |- ( 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 | eqtr2d | |- ( ph -> ( ( A x. B ) - B ) = ( ( A - 1 ) x. B ) ) |