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	|- ( ph -> A e. RR )
	iccsuble.2	|- ( ph -> B e. RR )
	iccsuble.3	|- ( ph -> C e. ( A [,] B ) )
	iccsuble.4	|- ( ph -> D e. ( A [,] B ) )
Assertion	iccsuble	|- ( ph -> ( C - D ) <_ ( B - A ) )

Proof

Step	Hyp	Ref	Expression
1		iccsuble.1	|- ( ph -> A e. RR )
2		iccsuble.2	|- ( ph -> B e. RR )
3		iccsuble.3	|- ( ph -> C e. ( A [,] B ) )
4		iccsuble.4	|- ( ph -> D e. ( A [,] B ) )
5		eliccre	|- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> C e. RR )
6	1 2 3 5	syl3anc	|- ( ph -> C e. RR )
7		eliccre	|- ( ( A e. RR /\ B e. RR /\ D e. ( A [,] B ) ) -> D e. RR )
8	1 2 4 7	syl3anc	|- ( ph -> D e. RR )
9		elicc2	|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
10	1 2 9	syl2anc	|- ( ph -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
11	3 10	mpbid	|- ( ph -> ( C e. RR /\ A <_ C /\ C <_ B ) )
12	11	simp3d	|- ( ph -> C <_ B )
13		elicc2	|- ( ( A e. RR /\ B e. RR ) -> ( D e. ( A [,] B ) <-> ( D e. RR /\ A <_ D /\ D <_ B ) ) )
14	1 2 13	syl2anc	|- ( ph -> ( D e. ( A [,] B ) <-> ( D e. RR /\ A <_ D /\ D <_ B ) ) )
15	4 14	mpbid	|- ( ph -> ( D e. RR /\ A <_ D /\ D <_ B ) )
16	15	simp2d	|- ( ph -> A <_ D )
17	6 1 2 8 12 16	le2subd	|- ( ph -> ( C - D ) <_ ( B - A ) )