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