Theorem lenegcon1

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004)

	Ref	Expression
Assertion	lenegcon1	|- ( ( A e. RR /\ B e. RR ) -> ( -u A <_ B <-> -u B <_ A ) )

Proof

Step	Hyp	Ref	Expression
1		renegcl	|- ( A e. RR -> -u A e. RR )
2		leneg	|- ( ( -u A e. RR /\ B e. RR ) -> ( -u A <_ B <-> -u B <_ -u -u A ) )
3	1 2	sylan	|- ( ( A e. RR /\ B e. RR ) -> ( -u A <_ B <-> -u B <_ -u -u A ) )
4		recn	|- ( A e. RR -> A e. CC )
5	4	negnegd	|- ( A e. RR -> -u -u A = A )
6	5	breq2d	|- ( A e. RR -> ( -u B <_ -u -u A <-> -u B <_ A ) )
7	6	adantr	|- ( ( A e. RR /\ B e. RR ) -> ( -u B <_ -u -u A <-> -u B <_ A ) )
8	3 7	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( -u A <_ B <-> -u B <_ A ) )