Metamath Proof Explorer

Theorem abs3lem

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

Ref Expression
Assertion abs3lem ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ → A − C < D 2 ∧ C − B < D 2 → A − B < D

Proof

Step Hyp Ref Expression
1 simplll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A ∈ ℂ
2 simpllr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → B ∈ ℂ
3 1 2 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − B ∈ ℂ
4 abscl ⊢ A − B ∈ ℂ → A − B ∈ ℝ
5 3 4 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − B ∈ ℝ
6 simplrl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → C ∈ ℂ
7 1 6 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − C ∈ ℂ
8 abscl ⊢ A − C ∈ ℂ → A − C ∈ ℝ
9 7 8 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − C ∈ ℝ
10 6 2 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → C − B ∈ ℂ
11 abscl ⊢ C − B ∈ ℂ → C − B ∈ ℝ
12 10 11 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → C − B ∈ ℝ
13 9 12 readdcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − C + C − B ∈ ℝ
14 simplrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → D ∈ ℝ
15 abs3dif ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ≤ A − C + C − B
16 1 2 6 15 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − B ≤ A − C + C − B
17 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − C < D 2
18 simprr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → C − B < D 2
19 9 12 14 17 18 lt2halvesd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − C + C − B < D
20 5 13 14 16 19 lelttrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ ∧ A − C < D 2 ∧ C − B < D 2 → A − B < D
21 20 ex ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℝ → A − C < D 2 ∧ C − B < D 2 → A − B < D