Metamath Proof Explorer

Theorem ltleadd

Description: Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 ltadd1 
 |-  ( ( A e. RR /\ C e. RR /\ B e. RR ) -> ( A < C <-> ( A + B ) < ( C + B ) ) )
2 1 3com23 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < C <-> ( A + B ) < ( C + B ) ) )
3 2 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A < C <-> ( A + B ) < ( C + B ) ) )
4 3 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A < C <-> ( A + B ) < ( C + B ) ) )
5 leadd2 
 |-  ( ( B e. RR /\ D e. RR /\ C e. RR ) -> ( B <_ D <-> ( C + B ) <_ ( C + D ) ) )
6 5 3com23 
 |-  ( ( B e. RR /\ C e. RR /\ D e. RR ) -> ( B <_ D <-> ( C + B ) <_ ( C + D ) ) )
7 6 3expb 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR ) ) -> ( B <_ D <-> ( C + B ) <_ ( C + D ) ) )
8 7 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B <_ D <-> ( C + B ) <_ ( C + D ) ) )
9 4 8 anbi12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B <_ D ) <-> ( ( A + B ) < ( C + B ) /\ ( C + B ) <_ ( C + D ) ) ) )
10 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
11 10 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A + B ) e. RR )
12 readdcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + B ) e. RR )
13 12 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( C + B ) e. RR )
14 13 ad2ant2lr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C + B ) e. RR )
15 readdcl 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C + D ) e. RR )
16 15 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C + D ) e. RR )
17 ltletr 
 |-  ( ( ( A + B ) e. RR /\ ( C + B ) e. RR /\ ( C + D ) e. RR ) -> ( ( ( A + B ) < ( C + B ) /\ ( C + B ) <_ ( C + D ) ) -> ( A + B ) < ( C + D ) ) )
18 11 14 16 17 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A + B ) < ( C + B ) /\ ( C + B ) <_ ( C + D ) ) -> ( A + B ) < ( C + D ) ) )
19 9 18 sylbid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B <_ D ) -> ( A + B ) < ( C + D ) ) )