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