Step |
Hyp |
Ref |
Expression |
1 |
|
ovnsubaddlem1.x |
|- ( ph -> X e. Fin ) |
2 |
|
ovnsubaddlem1.n0 |
|- ( ph -> X =/= (/) ) |
3 |
|
ovnsubaddlem1.a |
|- ( ph -> A : NN --> ~P ( RR ^m X ) ) |
4 |
|
ovnsubaddlem1.e |
|- ( ph -> E e. RR+ ) |
5 |
|
ovnsubaddlem1.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 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } ) |
6 |
|
ovnsubaddlem1.c |
|- C = ( a e. ~P ( RR ^m X ) |-> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
7 |
|
ovnsubaddlem1.l |
|- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) ) |
8 |
|
ovnsubaddlem1.d |
|- D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) ) |
9 |
|
ovnsubaddlem1.i |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) |
10 |
|
ovnsubaddlem1.f |
|- ( ph -> F : NN -1-1-onto-> ( NN X. NN ) ) |
11 |
|
ovnsubaddlem1.g |
|- G = ( m e. NN |-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
12 |
3
|
adantr |
|- ( ( ph /\ n e. NN ) -> A : NN --> ~P ( RR ^m X ) ) |
13 |
|
simpr |
|- ( ( ph /\ n e. NN ) -> n e. NN ) |
14 |
12 13
|
ffvelrnd |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) e. ~P ( RR ^m X ) ) |
15 |
|
elpwi |
|- ( ( A ` n ) e. ~P ( RR ^m X ) -> ( A ` n ) C_ ( RR ^m X ) ) |
16 |
14 15
|
syl |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( RR ^m X ) ) |
17 |
16
|
ralrimiva |
|- ( ph -> A. n e. NN ( A ` n ) C_ ( RR ^m X ) ) |
18 |
|
iunss |
|- ( U_ n e. NN ( A ` n ) C_ ( RR ^m X ) <-> A. n e. NN ( A ` n ) C_ ( RR ^m X ) ) |
19 |
17 18
|
sylibr |
|- ( ph -> U_ n e. NN ( A ` n ) C_ ( RR ^m X ) ) |
20 |
1 19
|
ovnxrcl |
|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) e. RR* ) |
21 |
|
nfv |
|- F/ m ph |
22 |
|
nnex |
|- NN e. _V |
23 |
22
|
a1i |
|- ( ph -> NN e. _V ) |
24 |
|
icossicc |
|- ( 0 [,) +oo ) C_ ( 0 [,] +oo ) |
25 |
|
nfv |
|- F/ k ( ph /\ m e. NN ) |
26 |
|
simpl |
|- ( ( ph /\ m e. NN ) -> ph ) |
27 |
26 1
|
syl |
|- ( ( ph /\ m e. NN ) -> X e. Fin ) |
28 |
|
f1of |
|- ( F : NN -1-1-onto-> ( NN X. NN ) -> F : NN --> ( NN X. NN ) ) |
29 |
10 28
|
syl |
|- ( ph -> F : NN --> ( NN X. NN ) ) |
30 |
29
|
adantr |
|- ( ( ph /\ m e. NN ) -> F : NN --> ( NN X. NN ) ) |
31 |
|
simpr |
|- ( ( ph /\ m e. NN ) -> m e. NN ) |
32 |
30 31
|
ffvelrnd |
|- ( ( ph /\ m e. NN ) -> ( F ` m ) e. ( NN X. NN ) ) |
33 |
|
xp1st |
|- ( ( F ` m ) e. ( NN X. NN ) -> ( 1st ` ( F ` m ) ) e. NN ) |
34 |
32 33
|
syl |
|- ( ( ph /\ m e. NN ) -> ( 1st ` ( F ` m ) ) e. NN ) |
35 |
|
xp2nd |
|- ( ( F ` m ) e. ( NN X. NN ) -> ( 2nd ` ( F ` m ) ) e. NN ) |
36 |
32 35
|
syl |
|- ( ( ph /\ m e. NN ) -> ( 2nd ` ( F ` m ) ) e. NN ) |
37 |
|
fvex |
|- ( 2nd ` ( F ` m ) ) e. _V |
38 |
|
eleq1 |
|- ( j = ( 2nd ` ( F ` m ) ) -> ( j e. NN <-> ( 2nd ` ( F ` m ) ) e. NN ) ) |
39 |
38
|
3anbi3d |
|- ( j = ( 2nd ` ( F ` m ) ) -> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ ( 2nd ` ( F ` m ) ) e. NN ) ) ) |
40 |
|
fveq2 |
|- ( j = ( 2nd ` ( F ` m ) ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
41 |
40
|
feq1d |
|- ( j = ( 2nd ` ( F ` m ) ) -> ( ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) ) |
42 |
39 41
|
imbi12d |
|- ( j = ( 2nd ` ( F ` m ) ) -> ( ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ ( 2nd ` ( F ` m ) ) e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) ) ) |
43 |
|
fvex |
|- ( 1st ` ( F ` m ) ) e. _V |
44 |
|
eleq1 |
|- ( n = ( 1st ` ( F ` m ) ) -> ( n e. NN <-> ( 1st ` ( F ` m ) ) e. NN ) ) |
45 |
44
|
3anbi2d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( ph /\ n e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) ) ) |
46 |
|
fveq2 |
|- ( n = ( 1st ` ( F ` m ) ) -> ( I ` n ) = ( I ` ( 1st ` ( F ` m ) ) ) ) |
47 |
46
|
fveq1d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( I ` n ) ` j ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) ) |
48 |
47
|
feq1d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( ( I ` n ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) ) |
49 |
45 48
|
imbi12d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) ) ) |
50 |
|
sseq1 |
|- ( a = ( A ` n ) -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) ) ) |
51 |
50
|
rabbidv |
|- ( a = ( A ` n ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
52 |
|
ovex |
|- ( ( ( RR X. RR ) ^m X ) ^m NN ) e. _V |
53 |
52
|
rabex |
|- { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V |
54 |
53
|
a1i |
|- ( ( ph /\ n e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V ) |
55 |
6 51 14 54
|
fvmptd3 |
|- ( ( ph /\ n e. NN ) -> ( C ` ( A ` n ) ) = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
56 |
|
ssrab2 |
|- { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) |
57 |
56
|
a1i |
|- ( ( ph /\ n e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
58 |
55 57
|
eqsstrd |
|- ( ( ph /\ n e. NN ) -> ( C ` ( A ` n ) ) C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
59 |
|
fveq2 |
|- ( a = ( A ` n ) -> ( C ` a ) = ( C ` ( A ` n ) ) ) |
60 |
59
|
eleq2d |
|- ( a = ( A ` n ) -> ( i e. ( C ` a ) <-> i e. ( C ` ( A ` n ) ) ) ) |
61 |
|
fveq2 |
|- ( a = ( A ` n ) -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` ( A ` n ) ) ) |
62 |
61
|
oveq1d |
|- ( a = ( A ` n ) -> ( ( ( voln* ` X ) ` a ) +e e ) = ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) ) |
63 |
62
|
breq2d |
|- ( a = ( A ` n ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) ) ) |
64 |
60 63
|
anbi12d |
|- ( a = ( A ` n ) -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) <-> ( i e. ( C ` ( A ` n ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) ) ) ) |
65 |
64
|
rabbidva2 |
|- ( a = ( A ` n ) -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) |
66 |
65
|
mpteq2dv |
|- ( a = ( A ` n ) -> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) ) |
67 |
|
rpex |
|- RR+ e. _V |
68 |
67
|
mptex |
|- ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) e. _V |
69 |
68
|
a1i |
|- ( ( ph /\ n e. NN ) -> ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) e. _V ) |
70 |
8 66 14 69
|
fvmptd3 |
|- ( ( ph /\ n e. NN ) -> ( D ` ( A ` n ) ) = ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) ) |
71 |
|
oveq2 |
|- ( e = ( E / ( 2 ^ n ) ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) = ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) |
72 |
71
|
breq2d |
|- ( e = ( E / ( 2 ^ n ) ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) |
73 |
72
|
rabbidv |
|- ( e = ( E / ( 2 ^ n ) ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } ) |
74 |
73
|
adantl |
|- ( ( ( ph /\ n e. NN ) /\ e = ( E / ( 2 ^ n ) ) ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } ) |
75 |
4
|
adantr |
|- ( ( ph /\ n e. NN ) -> E e. RR+ ) |
76 |
|
2nn |
|- 2 e. NN |
77 |
76
|
a1i |
|- ( n e. NN -> 2 e. NN ) |
78 |
|
nnnn0 |
|- ( n e. NN -> n e. NN0 ) |
79 |
77 78
|
nnexpcld |
|- ( n e. NN -> ( 2 ^ n ) e. NN ) |
80 |
79
|
nnrpd |
|- ( n e. NN -> ( 2 ^ n ) e. RR+ ) |
81 |
80
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR+ ) |
82 |
75 81
|
rpdivcld |
|- ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR+ ) |
83 |
|
fvex |
|- ( C ` ( A ` n ) ) e. _V |
84 |
83
|
rabex |
|- { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } e. _V |
85 |
84
|
a1i |
|- ( ( ph /\ n e. NN ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } e. _V ) |
86 |
70 74 82 85
|
fvmptd |
|- ( ( ph /\ n e. NN ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } ) |
87 |
|
ssrab2 |
|- { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } C_ ( C ` ( A ` n ) ) |
88 |
87
|
a1i |
|- ( ( ph /\ n e. NN ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } C_ ( C ` ( A ` n ) ) ) |
89 |
86 88
|
eqsstrd |
|- ( ( ph /\ n e. NN ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) C_ ( C ` ( A ` n ) ) ) |
90 |
89 9
|
sseldd |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( C ` ( A ` n ) ) ) |
91 |
58 90
|
sseldd |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
92 |
|
elmapfn |
|- ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` n ) Fn NN ) |
93 |
91 92
|
syl |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) Fn NN ) |
94 |
|
elmapi |
|- ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) ) |
95 |
91 94
|
syl |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) ) |
96 |
95
|
ffvelrnda |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) |
97 |
96
|
ralrimiva |
|- ( ( ph /\ n e. NN ) -> A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) |
98 |
93 97
|
jca |
|- ( ( ph /\ n e. NN ) -> ( ( I ` n ) Fn NN /\ A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) ) |
99 |
98
|
3adant3 |
|- ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) Fn NN /\ A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) ) |
100 |
|
ffnfv |
|- ( ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) <-> ( ( I ` n ) Fn NN /\ A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) ) |
101 |
99 100
|
sylibr |
|- ( ( ph /\ n e. NN /\ j e. NN ) -> ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) ) |
102 |
|
simp3 |
|- ( ( ph /\ n e. NN /\ j e. NN ) -> j e. NN ) |
103 |
101 102
|
ffvelrnd |
|- ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) |
104 |
|
elmapi |
|- ( ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) |
105 |
103 104
|
syl |
|- ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) |
106 |
43 49 105
|
vtocl |
|- ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) |
107 |
37 42 106
|
vtocl |
|- ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ ( 2nd ` ( F ` m ) ) e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) |
108 |
26 34 36 107
|
syl3anc |
|- ( ( ph /\ m e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) |
109 |
|
id |
|- ( m e. NN -> m e. NN ) |
110 |
|
fvex |
|- ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. _V |
111 |
110
|
a1i |
|- ( m e. NN -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. _V ) |
112 |
11
|
fvmpt2 |
|- ( ( m e. NN /\ ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. _V ) -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
113 |
109 111 112
|
syl2anc |
|- ( m e. NN -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
114 |
113
|
adantl |
|- ( ( ph /\ m e. NN ) -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
115 |
114
|
feq1d |
|- ( ( ph /\ m e. NN ) -> ( ( G ` m ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) ) |
116 |
108 115
|
mpbird |
|- ( ( ph /\ m e. NN ) -> ( G ` m ) : X --> ( RR X. RR ) ) |
117 |
25 27 7 116
|
hoiprodcl2 |
|- ( ( ph /\ m e. NN ) -> ( L ` ( G ` m ) ) e. ( 0 [,) +oo ) ) |
118 |
24 117
|
sseldi |
|- ( ( ph /\ m e. NN ) -> ( L ` ( G ` m ) ) e. ( 0 [,] +oo ) ) |
119 |
21 23 118
|
sge0xrclmpt |
|- ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) e. RR* ) |
120 |
|
nfv |
|- F/ n ph |
121 |
|
0xr |
|- 0 e. RR* |
122 |
121
|
a1i |
|- ( ( ph /\ n e. NN ) -> 0 e. RR* ) |
123 |
|
pnfxr |
|- +oo e. RR* |
124 |
123
|
a1i |
|- ( ( ph /\ n e. NN ) -> +oo e. RR* ) |
125 |
1
|
adantr |
|- ( ( ph /\ n e. NN ) -> X e. Fin ) |
126 |
125 16 5
|
ovnval2b |
|- ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) = if ( X = (/) , 0 , inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) ) |
127 |
2
|
neneqd |
|- ( ph -> -. X = (/) ) |
128 |
127
|
iffalsed |
|- ( ph -> if ( X = (/) , 0 , inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) = inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) |
129 |
128
|
adantr |
|- ( ( ph /\ n e. NN ) -> if ( X = (/) , 0 , inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) = inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) |
130 |
126 129
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) = inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) |
131 |
|
sseq1 |
|- ( a = ( A ` n ) -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) ) |
132 |
131
|
anbi1d |
|- ( a = ( A ` n ) -> ( ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) ) |
133 |
132
|
rexbidv |
|- ( a = ( A ` n ) -> ( 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 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) ) |
134 |
133
|
rabbidv |
|- ( a = ( A ` n ) -> { 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 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } ) |
135 |
|
xrex |
|- RR* e. _V |
136 |
135
|
rabex |
|- { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } e. _V |
137 |
136
|
a1i |
|- ( ( ph /\ n e. NN ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } e. _V ) |
138 |
5 134 14 137
|
fvmptd3 |
|- ( ( ph /\ n e. NN ) -> ( Z ` ( A ` n ) ) = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } ) |
139 |
|
ssrab2 |
|- { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR* |
140 |
139
|
a1i |
|- ( ( ph /\ n e. NN ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR* ) |
141 |
138 140
|
eqsstrd |
|- ( ( ph /\ n e. NN ) -> ( Z ` ( A ` n ) ) C_ RR* ) |
142 |
|
infxrcl |
|- ( ( Z ` ( A ` n ) ) C_ RR* -> inf ( ( Z ` ( A ` n ) ) , RR* , < ) e. RR* ) |
143 |
141 142
|
syl |
|- ( ( ph /\ n e. NN ) -> inf ( ( Z ` ( A ` n ) ) , RR* , < ) e. RR* ) |
144 |
130 143
|
eqeltrd |
|- ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) e. RR* ) |
145 |
4
|
rpred |
|- ( ph -> E e. RR ) |
146 |
145
|
adantr |
|- ( ( ph /\ n e. NN ) -> E e. RR ) |
147 |
|
2re |
|- 2 e. RR |
148 |
147
|
a1i |
|- ( n e. NN -> 2 e. RR ) |
149 |
148 78
|
reexpcld |
|- ( n e. NN -> ( 2 ^ n ) e. RR ) |
150 |
149
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR ) |
151 |
148
|
recnd |
|- ( n e. NN -> 2 e. CC ) |
152 |
|
2ne0 |
|- 2 =/= 0 |
153 |
152
|
a1i |
|- ( n e. NN -> 2 =/= 0 ) |
154 |
|
nnz |
|- ( n e. NN -> n e. ZZ ) |
155 |
151 153 154
|
expne0d |
|- ( n e. NN -> ( 2 ^ n ) =/= 0 ) |
156 |
155
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( 2 ^ n ) =/= 0 ) |
157 |
146 150 156
|
redivcld |
|- ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR ) |
158 |
157
|
rexrd |
|- ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR* ) |
159 |
144 158
|
xaddcld |
|- ( ( ph /\ n e. NN ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) e. RR* ) |
160 |
125 16
|
ovncl |
|- ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) e. ( 0 [,] +oo ) ) |
161 |
|
xrge0ge0 |
|- ( ( ( voln* ` X ) ` ( A ` n ) ) e. ( 0 [,] +oo ) -> 0 <_ ( ( voln* ` X ) ` ( A ` n ) ) ) |
162 |
160 161
|
syl |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( ( voln* ` X ) ` ( A ` n ) ) ) |
163 |
|
0red |
|- ( ( ph /\ n e. NN ) -> 0 e. RR ) |
164 |
82
|
rpgt0d |
|- ( ( ph /\ n e. NN ) -> 0 < ( E / ( 2 ^ n ) ) ) |
165 |
163 157 164
|
ltled |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( E / ( 2 ^ n ) ) ) |
166 |
157
|
ltpnfd |
|- ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) < +oo ) |
167 |
158 124 166
|
xrltled |
|- ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) <_ +oo ) |
168 |
122 124 158 165 167
|
eliccxrd |
|- ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. ( 0 [,] +oo ) ) |
169 |
144 168
|
xadd0ge |
|- ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) |
170 |
122 144 159 162 169
|
xrletrd |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) |
171 |
|
pnfge |
|- ( ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) e. RR* -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) <_ +oo ) |
172 |
159 171
|
syl |
|- ( ( ph /\ n e. NN ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) <_ +oo ) |
173 |
122 124 159 170 172
|
eliccxrd |
|- ( ( ph /\ n e. NN ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) e. ( 0 [,] +oo ) ) |
174 |
120 23 173
|
sge0xrclmpt |
|- ( ph -> ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) e. RR* ) |
175 |
|
sseq1 |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) ) ) |
176 |
175
|
rabbidv |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
177 |
3
|
adantr |
|- ( ( ph /\ m e. NN ) -> A : NN --> ~P ( RR ^m X ) ) |
178 |
177 34
|
ffvelrnd |
|- ( ( ph /\ m e. NN ) -> ( A ` ( 1st ` ( F ` m ) ) ) e. ~P ( RR ^m X ) ) |
179 |
52
|
rabex |
|- { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V |
180 |
179
|
a1i |
|- ( ( ph /\ m e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V ) |
181 |
6 176 178 180
|
fvmptd3 |
|- ( ( ph /\ m e. NN ) -> ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
182 |
|
ssrab2 |
|- { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) |
183 |
182
|
a1i |
|- ( ( ph /\ m e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
184 |
181 183
|
eqsstrd |
|- ( ( ph /\ m e. NN ) -> ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
185 |
|
fveq2 |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( C ` a ) = ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) |
186 |
185
|
eleq2d |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( i e. ( C ` a ) <-> i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) ) |
187 |
|
fveq2 |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) |
188 |
187
|
oveq1d |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( ( voln* ` X ) ` a ) +e e ) = ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) ) |
189 |
188
|
breq2d |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) ) ) |
190 |
186 189
|
anbi12d |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) <-> ( i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) ) ) ) |
191 |
190
|
rabbidva2 |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) |
192 |
191
|
mpteq2dv |
|- ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) ) |
193 |
67
|
mptex |
|- ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) e. _V |
194 |
193
|
a1i |
|- ( ( ph /\ m e. NN ) -> ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) e. _V ) |
195 |
8 192 178 194
|
fvmptd3 |
|- ( ( ph /\ m e. NN ) -> ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) = ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) ) |
196 |
|
oveq2 |
|- ( e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) -> ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) = ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) |
197 |
196
|
breq2d |
|- ( e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) ) |
198 |
197
|
rabbidv |
|- ( e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } ) |
199 |
198
|
adantl |
|- ( ( ( ph /\ m e. NN ) /\ e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } ) |
200 |
26 4
|
syl |
|- ( ( ph /\ m e. NN ) -> E e. RR+ ) |
201 |
|
2rp |
|- 2 e. RR+ |
202 |
201
|
a1i |
|- ( ( ph /\ m e. NN ) -> 2 e. RR+ ) |
203 |
34
|
nnzd |
|- ( ( ph /\ m e. NN ) -> ( 1st ` ( F ` m ) ) e. ZZ ) |
204 |
202 203
|
rpexpcld |
|- ( ( ph /\ m e. NN ) -> ( 2 ^ ( 1st ` ( F ` m ) ) ) e. RR+ ) |
205 |
200 204
|
rpdivcld |
|- ( ( ph /\ m e. NN ) -> ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) e. RR+ ) |
206 |
|
fvex |
|- ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) e. _V |
207 |
206
|
rabex |
|- { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } e. _V |
208 |
207
|
a1i |
|- ( ( ph /\ m e. NN ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } e. _V ) |
209 |
195 199 205 208
|
fvmptd |
|- ( ( ph /\ m e. NN ) -> ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } ) |
210 |
|
ssrab2 |
|- { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } C_ ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) |
211 |
210
|
a1i |
|- ( ( ph /\ m e. NN ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } C_ ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) |
212 |
209 211
|
eqsstrd |
|- ( ( ph /\ m e. NN ) -> ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) C_ ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) |
213 |
44
|
anbi2d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( ph /\ n e. NN ) <-> ( ph /\ ( 1st ` ( F ` m ) ) e. NN ) ) ) |
214 |
|
2fveq3 |
|- ( n = ( 1st ` ( F ` m ) ) -> ( D ` ( A ` n ) ) = ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) |
215 |
|
oveq2 |
|- ( n = ( 1st ` ( F ` m ) ) -> ( 2 ^ n ) = ( 2 ^ ( 1st ` ( F ` m ) ) ) ) |
216 |
215
|
oveq2d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( E / ( 2 ^ n ) ) = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) |
217 |
214 216
|
fveq12d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) = ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) |
218 |
46 217
|
eleq12d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) <-> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) ) |
219 |
213 218
|
imbi12d |
|- ( n = ( 1st ` ( F ` m ) ) -> ( ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) <-> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) ) ) |
220 |
43 219 9
|
vtocl |
|- ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) |
221 |
26 34 220
|
syl2anc |
|- ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) |
222 |
212 221
|
sseldd |
|- ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) |
223 |
184 222
|
sseldd |
|- ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) |
224 |
|
elmapfn |
|- ( ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) Fn NN ) |
225 |
223 224
|
syl |
|- ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) Fn NN ) |
226 |
|
elmapi |
|- ( ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) ) |
227 |
223 226
|
syl |
|- ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) ) |
228 |
227
|
ffvelrnda |
|- ( ( ( ph /\ m e. NN ) /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) ) |
229 |
228
|
ralrimiva |
|- ( ( ph /\ m e. NN ) -> A. j e. NN ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) ) |
230 |
225 229
|
jca |
|- ( ( ph /\ m e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) Fn NN /\ A. j e. NN ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) ) ) |
231 |
|
ffnfv |
|- ( ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) Fn NN /\ A. j e. NN ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) ) ) |
232 |
230 231
|
sylibr |
|- ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) ) |
233 |
232 36
|
ffvelrnd |
|- ( ( ph /\ m e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. ( ( RR X. RR ) ^m X ) ) |
234 |
233 11
|
fmptd |
|- ( ph -> G : NN --> ( ( RR X. RR ) ^m X ) ) |
235 |
|
simpl |
|- ( ( ph /\ n e. NN ) -> ph ) |
236 |
9 86
|
eleqtrd |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) e. { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } ) |
237 |
87 236
|
sseldi |
|- ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( C ` ( A ` n ) ) ) |
238 |
|
simp3 |
|- ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( I ` n ) e. ( C ` ( A ` n ) ) ) |
239 |
55
|
3adant3 |
|- ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( C ` ( A ` n ) ) = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
240 |
238 239
|
eleqtrd |
|- ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( I ` n ) e. { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } ) |
241 |
|
fveq1 |
|- ( h = ( I ` n ) -> ( h ` j ) = ( ( I ` n ) ` j ) ) |
242 |
241
|
coeq2d |
|- ( h = ( I ` n ) -> ( [,) o. ( h ` j ) ) = ( [,) o. ( ( I ` n ) ` j ) ) ) |
243 |
242
|
fveq1d |
|- ( h = ( I ` n ) -> ( ( [,) o. ( h ` j ) ) ` k ) = ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) |
244 |
243
|
ixpeq2dv |
|- ( h = ( I ` n ) -> X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) |
245 |
244
|
iuneq2d |
|- ( h = ( I ` n ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) |
246 |
245
|
sseq2d |
|- ( h = ( I ` n ) -> ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) ) |
247 |
246
|
elrab |
|- ( ( I ` n ) e. { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } <-> ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) ) |
248 |
240 247
|
sylib |
|- ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) ) |
249 |
248
|
simprd |
|- ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) |
250 |
235 13 237 249
|
syl3anc |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) |
251 |
|
f1ofo |
|- ( F : NN -1-1-onto-> ( NN X. NN ) -> F : NN -onto-> ( NN X. NN ) ) |
252 |
10 251
|
syl |
|- ( ph -> F : NN -onto-> ( NN X. NN ) ) |
253 |
252
|
ad2antrr |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> F : NN -onto-> ( NN X. NN ) ) |
254 |
|
opelxpi |
|- ( ( n e. NN /\ j e. NN ) -> <. n , j >. e. ( NN X. NN ) ) |
255 |
13 254
|
sylan |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> <. n , j >. e. ( NN X. NN ) ) |
256 |
|
foelrni |
|- ( ( F : NN -onto-> ( NN X. NN ) /\ <. n , j >. e. ( NN X. NN ) ) -> E. m e. NN ( F ` m ) = <. n , j >. ) |
257 |
253 255 256
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> E. m e. NN ( F ` m ) = <. n , j >. ) |
258 |
|
nfv |
|- F/ m ( ( ph /\ n e. NN ) /\ j e. NN ) |
259 |
|
nfre1 |
|- F/ m E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) |
260 |
|
simpl |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> m e. NN ) |
261 |
|
fveq2 |
|- ( ( F ` m ) = <. n , j >. -> ( 1st ` ( F ` m ) ) = ( 1st ` <. n , j >. ) ) |
262 |
|
op1stg |
|- ( ( n e. _V /\ j e. _V ) -> ( 1st ` <. n , j >. ) = n ) |
263 |
262
|
el2v |
|- ( 1st ` <. n , j >. ) = n |
264 |
263
|
a1i |
|- ( ( F ` m ) = <. n , j >. -> ( 1st ` <. n , j >. ) = n ) |
265 |
261 264
|
eqtrd |
|- ( ( F ` m ) = <. n , j >. -> ( 1st ` ( F ` m ) ) = n ) |
266 |
265
|
adantl |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( 1st ` ( F ` m ) ) = n ) |
267 |
260 266
|
jca |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( m e. NN /\ ( 1st ` ( F ` m ) ) = n ) ) |
268 |
|
2fveq3 |
|- ( i = m -> ( 1st ` ( F ` i ) ) = ( 1st ` ( F ` m ) ) ) |
269 |
268
|
eqeq1d |
|- ( i = m -> ( ( 1st ` ( F ` i ) ) = n <-> ( 1st ` ( F ` m ) ) = n ) ) |
270 |
269
|
elrab |
|- ( m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } <-> ( m e. NN /\ ( 1st ` ( F ` m ) ) = n ) ) |
271 |
267 270
|
sylibr |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } ) |
272 |
271
|
3adant1 |
|- ( ( ( ( ph /\ n e. NN ) /\ j e. NN ) /\ m e. NN /\ ( F ` m ) = <. n , j >. ) -> m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } ) |
273 |
260 113
|
syl |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
274 |
265
|
fveq2d |
|- ( ( F ` m ) = <. n , j >. -> ( I ` ( 1st ` ( F ` m ) ) ) = ( I ` n ) ) |
275 |
|
vex |
|- n e. _V |
276 |
|
vex |
|- j e. _V |
277 |
275 276
|
op2ndd |
|- ( ( F ` m ) = <. n , j >. -> ( 2nd ` ( F ` m ) ) = j ) |
278 |
274 277
|
fveq12d |
|- ( ( F ` m ) = <. n , j >. -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) = ( ( I ` n ) ` j ) ) |
279 |
278
|
adantl |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) = ( ( I ` n ) ` j ) ) |
280 |
273 279
|
eqtr2d |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( ( I ` n ) ` j ) = ( G ` m ) ) |
281 |
280
|
coeq2d |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( [,) o. ( ( I ` n ) ` j ) ) = ( [,) o. ( G ` m ) ) ) |
282 |
281
|
fveq1d |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) = ( ( [,) o. ( G ` m ) ) ` k ) ) |
283 |
282
|
ixpeq2dv |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
284 |
|
eqimss |
|- ( X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
285 |
283 284
|
syl |
|- ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
286 |
285
|
3adant1 |
|- ( ( ( ( ph /\ n e. NN ) /\ j e. NN ) /\ m e. NN /\ ( F ` m ) = <. n , j >. ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
287 |
|
rspe |
|- ( ( m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } /\ X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
288 |
272 286 287
|
syl2anc |
|- ( ( ( ( ph /\ n e. NN ) /\ j e. NN ) /\ m e. NN /\ ( F ` m ) = <. n , j >. ) -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
289 |
288
|
3exp |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( m e. NN -> ( ( F ` m ) = <. n , j >. -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) ) ) |
290 |
258 259 289
|
rexlimd |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( E. m e. NN ( F ` m ) = <. n , j >. -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) ) |
291 |
257 290
|
mpd |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
292 |
291
|
ralrimiva |
|- ( ( ph /\ n e. NN ) -> A. j e. NN E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
293 |
|
iunss2 |
|- ( A. j e. NN E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
294 |
292 293
|
syl |
|- ( ( ph /\ n e. NN ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
295 |
250 294
|
sstrd |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
296 |
|
ssrab2 |
|- { i e. NN | ( 1st ` ( F ` i ) ) = n } C_ NN |
297 |
|
iunss1 |
|- ( { i e. NN | ( 1st ` ( F ` i ) ) = n } C_ NN -> U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
298 |
296 297
|
ax-mp |
|- U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) |
299 |
298
|
a1i |
|- ( ( ph /\ n e. NN ) -> U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
300 |
295 299
|
sstrd |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
301 |
300
|
ralrimiva |
|- ( ph -> A. n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
302 |
|
iunss |
|- ( U_ n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) <-> A. n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
303 |
301 302
|
sylibr |
|- ( ph -> U_ n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) |
304 |
1 2 7 234 303
|
ovnlecvr |
|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) ) |
305 |
114
|
fveq2d |
|- ( ( ph /\ m e. NN ) -> ( L ` ( G ` m ) ) = ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) |
306 |
305
|
mpteq2dva |
|- ( ph -> ( m e. NN |-> ( L ` ( G ` m ) ) ) = ( m e. NN |-> ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) ) |
307 |
306
|
fveq2d |
|- ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) = ( sum^ ` ( m e. NN |-> ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) ) ) |
308 |
|
nfv |
|- F/ p ph |
309 |
|
2fveq3 |
|- ( p = ( F ` m ) -> ( I ` ( 1st ` p ) ) = ( I ` ( 1st ` ( F ` m ) ) ) ) |
310 |
|
fveq2 |
|- ( p = ( F ` m ) -> ( 2nd ` p ) = ( 2nd ` ( F ` m ) ) ) |
311 |
309 310
|
fveq12d |
|- ( p = ( F ` m ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) |
312 |
311
|
fveq2d |
|- ( p = ( F ` m ) -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) = ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) |
313 |
|
eqidd |
|- ( ( ph /\ m e. NN ) -> ( F ` m ) = ( F ` m ) ) |
314 |
|
nfv |
|- F/ k ( ph /\ p e. ( NN X. NN ) ) |
315 |
1
|
adantr |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> X e. Fin ) |
316 |
|
simpl |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> ph ) |
317 |
|
xp1st |
|- ( p e. ( NN X. NN ) -> ( 1st ` p ) e. NN ) |
318 |
317
|
adantl |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> ( 1st ` p ) e. NN ) |
319 |
|
xp2nd |
|- ( p e. ( NN X. NN ) -> ( 2nd ` p ) e. NN ) |
320 |
319
|
adantl |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> ( 2nd ` p ) e. NN ) |
321 |
|
fvex |
|- ( 2nd ` p ) e. _V |
322 |
|
eleq1 |
|- ( j = ( 2nd ` p ) -> ( j e. NN <-> ( 2nd ` p ) e. NN ) ) |
323 |
322
|
3anbi3d |
|- ( j = ( 2nd ` p ) -> ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` p ) e. NN /\ ( 2nd ` p ) e. NN ) ) ) |
324 |
|
fveq2 |
|- ( j = ( 2nd ` p ) -> ( ( I ` ( 1st ` p ) ) ` j ) = ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) |
325 |
324
|
feq1d |
|- ( j = ( 2nd ` p ) -> ( ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) ) ) |
326 |
323 325
|
imbi12d |
|- ( j = ( 2nd ` p ) -> ( ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` p ) e. NN /\ ( 2nd ` p ) e. NN ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) ) ) ) |
327 |
|
fvex |
|- ( 1st ` p ) e. _V |
328 |
|
eleq1 |
|- ( n = ( 1st ` p ) -> ( n e. NN <-> ( 1st ` p ) e. NN ) ) |
329 |
328
|
3anbi2d |
|- ( n = ( 1st ` p ) -> ( ( ph /\ n e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) ) ) |
330 |
|
fveq2 |
|- ( n = ( 1st ` p ) -> ( I ` n ) = ( I ` ( 1st ` p ) ) ) |
331 |
330
|
fveq1d |
|- ( n = ( 1st ` p ) -> ( ( I ` n ) ` j ) = ( ( I ` ( 1st ` p ) ) ` j ) ) |
332 |
331
|
feq1d |
|- ( n = ( 1st ` p ) -> ( ( ( I ` n ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) ) |
333 |
329 332
|
imbi12d |
|- ( n = ( 1st ` p ) -> ( ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) ) ) |
334 |
327 333 105
|
vtocl |
|- ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) |
335 |
321 326 334
|
vtocl |
|- ( ( ph /\ ( 1st ` p ) e. NN /\ ( 2nd ` p ) e. NN ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) ) |
336 |
316 318 320 335
|
syl3anc |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) ) |
337 |
314 315 7 336
|
hoiprodcl2 |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) e. ( 0 [,) +oo ) ) |
338 |
24 337
|
sseldi |
|- ( ( ph /\ p e. ( NN X. NN ) ) -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) e. ( 0 [,] +oo ) ) |
339 |
308 21 312 23 10 313 338
|
sge0f1o |
|- ( ph -> ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) = ( sum^ ` ( m e. NN |-> ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) ) ) |
340 |
307 339
|
eqtr4d |
|- ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) = ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) ) |
341 |
|
nfv |
|- F/ j ph |
342 |
275 276
|
op1std |
|- ( p = <. n , j >. -> ( 1st ` p ) = n ) |
343 |
342
|
fveq2d |
|- ( p = <. n , j >. -> ( I ` ( 1st ` p ) ) = ( I ` n ) ) |
344 |
275 276
|
op2ndd |
|- ( p = <. n , j >. -> ( 2nd ` p ) = j ) |
345 |
343 344
|
fveq12d |
|- ( p = <. n , j >. -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) = ( ( I ` n ) ` j ) ) |
346 |
345
|
fveq2d |
|- ( p = <. n , j >. -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) = ( L ` ( ( I ` n ) ` j ) ) ) |
347 |
|
nfv |
|- F/ k ( ( ph /\ n e. NN ) /\ j e. NN ) |
348 |
125
|
adantr |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> X e. Fin ) |
349 |
96 104
|
syl |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) |
350 |
347 348 7 349
|
hoiprodcl2 |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( L ` ( ( I ` n ) ` j ) ) e. ( 0 [,) +oo ) ) |
351 |
24 350
|
sseldi |
|- ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( L ` ( ( I ` n ) ` j ) ) e. ( 0 [,] +oo ) ) |
352 |
351
|
3impa |
|- ( ( ph /\ n e. NN /\ j e. NN ) -> ( L ` ( ( I ` n ) ` j ) ) e. ( 0 [,] +oo ) ) |
353 |
341 346 23 23 352
|
sge0xp |
|- ( ph -> ( sum^ ` ( n e. NN |-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) ) = ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) ) |
354 |
353
|
eqcomd |
|- ( ph -> ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) = ( sum^ ` ( n e. NN |-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) ) ) |
355 |
22
|
a1i |
|- ( ( ph /\ n e. NN ) -> NN e. _V ) |
356 |
|
eqid |
|- ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) = ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) |
357 |
351 356
|
fmptd |
|- ( ( ph /\ n e. NN ) -> ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) : NN --> ( 0 [,] +oo ) ) |
358 |
355 357
|
sge0cl |
|- ( ( ph /\ n e. NN ) -> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) e. ( 0 [,] +oo ) ) |
359 |
|
fveq1 |
|- ( i = ( I ` n ) -> ( i ` j ) = ( ( I ` n ) ` j ) ) |
360 |
359
|
fveq2d |
|- ( i = ( I ` n ) -> ( L ` ( i ` j ) ) = ( L ` ( ( I ` n ) ` j ) ) ) |
361 |
360
|
mpteq2dv |
|- ( i = ( I ` n ) -> ( j e. NN |-> ( L ` ( i ` j ) ) ) = ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) |
362 |
361
|
fveq2d |
|- ( i = ( I ` n ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) |
363 |
362
|
breq1d |
|- ( i = ( I ` n ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) |
364 |
363
|
elrab |
|- ( ( I ` n ) e. { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } <-> ( ( I ` n ) e. ( C ` ( A ` n ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) |
365 |
236 364
|
sylib |
|- ( ( ph /\ n e. NN ) -> ( ( I ` n ) e. ( C ` ( A ` n ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) |
366 |
365
|
simprd |
|- ( ( ph /\ n e. NN ) -> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) |
367 |
120 23 358 173 366
|
sge0lempt |
|- ( ph -> ( sum^ ` ( n e. NN |-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) ) |
368 |
354 367
|
eqbrtrd |
|- ( ph -> ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) ) |
369 |
340 368
|
eqbrtrd |
|- ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) ) |
370 |
20 119 174 304 369
|
xrletrd |
|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) ) |
371 |
120 23 160 168
|
sge0xadd |
|- ( ph -> ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) = ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. NN |-> ( E / ( 2 ^ n ) ) ) ) ) ) |
372 |
121
|
a1i |
|- ( ph -> 0 e. RR* ) |
373 |
123
|
a1i |
|- ( ph -> +oo e. RR* ) |
374 |
145
|
rexrd |
|- ( ph -> E e. RR* ) |
375 |
4
|
rpge0d |
|- ( ph -> 0 <_ E ) |
376 |
145
|
ltpnfd |
|- ( ph -> E < +oo ) |
377 |
372 373 374 375 376
|
elicod |
|- ( ph -> E e. ( 0 [,) +oo ) ) |
378 |
377
|
sge0ad2en |
|- ( ph -> ( sum^ ` ( n e. NN |-> ( E / ( 2 ^ n ) ) ) ) = E ) |
379 |
378
|
oveq2d |
|- ( ph -> ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. NN |-> ( E / ( 2 ^ n ) ) ) ) ) = ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) |
380 |
371 379
|
eqtrd |
|- ( ph -> ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) = ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) |
381 |
370 380
|
breqtrd |
|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) |