Metamath Proof Explorer

Theorem leaddsub

Description: 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 ltsubadd ⊢ C ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → C − B < A ↔ C < A + B
2 1 3com13 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C − B < A ↔ C < A + B
3 resubcl ⊢ C ∈ ℝ ∧ B ∈ ℝ → C − B ∈ ℝ
4 ltnle ⊢ C − B ∈ ℝ ∧ A ∈ ℝ → C − B < A ↔ ¬ A ≤ C − B
5 3 4 stoic3 ⊢ C ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → C − B < A ↔ ¬ A ≤ C − B
6 5 3com13 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C − B < A ↔ ¬ A ≤ C − B
7 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
8 ltnle ⊢ C ∈ ℝ ∧ A + B ∈ ℝ → C < A + B ↔ ¬ A + B ≤ C
9 7 8 sylan2 ⊢ C ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → C < A + B ↔ ¬ A + B ≤ C
10 9 3impb ⊢ C ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → C < A + B ↔ ¬ A + B ≤ C
11 10 3coml ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C < A + B ↔ ¬ A + B ≤ C
12 2 6 11 3bitr3rd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ A + B ≤ C ↔ ¬ A ≤ C − B
13 12 con4bid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ≤ C ↔ A ≤ C − B