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	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( 𝐽 < ( ( 𝐿 − 𝑀 ) − 𝑁 ) ↔ ( 𝐽 + 𝑀 ) < ( 𝐿 − 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → 𝐽 ∈ ℝ )
2		resubcl	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝐿 − 𝑀 ) ∈ ℝ )
3	2	3adant3	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 − 𝑀 ) ∈ ℝ )
4		simp3	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ∈ ℝ )
5	3 4	resubcld	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐿 − 𝑀 ) − 𝑁 ) ∈ ℝ )
6	5	adantl	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( 𝐿 − 𝑀 ) − 𝑁 ) ∈ ℝ )
7		simpr2	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → 𝑀 ∈ ℝ )
8	1 6 7	ltadd1d	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( 𝐽 < ( ( 𝐿 − 𝑀 ) − 𝑁 ) ↔ ( 𝐽 + 𝑀 ) < ( ( ( 𝐿 − 𝑀 ) − 𝑁 ) + 𝑀 ) ) )
9		recn	⊢ ( 𝐿 ∈ ℝ → 𝐿 ∈ ℂ )
10		recn	⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℂ )
11		recn	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
12		nnpcan	⊢ ( ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 𝐿 − 𝑀 ) − 𝑁 ) + 𝑀 ) = ( 𝐿 − 𝑁 ) )
13	9 10 11 12	syl3an	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝐿 − 𝑀 ) − 𝑁 ) + 𝑀 ) = ( 𝐿 − 𝑁 ) )
14	13	adantl	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( ( 𝐿 − 𝑀 ) − 𝑁 ) + 𝑀 ) = ( 𝐿 − 𝑁 ) )
15	14	breq2d	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( 𝐽 + 𝑀 ) < ( ( ( 𝐿 − 𝑀 ) − 𝑁 ) + 𝑀 ) ↔ ( 𝐽 + 𝑀 ) < ( 𝐿 − 𝑁 ) ) )
16	8 15	bitrd	⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( 𝐽 < ( ( 𝐿 − 𝑀 ) − 𝑁 ) ↔ ( 𝐽 + 𝑀 ) < ( 𝐿 − 𝑁 ) ) )