Theorem absdifltd

Description: The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypotheses	absltd.1	$$⊢\phi \to A\in ℝ$$
	absltd.2	$$⊢\phi \to B\in ℝ$$
	absltd.3	$$⊢\phi \to C\in ℝ$$
Assertion	absdifltd	$$⊢\phi \to \left(\left|A-B\right|<C\leftrightarrow \left(B-C<A\wedge A<B+C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		absltd.1	$$⊢\phi \to A\in ℝ$$
2		absltd.2	$$⊢\phi \to B\in ℝ$$
3		absltd.3	$$⊢\phi \to C\in ℝ$$
4		absdiflt	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(\left|A-B\right|<C\leftrightarrow \left(B-C<A\wedge A<B+C\right)\right)$$
5	1 2 3 4	syl3anc	$$⊢\phi \to \left(\left|A-B\right|<C\leftrightarrow \left(B-C<A\wedge A<B+C\right)\right)$$