Metamath Proof Explorer

Theorem ltsub13

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 ltaddsub ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A + C < B ↔ A < B − C
2 ltaddsub2 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A + C < B ↔ C < B − A
3 1 2 bitr3d ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A < B − C ↔ C < B − A
4 3 3com23 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B − C ↔ C < B − A