Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovnsubaddlem2 Structured version   Visualization version   Unicode version

Theorem ovnsubaddlem2 38387
Description:  (voln* `  X
) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
ovnsubaddlem2.x  |-  ( ph  ->  X  e.  Fin )
ovnsubaddlem2.n0  |-  ( ph  ->  X  =/=  (/) )
ovnsubaddlem2.a  |-  ( ph  ->  A : NN --> ~P ( RR  ^m  X ) )
ovnsubaddlem2.e  |-  ( ph  ->  E  e.  RR+ )
ovnsubaddlem2.z  |-  Z  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
ovnsubaddlem2.c  |-  C  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { l  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( l `  j
) ) `  k
) } )
ovnsubaddlem2.l  |-  L  =  ( h  e.  ( ( RR  X.  RR )  ^m  X )  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  h ) `
 k ) ) )
ovnsubaddlem2.d  |-  D  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  ( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } ) )
Assertion
Ref Expression
ovnsubaddlem2  |-  ( ph  ->  ( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
Distinct variable groups:    A, a,
e, i, j, n    A, k, l, a, i, j, n    z, A, a, i, j, k, n    C, a, e, i    D, a, e, i, j, n    D, k    E, a, e, i, j, n   
k, E    L, a,
e, i, j, n    X, a, e, i, j, n    h, X, k, i, j    X, l   
z, X    ph, a, e, i, j, n    ph, k
Allowed substitution hints:    ph( z, h, l)    A( h)    C( z, h, j, k, n, l)    D( z, h, l)    E( z, h, l)    L( z, h, k, l)    Z( z, e, h, i, j, k, n, a, l)

Proof of Theorem ovnsubaddlem2
Dummy variables  f 
g  m  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5873 . . . 4  |-  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  e. 
_V
2 nnenom 12190 . . . 4  |-  NN  ~~  om
31, 2axcc3 8865 . . 3  |-  E. g
( g  Fn  NN  /\ 
A. n  e.  NN  ( ( ( D `
 ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) )  =/=  (/)  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) ) )
4 simprl 763 . . . . . 6  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) ) )  -> 
g  Fn  NN )
5 nfv 1760 . . . . . . . . 9  |-  F/ n ph
6 nfra1 2768 . . . . . . . . 9  |-  F/ n A. n  e.  NN  ( ( ( D `
 ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) )  =/=  (/)  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
75, 6nfan 2010 . . . . . . . 8  |-  F/ n
( ph  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
8 rspa 2754 . . . . . . . . . . 11  |-  ( ( A. n  e.  NN  ( ( ( D `
 ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) )  =/=  (/)  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )  /\  n  e.  NN )  ->  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
98adantll 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. n  e.  NN  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  /\  n  e.  NN )  ->  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
10 ovnsubaddlem2.x . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  Fin )
1110adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  X  e. 
Fin )
12 ovnsubaddlem2.n0 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  =/=  (/) )
1312adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  X  =/=  (/) )
14 ovnsubaddlem2.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A : NN --> ~P ( RR  ^m  X ) )
1514adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  A : NN
--> ~P ( RR  ^m  X ) )
16 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
1715, 16ffvelrnd 6021 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  e. 
~P ( RR  ^m  X ) )
18 elpwi 3959 . . . . . . . . . . . . . . . . 17  |-  ( ( A `  n )  e.  ~P ( RR 
^m  X )  -> 
( A `  n
)  C_  ( RR  ^m  X ) )
1917, 18syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  ( RR  ^m  X ) )
20 ovnsubaddlem2.e . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR+ )
2120adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR+ )
22 nnnn0 10873 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  n  e.  NN0 )
23 2nn 10764 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  NN
2423a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN0  ->  2  e.  NN )
25 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN0  ->  n  e. 
NN0 )
26 nnexpcl 12282 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  NN  /\  n  e.  NN0 )  -> 
( 2 ^ n
)  e.  NN )
2724, 25, 26syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN0  ->  ( 2 ^ n )  e.  NN )
28 nnrp 11308 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2 ^ n )  e.  NN  ->  (
2 ^ n )  e.  RR+ )
2927, 28syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  ->  ( 2 ^ n )  e.  RR+ )
3022, 29syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
2 ^ n )  e.  RR+ )
3130adantl 468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2 ^ n )  e.  RR+ )
3221, 31rpdivcld 11355 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  e.  RR+ )
33 ovnsubaddlem2.c . . . . . . . . . . . . . . . 16  |-  C  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { l  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( l `  j
) ) `  k
) } )
34 ovnsubaddlem2.l . . . . . . . . . . . . . . . 16  |-  L  =  ( h  e.  ( ( RR  X.  RR )  ^m  X )  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  h ) `
 k ) ) )
35 ovnsubaddlem2.d . . . . . . . . . . . . . . . 16  |-  D  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  ( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } ) )
3611, 13, 19, 32, 33, 34, 35ovncvrrp 38380 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  E. i 
i  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) )
37 n0 3740 . . . . . . . . . . . . . . 15  |-  ( ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  <->  E. i  i  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
3836, 37sylibr 216 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/) )
3938adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  (
( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/) )
40 simpr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
4139, 40mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
4241ex 436 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
4342adantlr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. n  e.  NN  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  /\  n  e.  NN )  ->  (
( ( ( D `
 ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) )  =/=  (/)  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
449, 43mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  A. n  e.  NN  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  /\  n  e.  NN )  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
4544ex 436 . . . . . . . 8  |-  ( (
ph  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  (
n  e.  NN  ->  ( g `  n )  e.  ( ( D `
 ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) ) ) )
467, 45ralrimi 2787 . . . . . . 7  |-  ( (
ph  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )
4746adantrl 721 . . . . . 6  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) ) )  ->  A. n  e.  NN  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) )
484, 47jca 535 . . . . 5  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) ) )  -> 
( g  Fn  NN  /\ 
A. n  e.  NN  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) ) )
4948ex 436 . . . 4  |-  ( ph  ->  ( ( g  Fn  NN  /\  A. n  e.  NN  ( ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  (
g  Fn  NN  /\  A. n  e.  NN  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) ) ) )
5049eximdv 1763 . . 3  |-  ( ph  ->  ( E. g ( g  Fn  NN  /\  A. n  e.  NN  (
( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  =/=  (/)  ->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  E. g
( g  Fn  NN  /\ 
A. n  e.  NN  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) ) ) )
513, 50mpi 20 . 2  |-  ( ph  ->  E. g ( g  Fn  NN  /\  A. n  e.  NN  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) ) )
52 simpl 459 . . . . 5  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  ph )
53 simprl 763 . . . . 5  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  g  Fn  NN )
54 simprr 765 . . . . 5  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )
55 nnf1oxpnn 37466 . . . . . 6  |-  E. f 
f : NN -1-1-onto-> ( NN  X.  NN )
56 simpl1 1010 . . . . . . . . 9  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  ph )
57 simpl2 1011 . . . . . . . . 9  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  g  Fn  NN )
58 fveq2 5863 . . . . . . . . . . . . . 14  |-  ( q  =  n  ->  (
g `  q )  =  ( g `  n ) )
59 fveq2 5863 . . . . . . . . . . . . . . . 16  |-  ( q  =  n  ->  ( A `  q )  =  ( A `  n ) )
6059fveq2d 5867 . . . . . . . . . . . . . . 15  |-  ( q  =  n  ->  ( D `  ( A `  q ) )  =  ( D `  ( A `  n )
) )
61 oveq2 6296 . . . . . . . . . . . . . . . 16  |-  ( q  =  n  ->  (
2 ^ q )  =  ( 2 ^ n ) )
6261oveq2d 6304 . . . . . . . . . . . . . . 15  |-  ( q  =  n  ->  ( E  /  ( 2 ^ q ) )  =  ( E  /  (
2 ^ n ) ) )
6360, 62fveq12d 5869 . . . . . . . . . . . . . 14  |-  ( q  =  n  ->  (
( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) )  =  ( ( D `
 ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) ) )
6458, 63eleq12d 2522 . . . . . . . . . . . . 13  |-  ( q  =  n  ->  (
( g `  q
)  e.  ( ( D `  ( A `
 q ) ) `
 ( E  / 
( 2 ^ q
) ) )  <->  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )
6564cbvralv 3018 . . . . . . . . . . . 12  |-  ( A. q  e.  NN  (
g `  q )  e.  ( ( D `  ( A `  q ) ) `  ( E  /  ( 2 ^ q ) ) )  <->  A. n  e.  NN  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) )
6665biimpri 210 . . . . . . . . . . 11  |-  ( A. n  e.  NN  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  ->  A. q  e.  NN  ( g `  q
)  e.  ( ( D `  ( A `
 q ) ) `
 ( E  / 
( 2 ^ q
) ) ) )
67663ad2ant3 1030 . . . . . . . . . 10  |-  ( (
ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  ->  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )
6867adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )
69 simpr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  f : NN -1-1-onto-> ( NN  X.  NN ) )
7010adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  f : NN
-1-1-onto-> ( NN  X.  NN ) )  ->  X  e.  Fin )
71703ad2antl1 1169 . . . . . . . . . 10  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  X  e.  Fin )
7212adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  f : NN
-1-1-onto-> ( NN  X.  NN ) )  ->  X  =/=  (/) )
73723ad2antl1 1169 . . . . . . . . . 10  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  X  =/=  (/) )
7414adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  f : NN
-1-1-onto-> ( NN  X.  NN ) )  ->  A : NN --> ~P ( RR 
^m  X ) )
75743ad2antl1 1169 . . . . . . . . . 10  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  A : NN --> ~P ( RR 
^m  X ) )
7620adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  f : NN
-1-1-onto-> ( NN  X.  NN ) )  ->  E  e.  RR+ )
77763ad2antl1 1169 . . . . . . . . . 10  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  E  e.  RR+ )
78 ovnsubaddlem2.z . . . . . . . . . 10  |-  Z  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
79 coeq2 4992 . . . . . . . . . . . . . . 15  |-  ( h  =  i  ->  ( [,)  o.  h )  =  ( [,)  o.  i
) )
8079fveq1d 5865 . . . . . . . . . . . . . 14  |-  ( h  =  i  ->  (
( [,)  o.  h
) `  k )  =  ( ( [,) 
o.  i ) `  k ) )
8180fveq2d 5867 . . . . . . . . . . . . 13  |-  ( h  =  i  ->  ( vol `  ( ( [,) 
o.  h ) `  k ) )  =  ( vol `  (
( [,)  o.  i
) `  k )
) )
8281prodeq2ad 37666 . . . . . . . . . . . 12  |-  ( h  =  i  ->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  h ) `  k
) )  =  prod_ k  e.  X  ( vol `  ( ( [,)  o.  i ) `  k
) ) )
8382cbvmptv 4494 . . . . . . . . . . 11  |-  ( h  e.  ( ( RR 
X.  RR )  ^m  X )  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  h ) `  k
) ) )  =  ( i  e.  ( ( RR  X.  RR )  ^m  X )  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  i ) `
 k ) ) )
8434, 83eqtri 2472 . . . . . . . . . 10  |-  L  =  ( i  e.  ( ( RR  X.  RR )  ^m  X )  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  i ) `
 k ) ) )
