Metamath Proof Explorer

Theorem ltsub1

Description: Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 lesub1 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → B ≤ A ↔ B − C ≤ A − C
2 1 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ A ↔ B − C ≤ A − C
3 2 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ B ≤ A ↔ ¬ B − C ≤ A − C
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 4 7 resubcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − C ∈ ℝ
9 5 7 resubcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B − C ∈ ℝ
10 8 9 ltnled ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − C < B − C ↔ ¬ B − C ≤ A − C
11 3 6 10 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ A − C < B − C