| 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 |
|
ffvelcdm |
|- ( ( 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 ) ) ) |