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⁢BC=AC−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⁢BC=AC−C⁢BC
5 3 4 syld3an2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A−C⁢BC=AC−C⁢BC
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⁢BC=CC⁢B
10 6 7 8 9 syl3anc ⊢B∈ℂ∧C∈ℂ∧C≠0→C⁢BC=CC⁢B
11 divid ⊢C∈ℂ∧C≠0→CC=1
12 11 oveq1d ⊢C∈ℂ∧C≠0→CC⁢B=1⁢B
13 mullid ⊢B∈ℂ→1⁢B=B
14 12 13 sylan9eqr ⊢B∈ℂ∧C∈ℂ∧C≠0→CC⁢B=B
15 10 14 eqtrd ⊢B∈ℂ∧C∈ℂ∧C≠0→C⁢BC=B
16 15 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢BC=B
17 16 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC−C⁢BC=AC−B
18 5 17 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A−C⁢BC=AC−B