# Metamath Proof Explorer

## Theorem subdi

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

Ref Expression
Assertion subdi $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B − C = A ⁢ B − A ⁢ C$

### Proof

Step Hyp Ref Expression
1 simp1 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ$
2 simp3 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ$
3 subcl $⊢ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ$
4 3 3adant1 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ$
5 1 2 4 adddid $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C + B - C = A ⁢ C + A ⁢ B − C$
6 pncan3 $⊢ C ∈ ℂ ∧ B ∈ ℂ → C + B - C = B$
7 6 ancoms $⊢ B ∈ ℂ ∧ C ∈ ℂ → C + B - C = B$
8 7 3adant1 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C + B - C = B$
9 8 oveq2d $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C + B - C = A ⁢ B$
10 5 9 eqtr3d $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C + A ⁢ B − C = A ⁢ B$
11 mulcl $⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ$
12 11 3adant3 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ∈ ℂ$
13 mulcl $⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C ∈ ℂ$
14 13 3adant2 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C ∈ ℂ$
15 mulcl $⊢ A ∈ ℂ ∧ B − C ∈ ℂ → A ⁢ B − C ∈ ℂ$
16 3 15 sylan2 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B − C ∈ ℂ$
17 16 3impb $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B − C ∈ ℂ$
18 12 14 17 subaddd $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B − A ⁢ C = A ⁢ B − C ↔ A ⁢ C + A ⁢ B − C = A ⁢ B$
19 10 18 mpbird $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B − A ⁢ C = A ⁢ B − C$
20 19 eqcomd $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B − C = A ⁢ B − A ⁢ C$