This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 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 ) ) → ( ( ( 𝐶 · 𝐴 ) − 𝐵 ) / 𝐶 ) = ( 𝐴 − ( 𝐵 / 𝐶 ) ) )