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 ) )