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