Metamath Proof Explorer

Theorem ltsubadd2

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997)

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

Proof

Step Hyp Ref Expression
1 ltsubadd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A < C + B
2 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
3 2 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
4 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
5 4 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
6 3 5 addcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C = C + B
7 6 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B + C ↔ A < C + B
8 1 7 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A < B + C