Metamath Proof Explorer

Theorem ltsubadd2b

Description: Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
2 1 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
3 2 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. CC )
4 simpl 
 |-  ( ( C e. RR /\ D e. RR ) -> C e. RR )
5 4 recnd 
 |-  ( ( C e. RR /\ D e. RR ) -> C e. CC )
6 5 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC )
7 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
8 7 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
9 8 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. CC )
10 3 6 9 addsubd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( B + C ) - A ) = ( ( B - A ) + C ) )
11 10 eqcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( B - A ) + C ) = ( ( B + C ) - A ) )
12 11 breq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( D < ( ( B - A ) + C ) <-> D < ( ( B + C ) - A ) ) )
13 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
14 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
15 resubcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
16 15 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
17 16 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B - A ) e. RR )
18 13 14 17 ltsubaddd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( D - C ) < ( B - A ) <-> D < ( ( B - A ) + C ) ) )
19 7 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
20 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
21 20 ad2ant2lr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B + C ) e. RR )
22 19 13 21 ltaddsub2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + D ) < ( B + C ) <-> D < ( ( B + C ) - A ) ) )
23 12 18 22 3bitr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( D - C ) < ( B - A ) <-> ( A + D ) < ( B + C ) ) )