Metamath Proof Explorer

Theorem leaddsub

Description: 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 ltsubadd 
 |-  ( ( C e. RR /\ B e. RR /\ A e. RR ) -> ( ( C - B ) < A <-> C < ( A + B ) ) )
2 1 3com13 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C - B ) < A <-> C < ( A + B ) ) )
3 resubcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C - B ) e. RR )
4 ltnle 
 |-  ( ( ( C - B ) e. RR /\ A e. RR ) -> ( ( C - B ) < A <-> -. A <_ ( C - B ) ) )
5 3 4 stoic3 
 |-  ( ( C e. RR /\ B e. RR /\ A e. RR ) -> ( ( C - B ) < A <-> -. A <_ ( C - B ) ) )
6 5 3com13 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C - B ) < A <-> -. A <_ ( C - B ) ) )
7 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
8 ltnle 
 |-  ( ( C e. RR /\ ( A + B ) e. RR ) -> ( C < ( A + B ) <-> -. ( A + B ) <_ C ) )
9 7 8 sylan2 
 |-  ( ( C e. RR /\ ( A e. RR /\ B e. RR ) ) -> ( C < ( A + B ) <-> -. ( A + B ) <_ C ) )
10 9 3impb 
 |-  ( ( C e. RR /\ A e. RR /\ B e. RR ) -> ( C < ( A + B ) <-> -. ( A + B ) <_ C ) )
11 10 3coml 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C < ( A + B ) <-> -. ( A + B ) <_ C ) )
12 2 6 11 3bitr3rd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. ( A + B ) <_ C <-> -. A <_ ( C - B ) ) )
13 12 con4bid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) <_ C <-> A <_ ( C - B ) ) )