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 ⊢ φ → A ∈ ℝ
iccsuble.2 ⊢ φ → B ∈ ℝ
iccsuble.3 ⊢ φ → C ∈ A B
iccsuble.4 ⊢ φ → D ∈ A B
Assertion iccsuble ⊢ φ → C − D ≤ B − A

Proof

Step Hyp Ref Expression
1 iccsuble.1 ⊢ φ → A ∈ ℝ
2 iccsuble.2 ⊢ φ → B ∈ ℝ
3 iccsuble.3 ⊢ φ → C ∈ A B
4 iccsuble.4 ⊢ φ → D ∈ A B
5 eliccre ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → C ∈ ℝ
6 1 2 3 5 syl3anc ⊢ φ → C ∈ ℝ
7 eliccre ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ D ∈ A B → D ∈ ℝ
8 1 2 4 7 syl3anc ⊢ φ → D ∈ ℝ
9 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
10 1 2 9 syl2anc ⊢ φ → C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
11 3 10 mpbid ⊢ φ → C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
12 11 simp3d ⊢ φ → C ≤ B
13 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → D ∈ A B ↔ D ∈ ℝ ∧ A ≤ D ∧ D ≤ B
14 1 2 13 syl2anc ⊢ φ → D ∈ A B ↔ D ∈ ℝ ∧ A ≤ D ∧ D ≤ B
15 4 14 mpbid ⊢ φ → D ∈ ℝ ∧ A ≤ D ∧ D ≤ B
16 15 simp2d ⊢ φ → A ≤ D
17 6 1 2 8 12 16 le2subd ⊢ φ → C − D ≤ B − A