Metamath Proof Explorer

Theorem ltaddsub

Description: 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004)

Ref Expression
Assertion ltaddsub ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B < C ↔ A < C − B

Proof

Step Hyp Ref Expression
1 lesubadd ⊢ 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 lenlt ⊢ 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 lenlt ⊢ 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