Theorem ltnegcon1

Description: Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004)

	Ref	Expression
Assertion	ltnegcon1	|- ( ( 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		ltneg	|- ( ( -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		simpl	|- ( ( A e. RR /\ B e. RR ) -> A e. RR )
5	4	recnd	|- ( ( A e. RR /\ B e. RR ) -> A e. CC )
6	5	negnegd	|- ( ( A e. RR /\ B e. RR ) -> -u -u A = A )
7	6	breq2d	|- ( ( 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 ) )