Theorem ltsubsubb

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

	Ref	Expression
Assertion	ltsubsubb	|- ( ( ( 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		simprl	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
2	1	recnd	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC )
3		simprr	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
4	3	recnd	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. CC )
5		simplr	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR )
6	5	recnd	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. CC )
7		subadd23	|- ( ( C e. CC /\ D e. CC /\ B e. CC ) -> ( ( C - D ) + B ) = ( C + ( B - D ) ) )
8	7	eqcomd	|- ( ( C e. CC /\ D e. CC /\ B e. CC ) -> ( C + ( B - D ) ) = ( ( C - D ) + B ) )
9	2 4 6 8	syl3anc	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C + ( B - D ) ) = ( ( C - D ) + B ) )
10	9	breq2d	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A < ( C + ( B - D ) ) <-> A < ( ( C - D ) + B ) ) )
11		simpll	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
12		resubcl	|- ( ( B e. RR /\ D e. RR ) -> ( B - D ) e. RR )
13	12	ad2ant2l	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B - D ) e. RR )
14	11 1 13	ltsubadd2d	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - C ) < ( B - D ) <-> A < ( C + ( B - D ) ) ) )
15		resubcl	|- ( ( 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	11 5 16	ltsubaddd	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - B ) < ( C - D ) <-> A < ( ( C - D ) + B ) ) )
18	10 14 17	3bitr4d	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - C ) < ( B - D ) <-> ( A - B ) < ( C - D ) ) )