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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
absnpncan3d.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
absnpncan3d.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
absnpncan3d.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
absnpncan3d.e ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
Assertion absnpncan3d ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐸 ) ) ≤ ( ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) + ( abs ‘ ( 𝐶 − 𝐷 ) ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 absnpncan3d.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 absnpncan3d.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 absnpncan3d.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 absnpncan3d.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5 absnpncan3d.e ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
6 1 5 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐸 ) ∈ ℂ )
7 6 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐸 ) ) ∈ ℝ )
8 1 4 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) ∈ ℂ )
9 8 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐷 ) ) ∈ ℝ )
10 4 5 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐸 ) ∈ ℂ )
11 10 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐷 − 𝐸 ) ) ∈ ℝ )
12 9 11 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐷 ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) ∈ ℝ )
13 1 2 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
14 13 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
15 2 3 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
16 15 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
17 14 16 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
18 3 4 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ∈ ℂ )
19 18 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 − 𝐷 ) ) ∈ ℝ )
20 17 19 readdcld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) + ( abs ‘ ( 𝐶 − 𝐷 ) ) ) ∈ ℝ )
21 20 11 readdcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) + ( abs ‘ ( 𝐶 − 𝐷 ) ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) ∈ ℝ )
22 1 5 4 abs3difd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐸 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐷 ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) )
23 1 2 3 4 absnpncan2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐷 ) ) ≤ ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) + ( abs ‘ ( 𝐶 − 𝐷 ) ) ) )
24 9 20 11 23 leadd1dd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐷 ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) ≤ ( ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) + ( abs ‘ ( 𝐶 − 𝐷 ) ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) )
25 7 12 21 22 24 letrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐸 ) ) ≤ ( ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) + ( abs ‘ ( 𝐶 − 𝐷 ) ) ) + ( abs ‘ ( 𝐷 − 𝐸 ) ) ) )