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