Metamath Proof Explorer

Theorem ovollb2

Description: It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb ). (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypothesis ovollb2.1 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
Assertion ovollb2 
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovollb2.1 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
2 simpr 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> A C_ U. ran ( [,] o. F ) )
3 ovolficcss 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )
4 3 adantr 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> U. ran ( [,] o. F ) C_ RR )
5 2 4 sstrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> A C_ RR )
6 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
7 5 6 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ( vol* ` A ) e. RR* )
8 7 adantr 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) = +oo ) -> ( vol* ` A ) e. RR* )
9 pnfge 
 |-  ( ( vol* ` A ) e. RR* -> ( vol* ` A ) <_ +oo )
10 8 9 syl 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) = +oo ) -> ( vol* ` A ) <_ +oo )
11 simpr 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) = +oo ) -> sup ( ran S , RR* , < ) = +oo )
12 10 11 breqtrrd 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) = +oo ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )
13 eqid 
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
14 13 1 ovolsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
15 14 adantr 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> S : NN --> ( 0 [,) +oo ) )
16 15 frnd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ran S C_ ( 0 [,) +oo ) )
17 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
18 16 17 sstrdi 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ran S C_ RR )
19 1nn 
 |-  1 e. NN
20 15 fdmd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> dom S = NN )
21 19 20 eleqtrrid 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> 1 e. dom S )
22 21 ne0d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> dom S =/= (/) )
23 dm0rn0 
 |-  ( dom S = (/) <-> ran S = (/) )
24 23 necon3bii 
 |-  ( dom S =/= (/) <-> ran S =/= (/) )
25 22 24 sylib 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ran S =/= (/) )
26 supxrre2 
 |-  ( ( ran S C_ RR /\ ran S =/= (/) ) -> ( sup ( ran S , RR* , < ) e. RR <-> sup ( ran S , RR* , < ) =/= +oo ) )
27 18 25 26 syl2anc 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ( sup ( ran S , RR* , < ) e. RR <-> sup ( ran S , RR* , < ) =/= +oo ) )
28 27 biimpar 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) =/= +oo ) -> sup ( ran S , RR* , < ) e. RR )
29 2fveq3 
 |-  ( m = n -> ( 1st ` ( F ` m ) ) = ( 1st ` ( F ` n ) ) )
30 oveq2 
 |-  ( m = n -> ( 2 ^ m ) = ( 2 ^ n ) )
31 30 oveq2d 
 |-  ( m = n -> ( ( x / 2 ) / ( 2 ^ m ) ) = ( ( x / 2 ) / ( 2 ^ n ) ) )
32 29 31 oveq12d 
 |-  ( m = n -> ( ( 1st ` ( F ` m ) ) - ( ( x / 2 ) / ( 2 ^ m ) ) ) = ( ( 1st ` ( F ` n ) ) - ( ( x / 2 ) / ( 2 ^ n ) ) ) )
33 2fveq3 
 |-  ( m = n -> ( 2nd ` ( F ` m ) ) = ( 2nd ` ( F ` n ) ) )
34 33 31 oveq12d 
 |-  ( m = n -> ( ( 2nd ` ( F ` m ) ) + ( ( x / 2 ) / ( 2 ^ m ) ) ) = ( ( 2nd ` ( F ` n ) ) + ( ( x / 2 ) / ( 2 ^ n ) ) ) )
35 32 34 opeq12d 
 |-  ( m = n -> <. ( ( 1st ` ( F ` m ) ) - ( ( x / 2 ) / ( 2 ^ m ) ) ) , ( ( 2nd ` ( F ` m ) ) + ( ( x / 2 ) / ( 2 ^ m ) ) ) >. = <. ( ( 1st ` ( F ` n ) ) - ( ( x / 2 ) / ( 2 ^ n ) ) ) , ( ( 2nd ` ( F ` n ) ) + ( ( x / 2 ) / ( 2 ^ n ) ) ) >. )
36 35 cbvmptv 
 |-  ( m e. NN |-> <. ( ( 1st ` ( F ` m ) ) - ( ( x / 2 ) / ( 2 ^ m ) ) ) , ( ( 2nd ` ( F ` m ) ) + ( ( x / 2 ) / ( 2 ^ m ) ) ) >. ) = ( n e. NN |-> <. ( ( 1st ` ( F ` n ) ) - ( ( x / 2 ) / ( 2 ^ n ) ) ) , ( ( 2nd ` ( F ` n ) ) + ( ( x / 2 ) / ( 2 ^ n ) ) ) >. )
37 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. ( ( 1st ` ( F ` m ) ) - ( ( x / 2 ) / ( 2 ^ m ) ) ) , ( ( 2nd ` ( F ` m ) ) + ( ( x / 2 ) / ( 2 ^ m ) ) ) >. ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. ( ( 1st ` ( F ` m ) ) - ( ( x / 2 ) / ( 2 ^ m ) ) ) , ( ( 2nd ` ( F ` m ) ) + ( ( x / 2 ) / ( 2 ^ m ) ) ) >. ) ) )
38 simplll 
 |-  ( ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) /\ x e. RR+ ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
39 simpllr 
 |-  ( ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) /\ x e. RR+ ) -> A C_ U. ran ( [,] o. F ) )
40 simpr 
 |-  ( ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) /\ x e. RR+ ) -> x e. RR+ )
41 simplr 
 |-  ( ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) /\ x e. RR+ ) -> sup ( ran S , RR* , < ) e. RR )
42 1 36 37 38 39 40 41 ovollb2lem 
 |-  ( ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) /\ x e. RR+ ) -> ( vol* ` A ) <_ ( sup ( ran S , RR* , < ) + x ) )
43 42 ralrimiva 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) -> A. x e. RR+ ( vol* ` A ) <_ ( sup ( ran S , RR* , < ) + x ) )
44 xralrple 
 |-  ( ( ( vol* ` A ) e. RR* /\ sup ( ran S , RR* , < ) e. RR ) -> ( ( vol* ` A ) <_ sup ( ran S , RR* , < ) <-> A. x e. RR+ ( vol* ` A ) <_ ( sup ( ran S , RR* , < ) + x ) ) )
45 7 44 sylan 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) -> ( ( vol* ` A ) <_ sup ( ran S , RR* , < ) <-> A. x e. RR+ ( vol* ` A ) <_ ( sup ( ran S , RR* , < ) + x ) ) )
46 43 45 mpbird 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) e. RR ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )
47 28 46 syldan 
 |-  ( ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) /\ sup ( ran S , RR* , < ) =/= +oo ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )
48 12 47 pm2.61dane 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. F ) ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )