Metamath Proof Explorer

Theorem abs3lem

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

Ref Expression
Assertion abs3lem ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → 𝐴 ∈ ℂ )
2 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → 𝐵 ∈ ℂ )
3 1 2 subcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
4 abscl ⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
5 3 4 syl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
6 simplrl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → 𝐶 ∈ ℂ )
7 1 6 subcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
8 abscl ⊢ ( ( 𝐴 − 𝐶 ) ∈ ℂ → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
9 7 8 syl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
10 6 2 subcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
11 abscl ⊢ ( ( 𝐶 − 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐶 − 𝐵 ) ) ∈ ℝ )
12 10 11 syl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐶 − 𝐵 ) ) ∈ ℝ )
13 9 12 readdcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℝ )
14 simplrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → 𝐷 ∈ ℝ )
15 abs3dif ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) )
16 1 2 6 15 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) )
17 simprl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) )
18 simprr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) )
19 9 12 14 17 18 lt2halvesd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) < 𝐷 )
20 5 13 14 16 19 lelttrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝐷 )
21 20 ex ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝐷 ) )