Metamath Proof Explorer

Theorem lesub

Description: Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion lesub ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B − C ↔ C ≤ B − A

Proof

Step Hyp Ref Expression
1 leaddsub ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A + C ≤ B ↔ A ≤ B − C
2 leaddsub2 ⊢ 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