Metamath Proof Explorer

Theorem ovolicc2

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

Ref Expression
Hypotheses ovolicc.1 
|- ( ph -> A e. RR )
ovolicc.2 
|- ( ph -> B e. RR )
ovolicc.3 
|- ( ph -> A <_ B )
ovolicc2.m 
|- M = { 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* , < ) ) }
Assertion ovolicc2 
|- ( ph -> ( B - A ) <_ ( vol* ` ( A [,] B ) ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 
 |-  ( ph -> A e. RR )
2 ovolicc.2 
 |-  ( ph -> B e. RR )
3 ovolicc.3 
 |-  ( ph -> A <_ B )
4 ovolicc2.m 
 |-  M = { 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* , < ) ) }
5 4 elovolm 
 |-  ( z e. M <-> 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* , < ) ) )
6 simprr 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ( A [,] B ) C_ U. ran ( (,) o. f ) )
7 unieq 
 |-  ( u = ran ( (,) o. f ) -> U. u = U. ran ( (,) o. f ) )
8 7 sseq2d 
 |-  ( u = ran ( (,) o. f ) -> ( ( A [,] B ) C_ U. u <-> ( A [,] B ) C_ U. ran ( (,) o. f ) ) )
9 pweq 
 |-  ( u = ran ( (,) o. f ) -> ~P u = ~P ran ( (,) o. f ) )
10 9 ineq1d 
 |-  ( u = ran ( (,) o. f ) -> ( ~P u i^i Fin ) = ( ~P ran ( (,) o. f ) i^i Fin ) )
11 10 rexeqdv 
 |-  ( u = ran ( (,) o. f ) -> ( E. v e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. v <-> E. v e. ( ~P ran ( (,) o. f ) i^i Fin ) ( A [,] B ) C_ U. v ) )
12 8 11 imbi12d 
 |-  ( u = ran ( (,) o. f ) -> ( ( ( A [,] B ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. v ) <-> ( ( A [,] B ) C_ U. ran ( (,) o. f ) -> E. v e. ( ~P ran ( (,) o. f ) i^i Fin ) ( A [,] B ) C_ U. v ) ) )
13 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
14 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
15 13 14 icccmp 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Comp )
16 1 2 15 syl2anc 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Comp )
17 retop 
 |-  ( topGen ` ran (,) ) e. Top
18 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
19 1 2 18 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
20 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
21 20 cmpsub 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR ) -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Comp <-> A. u e. ~P ( topGen ` ran (,) ) ( ( A [,] B ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. v ) ) )
22 17 19 21 sylancr 
 |-  ( ph -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Comp <-> A. u e. ~P ( topGen ` ran (,) ) ( ( A [,] B ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. v ) ) )
23 16 22 mpbid 
 |-  ( ph -> A. u e. ~P ( topGen ` ran (,) ) ( ( A [,] B ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. v ) )
24 23 adantr 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> A. u e. ~P ( topGen ` ran (,) ) ( ( A [,] B ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. v ) )
25 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
26 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
27 25 26 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
28 dffn3 
 |-  ( (,) Fn ( RR* X. RR* ) <-> (,) : ( RR* X. RR* ) --> ran (,) )
29 27 28 mpbi 
 |-  (,) : ( RR* X. RR* ) --> ran (,)
30 elovolmlem 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> f : NN --> ( <_ i^i ( RR X. RR ) ) )
31 30 bilani 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
32 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
33 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
34 32 33 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
35 fss 
 |-  ( ( f : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> f : NN --> ( RR* X. RR* ) )
36 31 34 35 sylancl 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> f : NN --> ( RR* X. RR* ) )
37 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ran (,) /\ f : NN --> ( RR* X. RR* ) ) -> ( (,) o. f ) : NN --> ran (,) )
38 29 36 37 sylancr 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( (,) o. f ) : NN --> ran (,) )
39 38 adantrr 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ( (,) o. f ) : NN --> ran (,) )
40 39 frnd 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ran ( (,) o. f ) C_ ran (,) )
41 retopbas 
 |-  ran (,) e. TopBases
42 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
43 41 42 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
44 40 43 sstrdi 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ran ( (,) o. f ) C_ ( topGen ` ran (,) ) )
45 fvex 
 |-  ( topGen ` ran (,) ) e. _V
46 45 elpw2 
 |-  ( ran ( (,) o. f ) e. ~P ( topGen ` ran (,) ) <-> ran ( (,) o. f ) C_ ( topGen ` ran (,) ) )
47 44 46 sylibr 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ran ( (,) o. f ) e. ~P ( topGen ` ran (,) ) )
48 12 24 47 rspcdva 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ( ( A [,] B ) C_ U. ran ( (,) o. f ) -> E. v e. ( ~P ran ( (,) o. f ) i^i Fin ) ( A [,] B ) C_ U. v ) )
49 6 48 mpd 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> E. v e. ( ~P ran ( (,) o. f ) i^i Fin ) ( A [,] B ) C_ U. v )
50 simprl 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> v e. ( ~P ran ( (,) o. f ) i^i Fin ) )
51 elin 
 |-  ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) <-> ( v e. ~P ran ( (,) o. f ) /\ v e. Fin ) )
52 50 51 sylib 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( v e. ~P ran ( (,) o. f ) /\ v e. Fin ) )
53 52 simprd 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> v e. Fin )
54 52 simpld 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> v e. ~P ran ( (,) o. f ) )
55 54 elpwid 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> v C_ ran ( (,) o. f ) )
56 55 sseld 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( t e. v -> t e. ran ( (,) o. f ) ) )
57 38 ffnd 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( (,) o. f ) Fn NN )
58 57 adantr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( (,) o. f ) Fn NN )
59 fvelrnb 
 |-  ( ( (,) o. f ) Fn NN -> ( t e. ran ( (,) o. f ) <-> E. k e. NN ( ( (,) o. f ) ` k ) = t ) )