8565biimpi 198 . . . . . . . . . . . . 13  |-  ( A. q  e.  NN  (
g `  q )  e.  ( ( D `  ( A `  q ) ) `  ( E  /  ( 2 ^ q ) ) )  ->  A. n  e.  NN  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) )
86853ad2ant3 1030 . . . . . . . . . . . 12  |-  ( (
ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  ->  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )
8786ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  (
g `  q )  e.  ( ( D `  ( A `  q ) ) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  /\  n  e.  NN )  ->  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )
88 simpr 463 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  (
g `  q )  e.  ( ( D `  ( A `  q ) ) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  /\  n  e.  NN )  ->  n  e.  NN )
89 rspa 2754 . . . . . . . . . . 11  |-  ( ( A. n  e.  NN  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  /\  n  e.  NN )  ->  ( g `  n
)  e.  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) ) )
9087, 88, 89syl2anc 666 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  (
g `  q )  e.  ( ( D `  ( A `  q ) ) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  /\  n  e.  NN )  ->  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
91 simpr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  f : NN -1-1-onto-> ( NN  X.  NN ) )
92 fveq2 5863 . . . . . . . . . . . . . 14  |-  ( q  =  m  ->  (
f `  q )  =  ( f `  m ) )
9392fveq2d 5867 . . . . . . . . . . . . 13  |-  ( q  =  m  ->  ( 1st `  ( f `  q ) )  =  ( 1st `  (
f `  m )
) )
9493fveq2d 5867 . . . . . . . . . . . 12  |-  ( q  =  m  ->  (
g `  ( 1st `  ( f `  q
) ) )  =  ( g `  ( 1st `  ( f `  m ) ) ) )
9592fveq2d 5867 . . . . . . . . . . . 12  |-  ( q  =  m  ->  ( 2nd `  ( f `  q ) )  =  ( 2nd `  (
f `  m )
) )
9694, 95fveq12d 5869 . . . . . . . . . . 11  |-  ( q  =  m  ->  (
( g `  ( 1st `  ( f `  q ) ) ) `
 ( 2nd `  (
f `  q )
) )  =  ( ( g `  ( 1st `  ( f `  m ) ) ) `
 ( 2nd `  (
f `  m )
) ) )
9796cbvmptv 4494 . . . . . . . . . 10  |-  ( q  e.  NN  |->  ( ( g `  ( 1st `  ( f `  q
) ) ) `  ( 2nd `  ( f `
 q ) ) ) )  =  ( m  e.  NN  |->  ( ( g `  ( 1st `  ( f `  m ) ) ) `
 ( 2nd `  (
f `  m )
) ) )
9871, 73, 75, 77, 78, 33, 84, 35, 90, 91, 97ovnsubaddlem1 38386 . . . . . . . . 9  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. q  e.  NN  ( g `  q )  e.  ( ( D `  ( A `  q )
) `  ( E  /  ( 2 ^ q ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  (
(voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
9956, 57, 68, 69, 98syl31anc 1270 . . . . . . . 8  |-  ( ( ( ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  /\  f : NN -1-1-onto-> ( NN  X.  NN ) )  ->  (
(voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
10099ex 436 . . . . . . 7  |-  ( (
ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( f : NN -1-1-onto-> ( NN  X.  NN )  ->  ( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) ) )
101100exlimdv 1778 . . . . . 6  |-  ( (
ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( E. f  f : NN -1-1-onto-> ( NN  X.  NN )  -> 
( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) ) )
10255, 101mpi 20 . . . . 5  |-  ( (
ph  /\  g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( (voln* `  X
) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
10352, 53, 54, 102syl3anc 1267 . . . 4  |-  ( (
ph  /\  ( g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) ) )  ->  (
(voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
104103ex 436 . . 3  |-  ( ph  ->  ( ( g  Fn  NN  /\  A. n  e.  NN  ( g `  n )  e.  ( ( D `  ( A `  n )
) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( (voln* `  X
) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) ) )
105104exlimdv 1778 . 2  |-  ( ph  ->  ( E. g ( g  Fn  NN  /\  A. n  e.  NN  (
g `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )  ->  ( (voln* `  X
) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) ) )
10651, 105mpd 15 1  |-  ( ph  ->  ( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 984    = wceq 1443   E.wex 1662    e. wcel 1886    =/= wne 2621   A.wral 2736   E.wrex 2737   {crab 2740    C_ wss 3403   (/)c0 3730   ~Pcpw 3950   U_ciun 4277   class class class wbr 4401    |-> cmpt 4460    X. cxp 4831    o. ccom 4837    Fn wfn 5576   -->wf 5577   -1-1-onto->wf1o 5580   ` cfv 5581  (class class class)co 6288   1stc1st 6788   2ndc2nd 6789    ^m cmap 7469   X_cixp 7519   Fincfn 7566   RRcr 9535   RR*cxr 9671    <_ cle 9673    / cdiv 10266   NNcn 10606   2c2 10656   NN0cn0 10866   RR+crp 11299   +ecxad 11404   [,)cico 11634   ^cexp 12269   prod_cprod 13952   volcvol 22408  Σ^csumge0 38198  voln*covoln 38351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cc 8862  ax-ac2 8890  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614  ax-addf 9615  ax-mulf 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-disj 4373  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-om 6690  df-1st 6790  df-2nd 6791  df-tpos 6970  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-ixp 7520  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fi 7922  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-acn 8373  df-ac 8544  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-4 10667  df-5 10668  df-6 10669  df-7 10670  df-8 10671  df-9 10672  df-10 10673  df-n0 10867  df-z 10935  df-dec 11049  df-uz 11157  df-q 11262  df-rp 11300  df-xneg 11406  df-xadd 11407  df-xmul 11408  df-ioo 11636  df-ico 11638  df-icc 11639  df-fz 11782  df-fzo 11913  df-fl 12025  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-rlim 13546  df-sum 13746  df-prod 13953  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-mulr 15197  df-starv 15198  df-tset 15202  df-ple 15203  df-ds 15205  df-unif 15206  df-rest 15314  df-0g 15333  df-topgen 15335  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-grp 16666  df-minusg 16667  df-subg 16807  df-cmn 17425  df-abl 17426  df-mgp 17717  df-ur 17729  df-ring 17775  df-cring 17776  df-oppr 17844  df-dvdsr 17862  df-unit 17863  df-invr 17893  df-dvr 17904  df-drng 17970  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-cnfld 18964  df-top 19914  df-bases 19915  df-topon 19916  df-cmp 20395  df-ovol 22409  df-vol 22411  df-sumge0 38199  df-ovoln 38352
This theorem is referenced by:  ovnsubadd  38388
  Copyright terms: Public domain W3C validator