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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ ( 𝐵 − 𝐶 ) ↔ 𝐶 ≤ ( 𝐵 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 leaddsub ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐵 − 𝐶 ) ) )
2 leaddsub2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) ≤ 𝐵 ↔ 𝐶 ≤ ( 𝐵 − 𝐴 ) ) )
3 1 2 bitr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ ( 𝐵 − 𝐶 ) ↔ 𝐶 ≤ ( 𝐵 − 𝐴 ) ) )
4 3 3com23 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ ( 𝐵 − 𝐶 ) ↔ 𝐶 ≤ ( 𝐵 − 𝐴 ) ) )