Theorem alrple

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014)

	Ref	Expression
Assertion	alrple	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexr	|- ( A e. RR -> A e. RR* )
2		xralrple	|- ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )
3	1 2	sylan	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )