Metamath Proof Explorer

Theorem ltsubaddb

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

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

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR )
2 1 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. CC )
3 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
4 3 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC )
5 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
6 5 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. CC )
7 2 4 6 addsubd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( B + C ) - D ) = ( ( B - D ) + C ) )
8 7 eqcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( B - D ) + C ) = ( ( B + C ) - D ) )
9 8 breq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A < ( ( B - D ) + C ) <-> A < ( ( B + C ) - D ) ) )
10 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
11 resubcl 
 |-  ( ( B e. RR /\ D e. RR ) -> ( B - D ) e. RR )
12 11 ad2ant2l 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B - D ) e. RR )
13 10 3 12 ltsubaddd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - C ) < ( B - D ) <-> A < ( ( B - D ) + C ) ) )
14 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
15 14 ad2ant2lr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B + C ) e. RR )
16 10 5 15 ltaddsubd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + D ) < ( B + C ) <-> A < ( ( B + C ) - D ) ) )
17 9 13 16 3bitr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - C ) < ( B - D ) <-> ( A + D ) < ( B + C ) ) )