Metamath Proof Explorer


Theorem iccvolcl

Description: A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion iccvolcl ABvolAB

Proof

Step Hyp Ref Expression
1 iccmbl ABABdomvol
2 mblvol ABdomvolvolAB=vol*AB
3 1 2 syl ABvolAB=vol*AB
4 rexr AA*
5 rexr BB*
6 icc0 A*B*AB=B<A
7 4 5 6 syl2an ABAB=B<A
8 7 biimpar ABB<AAB=
9 fveq2 AB=vol*AB=vol*
10 ovol0 vol*=0
11 9 10 eqtrdi AB=vol*AB=0
12 0re 0
13 11 12 eqeltrdi AB=vol*AB
14 8 13 syl ABB<Avol*AB
15 ovolicc ABABvol*AB=BA
16 15 3expa ABABvol*AB=BA
17 resubcl BABA
18 17 ancoms ABBA
19 18 adantr ABABBA
20 16 19 eqeltrd ABABvol*AB
21 simpr ABB
22 simpl ABA
23 14 20 21 22 ltlecasei ABvol*AB
24 3 23 eqeltrd ABvolAB