# Metamath Proof Explorer

## Theorem subdir

Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by NM, 30-Dec-2005)

Ref Expression
Assertion subdir ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right){C}={A}{C}-{B}{C}$

### Proof

Step Hyp Ref Expression
1 subdi ${⊢}\left({C}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℂ\right)\to {C}\left({A}-{B}\right)={C}{A}-{C}{B}$
2 1 3coml ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}\left({A}-{B}\right)={C}{A}-{C}{B}$
3 subcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}\in ℂ$
4 mulcom ${⊢}\left({A}-{B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right){C}={C}\left({A}-{B}\right)$
5 3 4 stoic3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right){C}={C}\left({A}-{B}\right)$
6 mulcom ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}{C}={C}{A}$
7 6 3adant2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}{C}={C}{A}$
8 mulcom ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}{C}={C}{B}$
9 8 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}{C}={C}{B}$
10 7 9 oveq12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}{C}-{B}{C}={C}{A}-{C}{B}$
11 2 5 10 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right){C}={A}{C}-{B}{C}$