Metamath Proof Explorer

Theorem div2neg

Description: Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012)

Ref Expression
Assertion div2neg ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-{A}}{-{B}}=\frac{{A}}{{B}}$

Proof

Step Hyp Ref Expression
1 negcl ${⊢}{B}\in ℂ\to -{B}\in ℂ$
2 1 3ad2ant2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -{B}\in ℂ$
3 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {A}\in ℂ$
4 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\in ℂ$
5 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\ne 0$
6 div12 ${⊢}\left(-{B}\in ℂ\wedge {A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(-{B}\right)\left(\frac{{A}}{{B}}\right)={A}\left(\frac{-{B}}{{B}}\right)$
7 2 3 4 5 6 syl112anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(-{B}\right)\left(\frac{{A}}{{B}}\right)={A}\left(\frac{-{B}}{{B}}\right)$
8 divneg ${⊢}\left({B}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{B}}{{B}}=\frac{-{B}}{{B}}$
9 4 8 syld3an1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{B}}{{B}}=\frac{-{B}}{{B}}$
10 divid ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{B}}{{B}}=1$
11 10 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{B}}{{B}}=1$
12 11 negeqd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{B}}{{B}}=-1$
13 9 12 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-{B}}{{B}}=-1$
14 13 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {A}\left(\frac{-{B}}{{B}}\right)={A}-1$
15 ax-1cn ${⊢}1\in ℂ$
16 15 negcli ${⊢}-1\in ℂ$
17 mulcom ${⊢}\left({A}\in ℂ\wedge -1\in ℂ\right)\to {A}-1=-1{A}$
18 16 17 mpan2 ${⊢}{A}\in ℂ\to {A}-1=-1{A}$
19 mulm1 ${⊢}{A}\in ℂ\to -1{A}=-{A}$
20 18 19 eqtrd ${⊢}{A}\in ℂ\to {A}-1=-{A}$
21 20 3ad2ant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {A}-1=-{A}$
22 14 21 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {A}\left(\frac{-{B}}{{B}}\right)=-{A}$
23 7 22 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(-{B}\right)\left(\frac{{A}}{{B}}\right)=-{A}$
24 negcl ${⊢}{A}\in ℂ\to -{A}\in ℂ$
25 24 3ad2ant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -{A}\in ℂ$
26 divcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}\in ℂ$
27 negeq0 ${⊢}{B}\in ℂ\to \left({B}=0↔-{B}=0\right)$
28 27 necon3bid ${⊢}{B}\in ℂ\to \left({B}\ne 0↔-{B}\ne 0\right)$
29 28 biimpa ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to -{B}\ne 0$
30 29 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -{B}\ne 0$
31 divmul ${⊢}\left(-{A}\in ℂ\wedge \frac{{A}}{{B}}\in ℂ\wedge \left(-{B}\in ℂ\wedge -{B}\ne 0\right)\right)\to \left(\frac{-{A}}{-{B}}=\frac{{A}}{{B}}↔\left(-{B}\right)\left(\frac{{A}}{{B}}\right)=-{A}\right)$
32 25 26 2 30 31 syl112anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(\frac{-{A}}{-{B}}=\frac{{A}}{{B}}↔\left(-{B}\right)\left(\frac{{A}}{{B}}\right)=-{A}\right)$
33 23 32 mpbird ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-{A}}{-{B}}=\frac{{A}}{{B}}$