Metamath Proof Explorer

Theorem subge0

Description: Nonnegative subtraction. (Contributed by NM, 14-Mar-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 e. RR )
2 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
3 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
4 leaddsub 
 |-  ( ( 0 e. RR /\ B e. RR /\ A e. RR ) -> ( ( 0 + B ) <_ A <-> 0 <_ ( A - B ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 + B ) <_ A <-> 0 <_ ( A - B ) ) )
6 2 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
7 6 addid2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 + B ) = B )
8 7 breq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 + B ) <_ A <-> B <_ A ) )
9 5 8 bitr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A - B ) <-> B <_ A ) )