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	⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐵 − 𝐴 ) )