# Metamath Proof Explorer

## Theorem abs3lem

Description: Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999)

Ref Expression
Assertion abs3lem ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\to \left(\left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\to \left|{A}-{B}\right|<{D}\right)$

### Proof

Step Hyp Ref Expression
1 simplll ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {A}\in ℂ$
2 simpllr ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {B}\in ℂ$
3 1 2 subcld ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {A}-{B}\in ℂ$
4 abscl ${⊢}{A}-{B}\in ℂ\to \left|{A}-{B}\right|\in ℝ$
5 3 4 syl ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{B}\right|\in ℝ$
6 simplrl ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {C}\in ℂ$
7 1 6 subcld ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {A}-{C}\in ℂ$
8 abscl ${⊢}{A}-{C}\in ℂ\to \left|{A}-{C}\right|\in ℝ$
9 7 8 syl ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{C}\right|\in ℝ$
10 6 2 subcld ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {C}-{B}\in ℂ$
11 abscl ${⊢}{C}-{B}\in ℂ\to \left|{C}-{B}\right|\in ℝ$
12 10 11 syl ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{C}-{B}\right|\in ℝ$
13 9 12 readdcld ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{C}\right|+\left|{C}-{B}\right|\in ℝ$
14 simplrr ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to {D}\in ℝ$
15 abs3dif ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left|{A}-{B}\right|\le \left|{A}-{C}\right|+\left|{C}-{B}\right|$
16 1 2 6 15 syl3anc ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{B}\right|\le \left|{A}-{C}\right|+\left|{C}-{B}\right|$
17 simprl ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{C}\right|<\frac{{D}}{2}$
18 simprr ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{C}-{B}\right|<\frac{{D}}{2}$
19 9 12 14 17 18 lt2halvesd ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{C}\right|+\left|{C}-{B}\right|<{D}$
20 5 13 14 16 19 lelttrd ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\wedge \left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\right)\to \left|{A}-{B}\right|<{D}$
21 20 ex ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℝ\right)\right)\to \left(\left(\left|{A}-{C}\right|<\frac{{D}}{2}\wedge \left|{C}-{B}\right|<\frac{{D}}{2}\right)\to \left|{A}-{B}\right|<{D}\right)$