Metamath Proof Explorer

Theorem reltsub1

Description: Subtraction from both sides of 'less than'. Compare ltsub1 . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion reltsub1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ A - ℝ C < B - ℝ C

Proof

Step Hyp Ref Expression
1 rersubcl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A - ℝ C ∈ ℝ
2 1 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C ∈ ℝ
3 rersubcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
4 3 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
5 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
6 2 4 5 ltadd2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C < B - ℝ C ↔ C + A - ℝ C < C + B - ℝ C
7 repncan3 ⊢ C ∈ ℝ ∧ A ∈ ℝ → C + A - ℝ C = A
8 7 ancoms ⊢ A ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C = A
9 8 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C = A
10 repncan3 ⊢ C ∈ ℝ ∧ B ∈ ℝ → C + B - ℝ C = B
11 10 ancoms ⊢ B ∈ ℝ ∧ C ∈ ℝ → C + B - ℝ C = B
12 11 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + B - ℝ C = B
13 9 12 breq12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C < C + B - ℝ C ↔ A < B
14 6 13 bitr2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ A - ℝ C < B - ℝ C