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 simpr 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
31 elovolmlem 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> f : NN --> ( <_ i^i ( RR X. RR ) ) )
32 30 31 sylib 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
33 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
34 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
35 33 34 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
36 fss 
 |-  ( ( f : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> f : NN --> ( RR* X. RR* ) )
37 32 35 36 sylancl 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> f : NN --> ( RR* X. RR* ) )
38 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ran (,) /\ f : NN --> ( RR* X. RR* ) ) -> ( (,) o. f ) : NN --> ran (,) )
39 29 37 38 sylancr 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( (,) o. f ) : NN --> ran (,) )
40 39 adantrr 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ( (,) o. f ) : NN --> ran (,) )
41 40 frnd 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ran ( (,) o. f ) C_ ran (,) )
42 retopbas 
 |-  ran (,) e. TopBases
43 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
44 42 43 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
45 41 44 sstrdi 
 |-  ( ( ph /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A [,] B ) C_ U. ran ( (,) o. f ) ) ) -> ran ( (,) o. f ) C_ ( topGen ` ran (,) ) )
46 fvex 
 |-  ( topGen ` ran (,) ) e. _V
47 46 elpw2 
 |-  ( ran ( (,) o. f ) e. ~P ( topGen ` ran (,) ) <-> ran ( (,) o. f ) C_ ( topGen ` ran (,) ) )
48 45 47 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 (,) ) )
49 12 24 48 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 ) )
50 6 49 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 )
51 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 ) )
52 elin 
 |-  ( v e. ( ~P ran ( (,) o. f ) i^i Fin ) <-> ( v e. ~P ran ( (,) o. f ) /\ v e. Fin ) )
53 51 52 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 ) )
54 53 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 )
55 53 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 ) )
56 55 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 ) )
57 56 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 ) ) )
58 39 ffnd 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( (,) o. f ) Fn NN )
59 58 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 )
60 fvelrnb 
 |-  ( ( (,) o. f ) Fn NN -> ( t e. ran ( (,) o. f ) <-> E. k e. NN ( ( (,) o. f ) ` k ) = t ) )
61 59 60 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 ) )
62 57 61 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 ) )
63 62 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 )
64 fveqeq2 
 |-  ( k = ( g ` t ) -> ( ( ( (,) o. f ) ` k ) = t <-> ( ( (,) o. f ) ` ( g ` t ) ) = t ) )
65 64 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 ) )
66 54 63 65 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 ) )
67 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 )
68 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 )
69 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 )
70 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
71 32 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 ) ) )
72 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 ) )
73 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 )
74 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 )
75 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 )
76 2fveq3 
 |-  ( t = x -> ( ( (,) o. f ) ` ( g ` t ) ) = ( ( (,) o. f ) ` ( g ` x ) ) )
77 id 
 |-  ( t = x -> t = x )
78 76 77 eqeq12d 
 |-  ( t = x -> ( ( ( (,) o. f ) ` ( g ` t ) ) = t <-> ( ( (,) o. f ) ` ( g ` x ) ) = x ) )
79 78 rspccva 
 |-  ( ( A. t e. v ( ( (,) o. f ) ` ( g ` t ) ) = t /\ x e. v ) -> ( ( (,) o. f ) ` ( g ` x ) ) = x )
80 75 79 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 )
81 eqid 
 |-  { u e. v | ( u i^i ( A [,] B ) ) =/= (/) } = { u e. v | ( u i^i ( A [,] B ) ) =/= (/) }
82 67 68 69 70 71 72 73 74 80 81 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* , < ) )
83 82 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* , < ) ) )
84 83 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* , < ) ) )
85 66 84 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* , < ) )
86 85 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* , < ) ) )
87 86 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* , < ) ) )
88 50 87 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* , < ) )
89 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* , < ) ) )
90 88 89 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 ) )
91 90 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 ) ) )
92 91 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 ) )
93 92 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 ) )
94 5 93 syl5bi 
 |-  ( ph -> ( z e. M -> ( B - A ) <_ z ) )
95 94 ralrimiv 
 |-  ( ph -> A. z e. M ( B - A ) <_ z )
96 4 ssrab3 
 |-  M C_ RR*
97 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
98 97 rexrd 
 |-  ( ph -> ( B - A ) e. RR* )
99 infxrgelb 
 |-  ( ( M C_ RR* /\ ( B - A ) e. RR* ) -> ( ( B - A ) <_ inf ( M , RR* , < ) <-> A. z e. M ( B - A ) <_ z ) )
100 96 98 99 sylancr 
 |-  ( ph -> ( ( B - A ) <_ inf ( M , RR* , < ) <-> A. z e. M ( B - A ) <_ z ) )
101 95 100 mpbird 
 |-  ( ph -> ( B - A ) <_ inf ( M , RR* , < ) )
102 4 ovolval 
 |-  ( ( A [,] B ) C_ RR -> ( vol* ` ( A [,] B ) ) = inf ( M , RR* , < ) )
103 19 102 syl 
 |-  ( ph -> ( vol* ` ( A [,] B ) ) = inf ( M , RR* , < ) )
104 101 103 breqtrrd 
 |-  ( ph -> ( B - A ) <_ ( vol* ` ( A [,] B ) ) )