This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absnpncan2d

Description: Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses absnpncan2d.a ⊢ φ → A ∈ ℂ
absnpncan2d.b ⊢ φ → B ∈ ℂ
absnpncan2d.c ⊢ φ → C ∈ ℂ
absnpncan2d.d ⊢ φ → D ∈ ℂ
Assertion absnpncan2d ⊢ φ → A − D ≤ A − B + B − C + C − D

Proof

Step Hyp Ref Expression
1 absnpncan2d.a ⊢ φ → A ∈ ℂ
2 absnpncan2d.b ⊢ φ → B ∈ ℂ
3 absnpncan2d.c ⊢ φ → C ∈ ℂ
4 absnpncan2d.d ⊢ φ → D ∈ ℂ
5 1 4 subcld ⊢ φ → A − D ∈ ℂ
6 5 abscld ⊢ φ → A − D ∈ ℝ
7 1 3 subcld ⊢ φ → A − C ∈ ℂ
8 7 abscld ⊢ φ → A − C ∈ ℝ
9 3 4 subcld ⊢ φ → C − D ∈ ℂ
10 9 abscld ⊢ φ → C − D ∈ ℝ
11 8 10 readdcld ⊢ φ → A − C + C − D ∈ ℝ
12 1 2 subcld ⊢ φ → A − B ∈ ℂ
13 12 abscld ⊢ φ → A − B ∈ ℝ
14 2 3 subcld ⊢ φ → B − C ∈ ℂ
15 14 abscld ⊢ φ → B − C ∈ ℝ
16 13 15 readdcld ⊢ φ → A − B + B − C ∈ ℝ
17 16 10 readdcld ⊢ φ → A − B + B − C + C − D ∈ ℝ
18 1 4 3 abs3difd ⊢ φ → A − D ≤ A − C + C − D
19 1 3 2 abs3difd ⊢ φ → A − C ≤ A − B + B − C
20 8 16 10 19 leadd1dd ⊢ φ → A − C + C − D ≤ A − B + B − C + C − D
21 6 11 17 18 20 letrd ⊢ φ → A − D ≤ A − B + B − C + C − D