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

Proof

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