Metamath Proof Explorer

Theorem ltadd1

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

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

Proof

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