Step |
Hyp |
Ref |
Expression |
1 |
|
uniioombl.1 |
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
2 |
|
uniioombl.2 |
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) |
3 |
|
uniioombl.3 |
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) ) |
4 |
|
uniioombl.a |
|- A = U. ran ( (,) o. F ) |
5 |
|
uniioombl.e |
|- ( ph -> ( vol* ` E ) e. RR ) |
6 |
|
uniioombl.c |
|- ( ph -> C e. RR+ ) |
7 |
|
uniioombl.g |
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
8 |
|
uniioombl.s |
|- ( ph -> E C_ U. ran ( (,) o. G ) ) |
9 |
|
uniioombl.t |
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) ) |
10 |
|
uniioombl.v |
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) ) |
11 |
|
uniioombl.m |
|- ( ph -> M e. NN ) |
12 |
|
uniioombl.m2 |
|- ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C ) |
13 |
|
uniioombl.k |
|- K = U. ( ( (,) o. G ) " ( 1 ... M ) ) |
14 |
|
uniioombl.n |
|- ( ph -> N e. NN ) |
15 |
|
uniioombl.n2 |
|- ( ph -> A. j e. ( 1 ... M ) ( abs ` ( sum_ i e. ( 1 ... N ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) ) |
16 |
|
uniioombl.l |
|- L = U. ( ( (,) o. F ) " ( 1 ... N ) ) |
17 |
|
inss1 |
|- ( E i^i A ) C_ E |
18 |
7
|
uniiccdif |
|- ( ph -> ( U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) /\ ( vol* ` ( U. ran ( [,] o. G ) \ U. ran ( (,) o. G ) ) ) = 0 ) ) |
19 |
18
|
simpld |
|- ( ph -> U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) ) |
20 |
|
ovolficcss |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. G ) C_ RR ) |
21 |
7 20
|
syl |
|- ( ph -> U. ran ( [,] o. G ) C_ RR ) |
22 |
19 21
|
sstrd |
|- ( ph -> U. ran ( (,) o. G ) C_ RR ) |
23 |
8 22
|
sstrd |
|- ( ph -> E C_ RR ) |
24 |
|
ovolsscl |
|- ( ( ( E i^i A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i A ) ) e. RR ) |
25 |
17 23 5 24
|
mp3an2i |
|- ( ph -> ( vol* ` ( E i^i A ) ) e. RR ) |
26 |
|
difssd |
|- ( ph -> ( E \ A ) C_ E ) |
27 |
|
ovolsscl |
|- ( ( ( E \ A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ A ) ) e. RR ) |
28 |
26 23 5 27
|
syl3anc |
|- ( ph -> ( vol* ` ( E \ A ) ) e. RR ) |
29 |
25 28
|
readdcld |
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) e. RR ) |
30 |
|
inss1 |
|- ( K i^i A ) C_ K |
31 |
|
imassrn |
|- ( ( (,) o. G ) " ( 1 ... M ) ) C_ ran ( (,) o. G ) |
32 |
31
|
unissi |
|- U. ( ( (,) o. G ) " ( 1 ... M ) ) C_ U. ran ( (,) o. G ) |
33 |
13 32
|
eqsstri |
|- K C_ U. ran ( (,) o. G ) |
34 |
33 22
|
sstrid |
|- ( ph -> K C_ RR ) |
35 |
1 2 3 4 5 6 7 8 9 10
|
uniioombllem1 |
|- ( ph -> sup ( ran T , RR* , < ) e. RR ) |
36 |
|
ssid |
|- U. ran ( (,) o. G ) C_ U. ran ( (,) o. G ) |
37 |
9
|
ovollb |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. G ) C_ U. ran ( (,) o. G ) ) -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) |
38 |
7 36 37
|
sylancl |
|- ( ph -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) |
39 |
|
ovollecl |
|- ( ( U. ran ( (,) o. G ) C_ RR /\ sup ( ran T , RR* , < ) e. RR /\ ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) -> ( vol* ` U. ran ( (,) o. G ) ) e. RR ) |
40 |
22 35 38 39
|
syl3anc |
|- ( ph -> ( vol* ` U. ran ( (,) o. G ) ) e. RR ) |
41 |
|
ovolsscl |
|- ( ( K C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` K ) e. RR ) |
42 |
33 22 40 41
|
mp3an2i |
|- ( ph -> ( vol* ` K ) e. RR ) |
43 |
|
ovolsscl |
|- ( ( ( K i^i A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i A ) ) e. RR ) |
44 |
30 34 42 43
|
mp3an2i |
|- ( ph -> ( vol* ` ( K i^i A ) ) e. RR ) |
45 |
|
difssd |
|- ( ph -> ( K \ A ) C_ K ) |
46 |
|
ovolsscl |
|- ( ( ( K \ A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ A ) ) e. RR ) |
47 |
45 34 42 46
|
syl3anc |
|- ( ph -> ( vol* ` ( K \ A ) ) e. RR ) |
48 |
44 47
|
readdcld |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) e. RR ) |
49 |
6
|
rpred |
|- ( ph -> C e. RR ) |
50 |
49 49
|
readdcld |
|- ( ph -> ( C + C ) e. RR ) |
51 |
48 50
|
readdcld |
|- ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) e. RR ) |
52 |
|
4re |
|- 4 e. RR |
53 |
|
remulcl |
|- ( ( 4 e. RR /\ C e. RR ) -> ( 4 x. C ) e. RR ) |
54 |
52 49 53
|
sylancr |
|- ( ph -> ( 4 x. C ) e. RR ) |
55 |
5 54
|
readdcld |
|- ( ph -> ( ( vol* ` E ) + ( 4 x. C ) ) e. RR ) |
56 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
uniioombllem3 |
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) < ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) ) |
57 |
29 51 56
|
ltled |
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) ) |
58 |
5 50
|
readdcld |
|- ( ph -> ( ( vol* ` E ) + ( C + C ) ) e. RR ) |
59 |
42 49
|
readdcld |
|- ( ph -> ( ( vol* ` K ) + C ) e. RR ) |
60 |
|
inss1 |
|- ( K i^i L ) C_ K |
61 |
|
ovolsscl |
|- ( ( ( K i^i L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i L ) ) e. RR ) |
62 |
60 34 42 61
|
mp3an2i |
|- ( ph -> ( vol* ` ( K i^i L ) ) e. RR ) |
63 |
62 49
|
readdcld |
|- ( ph -> ( ( vol* ` ( K i^i L ) ) + C ) e. RR ) |
64 |
|
difssd |
|- ( ph -> ( K \ L ) C_ K ) |
65 |
|
ovolsscl |
|- ( ( ( K \ L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ L ) ) e. RR ) |
66 |
64 34 42 65
|
syl3anc |
|- ( ph -> ( vol* ` ( K \ L ) ) e. RR ) |
67 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
|
uniioombllem4 |
|- ( ph -> ( vol* ` ( K i^i A ) ) <_ ( ( vol* ` ( K i^i L ) ) + C ) ) |
68 |
|
imassrn |
|- ( ( (,) o. F ) " ( 1 ... N ) ) C_ ran ( (,) o. F ) |
69 |
68
|
unissi |
|- U. ( ( (,) o. F ) " ( 1 ... N ) ) C_ U. ran ( (,) o. F ) |
70 |
69 16 4
|
3sstr4i |
|- L C_ A |
71 |
|
sscon |
|- ( L C_ A -> ( K \ A ) C_ ( K \ L ) ) |
72 |
70 71
|
mp1i |
|- ( ph -> ( K \ A ) C_ ( K \ L ) ) |
73 |
64 34
|
sstrd |
|- ( ph -> ( K \ L ) C_ RR ) |
74 |
|
ovolss |
|- ( ( ( K \ A ) C_ ( K \ L ) /\ ( K \ L ) C_ RR ) -> ( vol* ` ( K \ A ) ) <_ ( vol* ` ( K \ L ) ) ) |
75 |
72 73 74
|
syl2anc |
|- ( ph -> ( vol* ` ( K \ A ) ) <_ ( vol* ` ( K \ L ) ) ) |
76 |
44 47 63 66 67 75
|
le2addd |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) ) |
77 |
62
|
recnd |
|- ( ph -> ( vol* ` ( K i^i L ) ) e. CC ) |
78 |
49
|
recnd |
|- ( ph -> C e. CC ) |
79 |
66
|
recnd |
|- ( ph -> ( vol* ` ( K \ L ) ) e. CC ) |
80 |
77 78 79
|
add32d |
|- ( ph -> ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) = ( ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) + C ) ) |
81 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
82 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
83 |
|
rexpssxrxp |
|- ( RR X. RR ) C_ ( RR* X. RR* ) |
84 |
82 83
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) |
85 |
|
fss |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) ) |
86 |
1 84 85
|
sylancl |
|- ( ph -> F : NN --> ( RR* X. RR* ) ) |
87 |
|
fco |
|- ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR ) |
88 |
81 86 87
|
sylancr |
|- ( ph -> ( (,) o. F ) : NN --> ~P RR ) |
89 |
|
ffun |
|- ( ( (,) o. F ) : NN --> ~P RR -> Fun ( (,) o. F ) ) |
90 |
|
funiunfv |
|- ( Fun ( (,) o. F ) -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) ) |
91 |
88 89 90
|
3syl |
|- ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) ) |
92 |
91 16
|
eqtr4di |
|- ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = L ) |
93 |
|
fzfid |
|- ( ph -> ( 1 ... N ) e. Fin ) |
94 |
|
elfznn |
|- ( n e. ( 1 ... N ) -> n e. NN ) |
95 |
|
fvco3 |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) ) |
96 |
1 94 95
|
syl2an |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) ) |
97 |
|
ffvelrn |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) ) |
98 |
1 94 97
|
syl2an |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) ) |
99 |
98
|
elin2d |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) e. ( RR X. RR ) ) |
100 |
|
1st2nd2 |
|- ( ( F ` n ) e. ( RR X. RR ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) |
101 |
99 100
|
syl |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) |
102 |
101
|
fveq2d |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( (,) ` ( F ` n ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) ) |
103 |
|
df-ov |
|- ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) |
104 |
102 103
|
eqtr4di |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( (,) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) ) |
105 |
96 104
|
eqtrd |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) ) |
106 |
|
ioombl |
|- ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) e. dom vol |
107 |
105 106
|
eqeltrdi |
|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) e. dom vol ) |
108 |
107
|
ralrimiva |
|- ( ph -> A. n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol ) |
109 |
|
finiunmbl |
|- ( ( ( 1 ... N ) e. Fin /\ A. n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol ) -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol ) |
110 |
93 108 109
|
syl2anc |
|- ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol ) |
111 |
92 110
|
eqeltrrd |
|- ( ph -> L e. dom vol ) |
112 |
|
mblsplit |
|- ( ( L e. dom vol /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` K ) = ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) ) |
113 |
111 34 42 112
|
syl3anc |
|- ( ph -> ( vol* ` K ) = ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) ) |
114 |
113
|
oveq1d |
|- ( ph -> ( ( vol* ` K ) + C ) = ( ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) + C ) ) |
115 |
80 114
|
eqtr4d |
|- ( ph -> ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) = ( ( vol* ` K ) + C ) ) |
116 |
76 115
|
breqtrd |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( vol* ` K ) + C ) ) |
117 |
5 49
|
readdcld |
|- ( ph -> ( ( vol* ` E ) + C ) e. RR ) |
118 |
9
|
ovollb |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ K C_ U. ran ( (,) o. G ) ) -> ( vol* ` K ) <_ sup ( ran T , RR* , < ) ) |
119 |
7 33 118
|
sylancl |
|- ( ph -> ( vol* ` K ) <_ sup ( ran T , RR* , < ) ) |
120 |
42 35 117 119 10
|
letrd |
|- ( ph -> ( vol* ` K ) <_ ( ( vol* ` E ) + C ) ) |
121 |
42 117 49 120
|
leadd1dd |
|- ( ph -> ( ( vol* ` K ) + C ) <_ ( ( ( vol* ` E ) + C ) + C ) ) |
122 |
5
|
recnd |
|- ( ph -> ( vol* ` E ) e. CC ) |
123 |
122 78 78
|
addassd |
|- ( ph -> ( ( ( vol* ` E ) + C ) + C ) = ( ( vol* ` E ) + ( C + C ) ) ) |
124 |
121 123
|
breqtrd |
|- ( ph -> ( ( vol* ` K ) + C ) <_ ( ( vol* ` E ) + ( C + C ) ) ) |
125 |
48 59 58 116 124
|
letrd |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( vol* ` E ) + ( C + C ) ) ) |
126 |
48 58 50 125
|
leadd1dd |
|- ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) <_ ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) ) |
127 |
50
|
recnd |
|- ( ph -> ( C + C ) e. CC ) |
128 |
122 127 127
|
addassd |
|- ( ph -> ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) = ( ( vol* ` E ) + ( ( C + C ) + ( C + C ) ) ) ) |
129 |
|
2t2e4 |
|- ( 2 x. 2 ) = 4 |
130 |
129
|
oveq1i |
|- ( ( 2 x. 2 ) x. C ) = ( 4 x. C ) |
131 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
132 |
131 131 78
|
mulassd |
|- ( ph -> ( ( 2 x. 2 ) x. C ) = ( 2 x. ( 2 x. C ) ) ) |
133 |
78
|
2timesd |
|- ( ph -> ( 2 x. C ) = ( C + C ) ) |
134 |
133
|
oveq2d |
|- ( ph -> ( 2 x. ( 2 x. C ) ) = ( 2 x. ( C + C ) ) ) |
135 |
127
|
2timesd |
|- ( ph -> ( 2 x. ( C + C ) ) = ( ( C + C ) + ( C + C ) ) ) |
136 |
132 134 135
|
3eqtrd |
|- ( ph -> ( ( 2 x. 2 ) x. C ) = ( ( C + C ) + ( C + C ) ) ) |
137 |
130 136
|
eqtr3id |
|- ( ph -> ( 4 x. C ) = ( ( C + C ) + ( C + C ) ) ) |
138 |
137
|
oveq2d |
|- ( ph -> ( ( vol* ` E ) + ( 4 x. C ) ) = ( ( vol* ` E ) + ( ( C + C ) + ( C + C ) ) ) ) |
139 |
128 138
|
eqtr4d |
|- ( ph -> ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) = ( ( vol* ` E ) + ( 4 x. C ) ) ) |
140 |
126 139
|
breqtrd |
|- ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) ) |
141 |
29 51 55 57 140
|
letrd |
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) ) |