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 \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to (J < L - M - N \leftrightarrow J + M < L - N)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to J \in ℝ$
2		resubcl	$⊢ (L \in ℝ \land M \in ℝ) \to L - M \in ℝ$
3	2	3adant3	$⊢ (L \in ℝ \land M \in ℝ \land N \in ℝ) \to L - M \in ℝ$
4		simp3	$⊢ (L \in ℝ \land M \in ℝ \land N \in ℝ) \to N \in ℝ$
5	3 4	resubcld	$⊢ (L \in ℝ \land M \in ℝ \land N \in ℝ) \to L - M - N \in ℝ$
6	5	adantl	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to L - M - N \in ℝ$
7		simpr2	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to M \in ℝ$
8	1 6 7	ltadd1d	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to (J < L - M - N \leftrightarrow J + M < (L - M) - N + M)$
9		recn	$⊢ L \in ℝ \to L \in ℂ$
10		recn	$⊢ M \in ℝ \to M \in ℂ$
11		recn	$⊢ N \in ℝ \to N \in ℂ$
12		nnpcan	$⊢ (L \in ℂ \land M \in ℂ \land N \in ℂ) \to (L - M) - N + M = L - N$
13	9 10 11 12	syl3an	$⊢ (L \in ℝ \land M \in ℝ \land N \in ℝ) \to (L - M) - N + M = L - N$
14	13	adantl	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to (L - M) - N + M = L - N$
15	14	breq2d	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to (J + M < (L - M) - N + M \leftrightarrow J + M < L - N)$
16	8 15	bitrd	$⊢ (J \in ℝ \land (L \in ℝ \land M \in ℝ \land N \in ℝ)) \to (J < L - M - N \leftrightarrow J + M < L - N)$

Metamath Proof Explorer

Theorem ltsubsubaddltsub

Proof