Metamath Proof Explorer

Theorem ltsubadd

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
2 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
3 1 2 resubcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ∈ ℝ
4 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
5 ltadd1 ⊢ A − B ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A − B < C ↔ A - B + B < C + B
6 3 4 2 5 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A - B + B < C + B
7 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℂ
8 2 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
9 7 8 npcand ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - B + B = A
10 9 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - B + B < C + B ↔ A < C + B
11 6 10 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ A < C + B