Metamath Proof Explorer

Theorem ltsub23

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999)

Ref Expression
Assertion ltsub23 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A − C < B

Proof

Step Hyp Ref Expression
1 ltsubadd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A < C + B
2 ltsubadd2 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A − C < B ↔ A < C + B
3 2 3com23 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − C < B ↔ A < C + B
4 1 3 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A − C < B