Metamath Proof Explorer

Theorem ovolgelb

Description: The outer volume is the greatest lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypothesis ovolgelb.1 
|- S = seq 1 ( + , ( ( abs o. - ) o. g ) )
Assertion ovolgelb 
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) )

Proof

Step Hyp Ref Expression
1 ovolgelb.1 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. g ) )
2 simp2 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( vol* ` A ) e. RR )
3 simp3 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> B e. RR+ )
4 2 3 ltaddrpd 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( vol* ` A ) < ( ( vol* ` A ) + B ) )
5 3 rpred 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> B e. RR )
6 2 5 readdcld 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( ( vol* ` A ) + B ) e. RR )
7 2 6 ltnled 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( ( vol* ` A ) < ( ( vol* ` A ) + B ) <-> -. ( ( vol* ` A ) + B ) <_ ( vol* ` A ) ) )
8 4 7 mpbid 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> -. ( ( vol* ` A ) + B ) <_ ( vol* ` A ) )
9 eqid 
 |-  { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } = { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) }
10 9 ovolval 
 |-  ( A C_ RR -> ( vol* ` A ) = inf ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) )
11 10 3ad2ant1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( vol* ` A ) = inf ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) )
12 11 breq2d 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( ( ( vol* ` A ) + B ) <_ ( vol* ` A ) <-> ( ( vol* ` A ) + B ) <_ inf ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) ) )
13 ssrab2 
 |-  { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } C_ RR*
14 6 rexrd 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( ( vol* ` A ) + B ) e. RR* )
15 infxrgelb 
 |-  ( ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } C_ RR* /\ ( ( vol* ` A ) + B ) e. RR* ) -> ( ( ( vol* ` A ) + B ) <_ inf ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) <-> A. x e. { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } ( ( vol* ` A ) + B ) <_ x ) )
16 13 14 15 sylancr 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( ( ( vol* ` A ) + B ) <_ inf ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) <-> A. x e. { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } ( ( vol* ` A ) + B ) <_ x ) )
17 eqeq1 
 |-  ( y = x -> ( y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <-> x = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) )
18 1 rneqi 
 |-  ran S = ran seq 1 ( + , ( ( abs o. - ) o. g ) )
19 18 supeq1i 
 |-  sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < )
20 19 eqeq2i 
 |-  ( x = sup ( ran S , RR* , < ) <-> x = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) )
21 17 20 bitr4di 
 |-  ( y = x -> ( y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <-> x = sup ( ran S , RR* , < ) ) )
22 21 anbi2d 
 |-  ( y = x -> ( ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) <-> ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) ) )
23 22 rexbidv 
 |-  ( y = x -> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) <-> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) ) )
24 23 ralrab 
 |-  ( A. x e. { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } ( ( vol* ` A ) + B ) <_ x <-> A. x e. RR* ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) )
25 ralcom 
 |-  ( A. x e. RR* A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) A. x e. RR* ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) )
26 r19.23v 
 |-  ( A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) )
27 26 ralbii 
 |-  ( A. x e. RR* A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> A. x e. RR* ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) )
28 ancomst 
 |-  ( ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> ( ( x = sup ( ran S , RR* , < ) /\ A C_ U. ran ( (,) o. g ) ) -> ( ( vol* ` A ) + B ) <_ x ) )
29 impexp 
 |-  ( ( ( x = sup ( ran S , RR* , < ) /\ A C_ U. ran ( (,) o. g ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> ( x = sup ( ran S , RR* , < ) -> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ x ) ) )
30 28 29 bitri 
 |-  ( ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> ( x = sup ( ran S , RR* , < ) -> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ x ) ) )
31 30 ralbii 
 |-  ( A. x e. RR* ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> A. x e. RR* ( x = sup ( ran S , RR* , < ) -> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ x ) ) )
32 elovolmlem 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> g : NN --> ( <_ i^i ( RR X. RR ) ) )
33 eqid 
 |-  ( ( abs o. - ) o. g ) = ( ( abs o. - ) o. g )
34 33 1 ovolsf 
 |-  ( g : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
35 32 34 sylbi 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> S : NN --> ( 0 [,) +oo ) )
36 35 frnd 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ran S C_ ( 0 [,) +oo ) )
37 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
38 36 37 sstrdi 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ran S C_ RR* )
39 supxrcl 
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
40 38 39 syl 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> sup ( ran S , RR* , < ) e. RR* )
41 breq2 
 |-  ( x = sup ( ran S , RR* , < ) -> ( ( ( vol* ` A ) + B ) <_ x <-> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
42 41 imbi2d 
 |-  ( x = sup ( ran S , RR* , < ) -> ( ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ x ) <-> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) ) )
43 42 ceqsralv 
 |-  ( sup ( ran S , RR* , < ) e. RR* -> ( A. x e. RR* ( x = sup ( ran S , RR* , < ) -> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ x ) ) <-> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) ) )
44 40 43 syl 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( A. x e. RR* ( x = sup ( ran S , RR* , < ) -> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ x ) ) <-> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) ) )
45 31 44 syl5bb 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( A. x e. RR* ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) ) )
46 45 ralbiia 
 |-  ( A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) A. x e. RR* ( ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
47 25 27 46 3bitr3i 
 |-  ( A. x e. RR* ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = sup ( ran S , RR* , < ) ) -> ( ( vol* ` A ) + B ) <_ x ) <-> A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
48 24 47 bitri 
 |-  ( A. x e. { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } ( ( vol* ` A ) + B ) <_ x <-> A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
49 16 48 bitr2di 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) <-> ( ( vol* ` A ) + B ) <_ inf ( { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) ) )
50 12 49 bitr4d 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( ( ( vol* ` A ) + B ) <_ ( vol* ` A ) <-> A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) ) )
51 8 50 mtbid 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> -. A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
52 rexanali 
 |-  ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) <-> -. A. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) -> ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
53 51 52 sylibr 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
54 xrltnle 
 |-  ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` A ) + B ) e. RR* ) -> ( sup ( ran S , RR* , < ) < ( ( vol* ` A ) + B ) <-> -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) )
55 xrltle 
 |-  ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` A ) + B ) e. RR* ) -> ( sup ( ran S , RR* , < ) < ( ( vol* ` A ) + B ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) )
56 54 55 sylbird 
 |-  ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` A ) + B ) e. RR* ) -> ( -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) )
57 40 14 56 syl2anr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) )
58 57 anim2d 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( A C_ U. ran ( (,) o. g ) /\ -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) -> ( A C_ U. ran ( (,) o. g ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) ) )
59 58 reximdva 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ -. ( ( vol* ` A ) + B ) <_ sup ( ran S , RR* , < ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) ) )
60 53 59 mpd 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ B e. RR+ ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + B ) ) )