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

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