Theorem posdif

Description: Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004)

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

Proof

Step	Hyp	Ref	Expression
1		resubcl	|- ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
2	1	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
3		simpl	|- ( ( A e. RR /\ B e. RR ) -> A e. RR )
4		ltaddpos	|- ( ( ( B - A ) e. RR /\ A e. RR ) -> ( 0 < ( B - A ) <-> A < ( A + ( B - A ) ) ) )
5	2 3 4	syl2anc	|- ( ( A e. RR /\ B e. RR ) -> ( 0 < ( B - A ) <-> A < ( A + ( B - A ) ) ) )
6		recn	|- ( A e. RR -> A e. CC )
7		recn	|- ( B e. RR -> B e. CC )
8		pncan3	|- ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )
9	6 7 8	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( A + ( B - A ) ) = B )
10	9	breq2d	|- ( ( A e. RR /\ B e. RR ) -> ( A < ( A + ( B - A ) ) <-> A < B ) )
11	5 10	bitr2d	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )