Metamath Proof Explorer

Theorem ltaddsub

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

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

Proof

Step Hyp Ref Expression
1 lesubadd ⊢C∈ℝ∧B∈ℝ∧A∈ℝ→C−B≤A↔C≤A+B
2 1 3com13 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C−B≤A↔C≤A+B
3 resubcl ⊢C∈ℝ∧B∈ℝ→C−B∈ℝ
4 lenlt ⊢C−B∈ℝ∧A∈ℝ→C−B≤A↔¬A<C−B
5 3 4 stoic3 ⊢C∈ℝ∧B∈ℝ∧A∈ℝ→C−B≤A↔¬A<C−B
6 5 3com13 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C−B≤A↔¬A<C−B
7 readdcl ⊢A∈ℝ∧B∈ℝ→A+B∈ℝ
8 lenlt ⊢C∈ℝ∧A+B∈ℝ→C≤A+B↔¬A+B<C
9 7 8 sylan2 ⊢C∈ℝ∧A∈ℝ∧B∈ℝ→C≤A+B↔¬A+B<C
10 9 3impb ⊢C∈ℝ∧A∈ℝ∧B∈ℝ→C≤A+B↔¬A+B<C
11 10 3coml ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C≤A+B↔¬A+B<C
12 2 6 11 3bitr3rd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→¬A+B<C↔¬A<C−B
13 12 con4bid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+B<C↔A<C−B