Metamath Proof Explorer

Theorem subge02

Description: Nonnegative subtraction. (Contributed by NM, 27-Jul-2005)

Ref Expression
Assertion subge02 
|- ( ( 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 lesubadd 
 |-  ( ( A e. RR /\ B e. RR /\ A e. RR ) -> ( ( A - B ) <_ A <-> A <_ ( A + B ) ) )
3 2 3anidm13 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A - B ) <_ A <-> A <_ ( A + B ) ) )
4 1 3 bitr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( A - B ) <_ A ) )