Metamath Proof Explorer

Theorem divsubdir

Description: Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005)

Ref Expression
Assertion divsubdir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A − B C = A C − B C

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 divdir ⊢ A ∈ ℂ ∧ − B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + − B C = A C + − B C
3 1 2 syl3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + − B C = A C + − B C
4 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
5 4 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B C = A − B C
6 5 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + − B C = A − B C
7 3 6 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C + − B C = A − B C
8 divneg ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → − B C = − B C
9 8 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → − B C = − B C
10 9 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → − B C = − B C
11 10 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C + − B C = A C + − B C
12 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
13 12 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
14 13 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
15 divcl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
16 15 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
17 16 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
18 14 17 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C + − B C = A C − B C
19 11 18 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C + − B C = A C − B C
20 7 19 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A − B C = A C − B C