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 
|- ( 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 ) )