Theorem subdivcomb1

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

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

Proof

Step	Hyp	Ref	Expression
1		simp3l	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ )
2		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐴 ∈ ℂ )
3	1 2	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐴 ) ∈ ℂ )
4		divsubdir	⊢ ( ( ( 𝐶 · 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) − 𝐵 ) / 𝐶 ) = ( ( ( 𝐶 · 𝐴 ) / 𝐶 ) − ( 𝐵 / 𝐶 ) ) )
5	3 4	syld3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) − 𝐵 ) / 𝐶 ) = ( ( ( 𝐶 · 𝐴 ) / 𝐶 ) − ( 𝐵 / 𝐶 ) ) )
6		divcan3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐶 · 𝐴 ) / 𝐶 ) = 𝐴 )
7	6	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) / 𝐶 ) = 𝐴 )
8	7	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) / 𝐶 ) = 𝐴 )
9	8	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) / 𝐶 ) − ( 𝐵 / 𝐶 ) ) = ( 𝐴 − ( 𝐵 / 𝐶 ) ) )
10	5 9	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 𝐶 · 𝐴 ) − 𝐵 ) / 𝐶 ) = ( 𝐴 − ( 𝐵 / 𝐶 ) ) )