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 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ⁢ C = A ⁢ C − B ⁢ C

Proof

Step Hyp Ref Expression
1 subdi ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → C ⁢ A − B = C ⁢ A − C ⁢ B
2 1 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A − B = C ⁢ A − C ⁢ B
3 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
4 mulcom ⊢ A − B ∈ ℂ ∧ C ∈ ℂ → A − B ⁢ C = C ⁢ A − B
5 3 4 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ⁢ C = C ⁢ A − B
6 mulcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
7 6 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
8 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
9 8 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
10 7 9 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C − B ⁢ C = C ⁢ A − C ⁢ B
11 2 5 10 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ⁢ C = A ⁢ C − B ⁢ C