Metamath Proof Explorer

Theorem subdivcomb1

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

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

Proof

Step Hyp Ref Expression
1 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
2 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ
3 1 2 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A ∈ ℂ
4 divsubdir ⊢ C ⁢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A − B C = C ⁢ A C − B C
5 3 4 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A − B C = C ⁢ A C − B C
6 divcan3 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = A
7 6 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = A
8 7 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = A
9 8 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C − B C = A − B C
10 5 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A − B C = A − B C