Metamath Proof Explorer

Theorem lesubadd

Description: 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
2 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
3 1 2 resubcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A - B ) e. RR )
4 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
5 leadd1 
 |-  ( ( ( A - B ) e. RR /\ C e. RR /\ B e. RR ) -> ( ( A - B ) <_ C <-> ( ( A - B ) + B ) <_ ( C + B ) ) )
6 3 4 2 5 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> ( ( A - B ) + B ) <_ ( C + B ) ) )
7 1 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
8 2 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
9 7 8 npcand 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) + B ) = A )
10 9 breq1d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A - B ) + B ) <_ ( C + B ) <-> A <_ ( C + B ) ) )
11 6 10 bitrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( C + B ) ) )