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