Metamath Proof Explorer

Theorem ltaddsub2

Description: 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 recn ⊢ B ∈ ℝ → B ∈ ℂ
3 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
4 1 2 3 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B = B + A
5 4 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B = B + A
6 5 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B < C ↔ B + A < C
7 ltaddsub ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → B + A < C ↔ B < C − A
8 7 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + A < C ↔ B < C − A
9 6 8 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B < C ↔ B < C − A