Metamath Proof Explorer


Theorem ltsubsubb

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

Ref Expression
Assertion ltsubsubb A B C D A C < B D A B < C D

Proof

Step Hyp Ref Expression
1 simprl A B C D C
2 1 recnd A B C D C
3 simprr A B C D D
4 3 recnd A B C D D
5 simplr A B C D B
6 5 recnd A B C D B
7 subadd23 C D B C - D + B = C + B - D
8 7 eqcomd C D B C + B - D = C - D + B
9 2 4 6 8 syl3anc A B C D C + B - D = C - D + B
10 9 breq2d A B C D A < C + B - D A < C - D + B
11 simpll A B C D A
12 resubcl B D B D
13 12 ad2ant2l A B C D B D
14 11 1 13 ltsubadd2d A B C D A C < B D A < C + B - D
15 resubcl C D C D
16 15 adantl A B C D C D
17 11 5 16 ltsubaddd A B C D A B < C D A < C - D + B
18 10 14 17 3bitr4d A B C D A C < B D A B < C D