Metamath Proof Explorer

Theorem divsubdiv

Description: Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014) (Revised by Mario Carneiro, 2-May-2016)

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 divadddiv ⊢ A ∈ ℂ ∧ − B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + − B D = A ⁢ D + − B ⁢ C C ⁢ D
3 1 2 sylanl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + − B D = A ⁢ D + − B ⁢ C C ⁢ D
4 simplr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ∈ ℂ
5 simprrl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → D ∈ ℂ
6 simprrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → D ≠ 0
7 divneg ⊢ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → − B D = − B D
8 4 5 6 7 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → − B D = − B D
9 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + − B D = A C + − B D
10 simpll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ∈ ℂ
11 simprll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ∈ ℂ
12 simprlr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ≠ 0
13 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
14 10 11 12 13 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C ∈ ℂ
15 divcl ⊢ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → B D ∈ ℂ
16 4 5 6 15 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B D ∈ ℂ
17 14 16 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + − B D = A C − B D
18 9 17 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + − B D = A C − B D
19 3 18 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D + − B ⁢ C C ⁢ D = A C − B D
20 4 11 mulneg1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → − B ⁢ C = − B ⁢ C
21 20 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D + − B ⁢ C = A ⁢ D + − B ⁢ C
22 10 5 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D ∈ ℂ
23 4 11 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ⁢ C ∈ ℂ
24 22 23 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D + − B ⁢ C = A ⁢ D − B ⁢ C
25 21 24 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D + − B ⁢ C = A ⁢ D − B ⁢ C
26 25 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D + − B ⁢ C C ⁢ D = A ⁢ D − B ⁢ C C ⁢ D
27 19 26 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C − B D = A ⁢ D − B ⁢ C C ⁢ D