Theorem mullt0

Description: The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009)

	Ref	Expression
Assertion	mullt0	|- ( ( ( A e. RR /\ A < 0 ) /\ ( B e. RR /\ B < 0 ) ) -> 0 < ( A x. B ) )

Proof

Step	Hyp	Ref	Expression
1		renegcl	|- ( A e. RR -> -u A e. RR )
2	1	adantr	|- ( ( A e. RR /\ A < 0 ) -> -u A e. RR )
3		lt0neg1	|- ( A e. RR -> ( A < 0 <-> 0 < -u A ) )
4	3	biimpa	|- ( ( A e. RR /\ A < 0 ) -> 0 < -u A )
5	2 4	jca	|- ( ( A e. RR /\ A < 0 ) -> ( -u A e. RR /\ 0 < -u A ) )
6		renegcl	|- ( B e. RR -> -u B e. RR )
7	6	adantr	|- ( ( B e. RR /\ B < 0 ) -> -u B e. RR )
8		lt0neg1	|- ( B e. RR -> ( B < 0 <-> 0 < -u B ) )
9	8	biimpa	|- ( ( B e. RR /\ B < 0 ) -> 0 < -u B )
10	7 9	jca	|- ( ( B e. RR /\ B < 0 ) -> ( -u B e. RR /\ 0 < -u B ) )
11		mulgt0	|- ( ( ( -u A e. RR /\ 0 < -u A ) /\ ( -u B e. RR /\ 0 < -u B ) ) -> 0 < ( -u A x. -u B ) )
12	5 10 11	syl2an	|- ( ( ( A e. RR /\ A < 0 ) /\ ( B e. RR /\ B < 0 ) ) -> 0 < ( -u A x. -u B ) )
13		recn	|- ( A e. RR -> A e. CC )
14		recn	|- ( B e. RR -> B e. CC )
15		mul2neg	|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. -u B ) = ( A x. B ) )
16	13 14 15	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( -u A x. -u B ) = ( A x. B ) )
17	16	ad2ant2r	|- ( ( ( A e. RR /\ A < 0 ) /\ ( B e. RR /\ B < 0 ) ) -> ( -u A x. -u B ) = ( A x. B ) )
18	12 17	breqtrd	|- ( ( ( A e. RR /\ A < 0 ) /\ ( B e. RR /\ B < 0 ) ) -> 0 < ( A x. B ) )