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

Metamath Proof Explorer

Theorem absnpncan3d

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

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

Proof

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