Theorem subdivcomb2

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

	Ref	Expression
Assertion	subdivcomb2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 − ( 𝐶 · 𝐵 ) ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simp3l	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ )
2		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℂ )
3	1 2	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
4		divsubdir	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 − ( 𝐶 · 𝐵 ) ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) − ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) )
5	3 4	syld3an2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 − ( 𝐶 · 𝐵 ) ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) − ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) )
6		simprl	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ )
7		simpl	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℂ )
8		simpr	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
9		div23	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = ( ( 𝐶 / 𝐶 ) · 𝐵 ) )
10	6 7 8 9	syl3anc	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = ( ( 𝐶 / 𝐶 ) · 𝐵 ) )
11		divid	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐶 / 𝐶 ) = 1 )
12	11	oveq1d	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐶 / 𝐶 ) · 𝐵 ) = ( 1 · 𝐵 ) )
13		mullid	⊢ ( 𝐵 ∈ ℂ → ( 1 · 𝐵 ) = 𝐵 )
14	12 13	sylan9eqr	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 / 𝐶 ) · 𝐵 ) = 𝐵 )
15	10 14	eqtrd	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
16	15	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
17	16	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) − ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) = ( ( 𝐴 / 𝐶 ) − 𝐵 ) )
18	5 17	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 − ( 𝐶 · 𝐵 ) ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) − 𝐵 ) )