Metamath Proof Explorer

Theorem div2sub

Description: Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion div2sub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → A − B C − D = B − A D − C

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 subcl ⊢ C ∈ ℂ ∧ D ∈ ℂ → C − D ∈ ℂ
3 2 3adant3 ⊢ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → C − D ∈ ℂ
4 subeq0 ⊢ C ∈ ℂ ∧ D ∈ ℂ → C − D = 0 ↔ C = D
5 4 necon3bid ⊢ C ∈ ℂ ∧ D ∈ ℂ → C − D ≠ 0 ↔ C ≠ D
6 5 biimp3ar ⊢ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → C − D ≠ 0
7 3 6 jca ⊢ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → C − D ∈ ℂ ∧ C − D ≠ 0
8 div2neg ⊢ A − B ∈ ℂ ∧ C − D ∈ ℂ ∧ C − D ≠ 0 → − A − B − C − D = A − B C − D
9 8 3expb ⊢ A − B ∈ ℂ ∧ C − D ∈ ℂ ∧ C − D ≠ 0 → − A − B − C − D = A − B C − D
10 1 7 9 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → − A − B − C − D = A − B C − D
11 negsubdi2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A
12 negsubdi2 ⊢ C ∈ ℂ ∧ D ∈ ℂ → − C − D = D − C
13 12 3adant3 ⊢ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → − C − D = D − C
14 11 13 oveqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → − A − B − C − D = B − A D − C
15 10 14 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ D → A − B C − D = B − A D − C