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 B C D A C < B D A + D < B + C

Proof

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