Metamath Proof Explorer


Theorem ltsubsubaddltsub

Description: If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018)

Ref Expression
Assertion ltsubsubaddltsub J L M N J < L - M - N J + M < L N

Proof

Step Hyp Ref Expression
1 simpl J L M N J
2 resubcl L M L M
3 2 3adant3 L M N L M
4 simp3 L M N N
5 3 4 resubcld L M N L - M - N
6 5 adantl J L M N L - M - N
7 simpr2 J L M N M
8 1 6 7 ltadd1d J L M N J < L - M - N J + M < L M - N + M
9 recn L L
10 recn M M
11 recn N N
12 nnpcan L M N L M - N + M = L N
13 9 10 11 12 syl3an L M N L M - N + M = L N
14 13 adantl J L M N L M - N + M = L N
15 14 breq2d J L M N J + M < L M - N + M J + M < L N
16 8 15 bitrd J L M N J < L - M - N J + M < L N