Metamath Proof Explorer

Theorem lt2sub

Description: Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
2 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
3 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR )
4 ltsub1 
 |-  ( ( A e. RR /\ C e. RR /\ B e. RR ) -> ( A < C <-> ( A - B ) < ( C - B ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A < C <-> ( A - B ) < ( C - B ) ) )
6 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
7 ltsub2 
 |-  ( ( D e. RR /\ B e. RR /\ C e. RR ) -> ( D < B <-> ( C - B ) < ( C - D ) ) )
8 6 3 2 7 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( D < B <-> ( C - B ) < ( C - D ) ) )
9 5 8 anbi12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ D < B ) <-> ( ( A - B ) < ( C - B ) /\ ( C - B ) < ( C - D ) ) ) )
10 resubcl 
 |-  ( ( 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 2 3 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C - B ) e. RR )
13 resubcl 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C - D ) e. RR )
14 13 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C - D ) e. RR )
15 lttr 
 |-  ( ( ( A - B ) e. RR /\ ( C - B ) e. RR /\ ( C - D ) e. RR ) -> ( ( ( A - B ) < ( C - B ) /\ ( C - B ) < ( C - D ) ) -> ( A - B ) < ( C - D ) ) )
16 11 12 14 15 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 ) ) )
17 9 16 sylbid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ D < B ) -> ( A - B ) < ( C - D ) ) )