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 φCAB
iccsuble.4 φDAB
Assertion iccsuble φCDBA

Proof

Step Hyp Ref Expression
1 iccsuble.1 φA
2 iccsuble.2 φB
3 iccsuble.3 φCAB
4 iccsuble.4 φDAB
5 eliccre ABCABC
6 1 2 3 5 syl3anc φC
7 eliccre ABDABD
8 1 2 4 7 syl3anc φD
9 elicc2 ABCABCACCB
10 1 2 9 syl2anc φCABCACCB
11 3 10 mpbid φCACCB
12 11 simp3d φCB
13 elicc2 ABDABDADDB
14 1 2 13 syl2anc φDABDADDB
15 4 14 mpbid φDADDB
16 15 simp2d φAD
17 6 1 2 8 12 16 le2subd φCDBA