Metamath Proof Explorer

Theorem ovolicc

Description: The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolicc 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )

Proof

Step Hyp Ref Expression
1 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
2 1 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( A [,] B ) C_ RR )
3 ovolcl 
 |-  ( ( A [,] B ) C_ RR -> ( vol* ` ( A [,] B ) ) e. RR* )
4 2 3 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) e. RR* )
5 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> B e. RR )
6 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A e. RR )
7 5 6 resubcld 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( B - A ) e. RR )
8 7 rexrd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( B - A ) e. RR* )
9 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ B )
10 eqeq1 
 |-  ( m = n -> ( m = 1 <-> n = 1 ) )
11 10 ifbid 
 |-  ( m = n -> if ( m = 1 , <. A , B >. , <. 0 , 0 >. ) = if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) )
12 11 cbvmptv 
 |-  ( m e. NN |-> if ( m = 1 , <. A , B >. , <. 0 , 0 >. ) ) = ( n e. NN |-> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) )
13 6 5 9 12 ovolicc1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) <_ ( B - A ) )
14 eqeq1 
 |-  ( z = y -> ( z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <-> y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
15 14 anbi2d 
 |-  ( z = y -> ( ( ( A [,] B ) C_ U. ran ( (,) o. f ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> ( ( A [,] B ) C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
16 15 rexbidv 
 |-  ( z = y -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A [,] B ) C_ U. ran ( (,) o. f ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A [,] B ) C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
17 16 cbvrabv 
 |-  { z e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A [,] B ) C_ U. ran ( (,) o. f ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A [,] B ) C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
18 6 5 9 17 ovolicc2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( B - A ) <_ ( vol* ` ( A [,] B ) ) )
19 4 8 13 18 xrletrid 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )