Theorem addge02

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005)

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

Proof

Step	Hyp	Ref	Expression
1		addge01	|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> A <_ ( A + B ) ) )
2		recn	|- ( A e. RR -> A e. CC )
3		recn	|- ( B e. RR -> B e. CC )
4		addcom	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
5	2 3 4	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
6	5	breq2d	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ ( A + B ) <-> A <_ ( B + A ) ) )
7	1 6	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> A <_ ( B + A ) ) )