Metamath Proof Explorer

Theorem ltaddsublt

Description: Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 ltadd2 ⊢B∈ℝ∧C∈ℝ∧A∈ℝ→B<C↔A+B<A+C
2 1 3comr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<C↔A+B<A+C
3 readdcl ⊢A∈ℝ∧B∈ℝ→A+B∈ℝ
4 3 3adant3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+B∈ℝ
5 simp3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈ℝ
6 simp1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℝ
7 4 5 6 ltsubaddd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+B-C<A↔A+B<A+C
8 2 7 bitr4d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<C↔A+B-C<A