Metamath Proof Explorer

Theorem ltsub2

Description: Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 lesub2 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → B ≤ A ↔ C − A ≤ C − B
2 1 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ A ↔ C − A ≤ C − B
3 2 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ B ≤ A ↔ ¬ C − A ≤ C − B
4 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
5 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
6 4 5 ltnled ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ ¬ B ≤ A
7 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
8 7 5 resubcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C − B ∈ ℝ
9 7 4 resubcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C − A ∈ ℝ
10 8 9 ltnled ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C − B < C − A ↔ ¬ C − A ≤ C − B
11 3 6 10 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ C − B < C − A