Metamath Proof Explorer

Theorem leadd1

Description: Addition to both sides of 'less than or equal to'. (Contributed by NM, 18-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 ltadd1 
 |-  ( ( B e. RR /\ A e. RR /\ C e. RR ) -> ( B < A <-> ( B + C ) < ( A + C ) ) )
2 1 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < A <-> ( B + C ) < ( A + C ) ) )
3 2 notbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. B < A <-> -. ( B + C ) < ( A + C ) ) )
4 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
5 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
6 4 5 lenltd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> -. B < A ) )
7 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
8 4 7 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + C ) e. RR )
9 5 7 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
10 8 9 lenltd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) <_ ( B + C ) <-> -. ( B + C ) < ( A + C ) ) )
11 3 6 10 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( A + C ) <_ ( B + C ) ) )