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 e. RR /\ ( L e. RR /\ M e. RR /\ N e. RR ) ) -> ( J < ( ( L - M ) - N ) <-> ( J + M ) < ( L - N ) ) )

Proof

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