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−BC−D=B−AD−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−BC−D
9 8 3expb ⊢A−B∈ℂ∧C−D∈ℂ∧C−D≠0→−A−B−C−D=A−BC−D
10 1 7 9 syl2an ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ∧C≠D→−A−B−C−D=A−BC−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−AD−C
15 10 14 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ∧C≠D→A−BC−D=B−AD−C