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