Description: A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | iccvolcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccmbl | |
|
2 | mblvol | |
|
3 | 1 2 | syl | |
4 | rexr | |
|
5 | rexr | |
|
6 | icc0 | |
|
7 | 4 5 6 | syl2an | |
8 | 7 | biimpar | |
9 | fveq2 | |
|
10 | ovol0 | |
|
11 | 9 10 | eqtrdi | |
12 | 0re | |
|
13 | 11 12 | eqeltrdi | |
14 | 8 13 | syl | |
15 | ovolicc | |
|
16 | 15 | 3expa | |
17 | resubcl | |
|
18 | 17 | ancoms | |
19 | 18 | adantr | |
20 | 16 19 | eqeltrd | |
21 | simpr | |
|
22 | simpl | |
|
23 | 14 20 21 22 | ltlecasei | |
24 | 3 23 | eqeltrd | |