# 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 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\right)\to \frac{{A}-{B}}{{C}-{D}}=\frac{{B}-{A}}{{D}-{C}}$

### Proof

Step Hyp Ref Expression
1 subcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}\in ℂ$
2 subcl ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\right)\to {C}-{D}\in ℂ$
3 2 3adant3 ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\to {C}-{D}\in ℂ$
4 subeq0 ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\right)\to \left({C}-{D}=0↔{C}={D}\right)$
5 4 necon3bid ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\right)\to \left({C}-{D}\ne 0↔{C}\ne {D}\right)$
6 5 biimp3ar ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\to {C}-{D}\ne 0$
7 3 6 jca ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\to \left({C}-{D}\in ℂ\wedge {C}-{D}\ne 0\right)$
8 div2neg ${⊢}\left({A}-{B}\in ℂ\wedge {C}-{D}\in ℂ\wedge {C}-{D}\ne 0\right)\to \frac{-\left({A}-{B}\right)}{-\left({C}-{D}\right)}=\frac{{A}-{B}}{{C}-{D}}$
9 8 3expb ${⊢}\left({A}-{B}\in ℂ\wedge \left({C}-{D}\in ℂ\wedge {C}-{D}\ne 0\right)\right)\to \frac{-\left({A}-{B}\right)}{-\left({C}-{D}\right)}=\frac{{A}-{B}}{{C}-{D}}$
10 1 7 9 syl2an ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\right)\to \frac{-\left({A}-{B}\right)}{-\left({C}-{D}\right)}=\frac{{A}-{B}}{{C}-{D}}$
11 negsubdi2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to -\left({A}-{B}\right)={B}-{A}$
12 negsubdi2 ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\right)\to -\left({C}-{D}\right)={D}-{C}$
13 12 3adant3 ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\to -\left({C}-{D}\right)={D}-{C}$
14 11 13 oveqan12d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\right)\to \frac{-\left({A}-{B}\right)}{-\left({C}-{D}\right)}=\frac{{B}-{A}}{{D}-{C}}$
15 10 14 eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\wedge {C}\ne {D}\right)\right)\to \frac{{A}-{B}}{{C}-{D}}=\frac{{B}-{A}}{{D}-{C}}$