Metamath Proof Explorer

Theorem lesubadd2

Description: 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999)

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

Proof

Step Hyp Ref Expression
1 lesubadd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( C + B ) ) )
2 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
3 2 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
4 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
5 4 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
6 3 5 addcomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) = ( C + B ) )
7 6 breq2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ ( B + C ) <-> A <_ ( C + B ) ) )
8 1 7 bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( B + C ) ) )