Metamath Proof Explorer

Theorem addge01

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

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

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 leadd2 
 |-  ( ( 0 e. RR /\ B e. RR /\ A e. RR ) -> ( 0 <_ B <-> ( A + 0 ) <_ ( A + B ) ) )
3 1 2 mp3an1 
 |-  ( ( B e. RR /\ A e. RR ) -> ( 0 <_ B <-> ( A + 0 ) <_ ( A + B ) ) )
4 3 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( A + 0 ) <_ ( A + B ) ) )
5 recn 
 |-  ( A e. RR -> A e. CC )
6 5 addid1d 
 |-  ( A e. RR -> ( A + 0 ) = A )
7 6 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + 0 ) = A )
8 7 breq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + 0 ) <_ ( A + B ) <-> A <_ ( A + B ) ) )
9 4 8 bitrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> A <_ ( A + B ) ) )