Metamath Proof Explorer

Theorem ltadd2

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

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

Proof

Step Hyp Ref Expression
1 axltadd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( C + A ) < ( C + B ) ) )
2 oveq2 
 |-  ( A = B -> ( C + A ) = ( C + B ) )
3 2 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A = B -> ( C + A ) = ( C + B ) ) )
4 axltadd 
 |-  ( ( B e. RR /\ A e. RR /\ C e. RR ) -> ( B < A -> ( C + B ) < ( C + A ) ) )
5 4 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < A -> ( C + B ) < ( C + A ) ) )
6 3 5 orim12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A = B \/ B < A ) -> ( ( C + A ) = ( C + B ) \/ ( C + B ) < ( C + A ) ) ) )
7 6 con3d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. ( ( C + A ) = ( C + B ) \/ ( C + B ) < ( C + A ) ) -> -. ( A = B \/ B < A ) ) )
8 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
9 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
10 8 9 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + A ) e. RR )
11 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
12 8 11 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + B ) e. RR )
13 axlttri 
 |-  ( ( ( C + A ) e. RR /\ ( C + B ) e. RR ) -> ( ( C + A ) < ( C + B ) <-> -. ( ( C + A ) = ( C + B ) \/ ( C + B ) < ( C + A ) ) ) )
14 10 12 13 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) < ( C + B ) <-> -. ( ( C + A ) = ( C + B ) \/ ( C + B ) < ( C + A ) ) ) )
15 axlttri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
16 9 11 15 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
17 7 14 16 3imtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) < ( C + B ) -> A < B ) )
18 1 17 impbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C + A ) < ( C + B ) ) )