Metamath Proof Explorer

Theorem ltaddsublt

Description: Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018)

Ref Expression
Assertion ltaddsublt ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B < C ↔ A + B - C < A

Proof

Step Hyp Ref Expression
1 ltadd2 ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → B < C ↔ A + B < A + C
2 1 3comr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B < C ↔ A + B < A + C
3 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
4 3 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ∈ ℝ
5 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
6 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
7 4 5 6 ltsubaddd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - C < A ↔ A + B < A + C
8 2 7 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B < C ↔ A + B - C < A