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