Metamath Proof Explorer

Theorem subdivcomb2

Description: Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
3 1 2 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B ∈ ℂ
4 divsubdir ⊢ A ∈ ℂ ∧ C ⁢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A − C ⁢ B C = A C − C ⁢ B C
5 3 4 syld3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A − C ⁢ B C = A C − C ⁢ B C
6 simprl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
7 simpl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
8 simpr ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ ∧ C ≠ 0
9 div23 ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = C C ⁢ B
10 6 7 8 9 syl3anc ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = C C ⁢ B
11 divid ⊢ C ∈ ℂ ∧ C ≠ 0 → C C = 1
12 11 oveq1d ⊢ C ∈ ℂ ∧ C ≠ 0 → C C ⁢ B = 1 ⁢ B
13 mulid2 ⊢ B ∈ ℂ → 1 ⁢ B = B
14 12 13 sylan9eqr ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C C ⁢ B = B
15 10 14 eqtrd ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = B
16 15 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = B
17 16 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C − C ⁢ B C = A C − B
18 5 17 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A − C ⁢ B C = A C − B