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 ) ) )