Metamath Proof Explorer

Theorem leaddsuble

Description: Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018)

Ref Expression
Assertion leaddsuble ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A + B - C ≤ A

Proof

Step Hyp Ref Expression
1 leadd2 ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → B ≤ C ↔ A + B ≤ A + C
2 1 3comr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A + B ≤ A + C
3 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
4 3 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ∈ ℝ
5 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
6 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
7 4 5 6 lesubaddd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - C ≤ A ↔ A + B ≤ A + C
8 2 7 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A + B - C ≤ A