Metamath Proof Explorer

Theorem reltsubadd2

Description: 'Less than' relationship between addition and subtraction. Compare ltsubadd2 . (Contributed by SN, 13-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
2 readdcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
3 2 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
4 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
5 reltsub1 ⊢ A ∈ ℝ ∧ B + C ∈ ℝ ∧ B ∈ ℝ → A < B + C ↔ A - ℝ B < B + C - ℝ B
6 1 3 4 5 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B + C ↔ A - ℝ B < B + C - ℝ B
7 repncan2 ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C - ℝ B = C
8 7 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C - ℝ B = C
9 8 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B < B + C - ℝ B ↔ A - ℝ B < C
10 6 9 bitr2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B < C ↔ A < B + C