This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem div2neg

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

Ref Expression
Assertion div2neg 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u A / -u B ) = ( A / B ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 1 3ad2ant2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u B e. CC )
3 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A e. CC )
4 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
5 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B =/= 0 )
6 div12 
 |-  ( ( -u B e. CC /\ A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( -u B x. ( A / B ) ) = ( A x. ( -u B / B ) ) )
7 2 3 4 5 6 syl112anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u B x. ( A / B ) ) = ( A x. ( -u B / B ) ) )
8 divneg 
 |-  ( ( B e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( B / B ) = ( -u B / B ) )
9 4 8 syld3an1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( B / B ) = ( -u B / B ) )
10 divid 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( B / B ) = 1 )
11 10 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B / B ) = 1 )
12 11 negeqd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( B / B ) = -u 1 )
13 9 12 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u B / B ) = -u 1 )
14 13 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. ( -u B / B ) ) = ( A x. -u 1 ) )
15 ax-1cn 
 |-  1 e. CC
16 15 negcli 
 |-  -u 1 e. CC
17 mulcom 
 |-  ( ( A e. CC /\ -u 1 e. CC ) -> ( A x. -u 1 ) = ( -u 1 x. A ) )
18 16 17 mpan2 
 |-  ( A e. CC -> ( A x. -u 1 ) = ( -u 1 x. A ) )
19 mulm1 
 |-  ( A e. CC -> ( -u 1 x. A ) = -u A )
20 18 19 eqtrd 
 |-  ( A e. CC -> ( A x. -u 1 ) = -u A )
21 20 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. -u 1 ) = -u A )
22 14 21 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. ( -u B / B ) ) = -u A )
23 7 22 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u B x. ( A / B ) ) = -u A )
24 negcl 
 |-  ( A e. CC -> -u A e. CC )
25 24 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u A e. CC )
26 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
27 negeq0 
 |-  ( B e. CC -> ( B = 0 <-> -u B = 0 ) )
28 27 necon3bid 
 |-  ( B e. CC -> ( B =/= 0 <-> -u B =/= 0 ) )
29 28 biimpa 
 |-  ( ( B e. CC /\ B =/= 0 ) -> -u B =/= 0 )
30 29 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u B =/= 0 )
31 divmul 
 |-  ( ( -u A e. CC /\ ( A / B ) e. CC /\ ( -u B e. CC /\ -u B =/= 0 ) ) -> ( ( -u A / -u B ) = ( A / B ) <-> ( -u B x. ( A / B ) ) = -u A ) )
32 25 26 2 30 31 syl112anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( -u A / -u B ) = ( A / B ) <-> ( -u B x. ( A / B ) ) = -u A ) )
33 23 32 mpbird 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u A / -u B ) = ( A / B ) )