# Metamath Proof Explorer

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

Ref Expression
Assertion ltaddsub ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}+{B}<{C}↔{A}<{C}-{B}\right)$

### Proof

Step Hyp Ref Expression
1 lesubadd ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\wedge {A}\in ℝ\right)\to \left({C}-{B}\le {A}↔{C}\le {A}+{B}\right)$
2 1 3com13 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}-{B}\le {A}↔{C}\le {A}+{B}\right)$
3 resubcl ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\right)\to {C}-{B}\in ℝ$
4 lenlt ${⊢}\left({C}-{B}\in ℝ\wedge {A}\in ℝ\right)\to \left({C}-{B}\le {A}↔¬{A}<{C}-{B}\right)$
5 3 4 stoic3 ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\wedge {A}\in ℝ\right)\to \left({C}-{B}\le {A}↔¬{A}<{C}-{B}\right)$
6 5 3com13 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}-{B}\le {A}↔¬{A}<{C}-{B}\right)$
7 readdcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}+{B}\in ℝ$
8 lenlt ${⊢}\left({C}\in ℝ\wedge {A}+{B}\in ℝ\right)\to \left({C}\le {A}+{B}↔¬{A}+{B}<{C}\right)$
9 7 8 sylan2 ${⊢}\left({C}\in ℝ\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\to \left({C}\le {A}+{B}↔¬{A}+{B}<{C}\right)$
10 9 3impb ${⊢}\left({C}\in ℝ\wedge {A}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\le {A}+{B}↔¬{A}+{B}<{C}\right)$
11 10 3coml ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\le {A}+{B}↔¬{A}+{B}<{C}\right)$
12 2 6 11 3bitr3rd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(¬{A}+{B}<{C}↔¬{A}<{C}-{B}\right)$
13 12 con4bid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}+{B}<{C}↔{A}<{C}-{B}\right)$