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

Metamath Proof Explorer

Theorem iccsuble

Description: An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iccsuble.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
iccsuble.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
iccsuble.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
iccsuble.4 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 [,] 𝐵 ) )
Assertion iccsuble ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐵 − 𝐴 ) )

Proof

Step Hyp Ref Expression
1 iccsuble.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 iccsuble.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 iccsuble.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
4 iccsuble.4 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 [,] 𝐵 ) )
5 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℝ )
6 1 2 3 5 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐷 ∈ ℝ )
8 1 2 4 7 syl3anc ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
9 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
11 3 10 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) )
12 11 simp3d ⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
13 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) )
14 1 2 13 syl2anc ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) )
15 4 14 mpbid ⊢ ( 𝜑 → ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 ≤ 𝐵 ) )
16 15 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝐷 )
17 6 1 2 8 12 16 le2subd ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐵 − 𝐴 ) )