60 58 59 syl 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( t e. ran ( (,) o. f ) <-> E. k e. NN ( ( (,) o. f ) ` k ) = t ) )
61 56 60 sylibd 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( t e. v -> E. k e. NN ( ( (,) o. f ) ` k ) = t ) )
62 61 ralrimiv 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> A. t e. v E. k e. NN ( ( (,) o. f ) ` k ) = t )
63 fveqeq2 
 |-  ( k = ( g ` t ) -> ( ( ( (,) o. f ) ` k ) = t <-> ( ( (,) o. f ) ` ( g ` t ) ) = t ) )
64 63 ac6sfi 
 |-  ( ( v e. Fin /\ A. t e. v E. k e. NN ( ( (,) o. f ) ` k ) = t ) -> E. g ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) )
65 53 62 64 syl2anc 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> E. g ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) )
66 1 ad2antrr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> A e. RR )
67 2 ad2antrr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> B e. RR )
68 3 ad2antrr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> A <_ B )
69 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
70 31 adantr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
71 simprll 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> v e. ( ~P ran ( (,) o. f ) i^i Fin ) )
72 simprlr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> ( A [,] B ) C_ U. v )
73 simprrl 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> g : v --> NN )
74 simprrr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t )
75 2fveq3 
 |-  ( t = x -> ( ( (,) o. f ) ` ( g ` t ) ) = ( ( (,) o. f ) ` ( g ` x ) ) )
76 id 
 |-  ( t = x -> t = x )
77 75 76 eqeq12d 
 |-  ( t = x -> ( ( ( (,) o. f ) ` ( g ` t ) ) = t <-> ( ( (,) o. f ) ` ( g ` x ) ) = x ) )
78 77 rspccva 
 |-  ( ( A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t /\ x e. v ) -> ( ( (,) o. f ) ` ( g ` x ) ) = x )
79 74 78 sylan 
 |-  ( ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) /\ x e. v ) -> ( ( (,) o. f ) ` ( g ` x ) ) = x )
80 eqid 
 |-  { u e. v | ( u i^i ( A [,] B ) ) =/= (/) } = { u e. v | ( u i^i ( A [,] B ) ) =/= (/) }
81 66 67 68 69 70 71 72 73 79 80 ovolicc2lem5 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) /\ ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) ) ) -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
82 81 expr 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
83 82 exlimdv 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( E. g ( g : v --> NN /\ A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t ) -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
84 65 83 mpd 
 |-  ( ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) /\ ( A [,] B ) C_ U. v ) ) -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
85 84 rexlimdvaa 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( E. v e. ( ~P ran ( (,) o. f ) i^i Fin ) ( A [,] B ) C_ U. v -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
86 85 adantrr 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ( E. v e. ( ~P ran ( (,) o. f ) i^i Fin ) ( A [,] B ) C_ U. v -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
87 49 86 mpd 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
88 breq2 
 |-  ( z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) -> ( ( B - A ) <_ z <-> ( B - A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
89 87 88 syl5ibrcom 
 |-  ( ( ph /\ ( 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* , < ) -> ( B - A ) <_ z ) )
90 89 expr 
 |-  ( ( ph /\ 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* , < ) -> ( B - A ) <_ z ) ) )
91 90 impd 
 |-  ( ( ph /\ 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* , < ) ) -> ( B - A ) <_ z ) )
92 91 rexlimdva 
 |-  ( ph -> ( 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* , < ) ) -> ( B - A ) <_ z ) )
93 5 92 biimtrid 
 |-  ( ph -> ( z e. M -> ( B - A ) <_ z ) )
94 93 ralrimiv 
 |-  ( ph -> A. z e. M ( B - A ) <_ z )
95 4 ssrab3 
 |-  M C_ RR*
96 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
97 96 rexrd 
 |-  ( ph -> ( B - A ) e. RR* )
98 infxrgelb 
 |-  ( ( M C_ RR* /\ ( B - A ) e. RR* ) -> ( ( B - A ) <_ inf ( M , RR* , < ) <-> A. z e. M ( B - A ) <_ z ) )
99 95 97 98 sylancr 
 |-  ( ph -> ( ( B - A ) <_ inf ( M , RR* , < ) <-> A. z e. M ( B - A ) <_ z ) )
100 94 99 mpbird 
 |-  ( ph -> ( B - A ) <_ inf ( M , RR* , < ) )
101 4 ovolval 
 |-  ( ( A [,] B ) C_ RR -> ( vol* ` ( A [,] B ) ) = inf ( M , RR* , < ) )
102 19 101 syl 
 |-  ( ph -> ( vol* ` ( A [,] B ) ) = inf ( M , RR* , < ) )
103 100 102 breqtrrd 
 |-  ( ph -> ( B - A ) <_ ( vol* ` ( A [,] B ) ) )