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 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
5 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
6 |
|
rexpssxrxp |
|- ( RR X. RR ) C_ ( RR* X. RR* ) |
7 |
5 6
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) |
8 |
|
fss |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) ) |
9 |
1 7 8
|
sylancl |
|- ( ph -> F : NN --> ( RR* X. RR* ) ) |
10 |
|
fco |
|- ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR ) |
11 |
4 9 10
|
sylancr |
|- ( ph -> ( (,) o. F ) : NN --> ~P RR ) |
12 |
11
|
frnd |
|- ( ph -> ran ( (,) o. F ) C_ ~P RR ) |
13 |
|
sspwuni |
|- ( ran ( (,) o. F ) C_ ~P RR <-> U. ran ( (,) o. F ) C_ RR ) |
14 |
12 13
|
sylib |
|- ( ph -> U. ran ( (,) o. F ) C_ RR ) |
15 |
|
elpwi |
|- ( z e. ~P RR -> z C_ RR ) |
16 |
15
|
ad2antrl |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> z C_ RR ) |
17 |
|
simprr |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( vol* ` z ) e. RR ) |
18 |
|
rphalfcl |
|- ( r e. RR+ -> ( r / 2 ) e. RR+ ) |
19 |
18
|
rphalfcld |
|- ( r e. RR+ -> ( ( r / 2 ) / 2 ) e. RR+ ) |
20 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) ) |
21 |
20
|
ovolgelb |
|- ( ( z C_ RR /\ ( vol* ` z ) e. RR /\ ( ( r / 2 ) / 2 ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) |
22 |
16 17 19 21
|
syl2an3an |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) |
23 |
1
|
ad3antrrr |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
24 |
2
|
ad3antrrr |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) |
25 |
|
eqid |
|- U. ran ( (,) o. F ) = U. ran ( (,) o. F ) |
26 |
17
|
adantr |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( vol* ` z ) e. RR ) |
27 |
26
|
adantr |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> ( vol* ` z ) e. RR ) |
28 |
18
|
adantl |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ ) |
29 |
28
|
adantr |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> ( r / 2 ) e. RR+ ) |
30 |
29
|
rphalfcld |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> ( ( r / 2 ) / 2 ) e. RR+ ) |
31 |
|
elmapi |
|- ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) ) |
32 |
31
|
ad2antrl |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) ) |
33 |
|
simprrl |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> z C_ U. ran ( (,) o. f ) ) |
34 |
|
simprrr |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) |
35 |
23 24 3 25 27 30 32 33 20 34
|
uniioombllem6 |
|- ( ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( z C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` z ) + ( ( r / 2 ) / 2 ) ) ) ) ) -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( ( vol* ` z ) + ( 4 x. ( ( r / 2 ) / 2 ) ) ) ) |
36 |
22 35
|
rexlimddv |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( ( vol* ` z ) + ( 4 x. ( ( r / 2 ) / 2 ) ) ) ) |
37 |
|
rpcn |
|- ( r e. RR+ -> r e. CC ) |
38 |
37
|
adantl |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> r e. CC ) |
39 |
|
2cnd |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> 2 e. CC ) |
40 |
|
2ne0 |
|- 2 =/= 0 |
41 |
40
|
a1i |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> 2 =/= 0 ) |
42 |
38 39 39 41 41
|
divdiv1d |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( ( r / 2 ) / 2 ) = ( r / ( 2 x. 2 ) ) ) |
43 |
|
2t2e4 |
|- ( 2 x. 2 ) = 4 |
44 |
43
|
oveq2i |
|- ( r / ( 2 x. 2 ) ) = ( r / 4 ) |
45 |
42 44
|
eqtrdi |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( ( r / 2 ) / 2 ) = ( r / 4 ) ) |
46 |
45
|
oveq2d |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( 4 x. ( ( r / 2 ) / 2 ) ) = ( 4 x. ( r / 4 ) ) ) |
47 |
|
4cn |
|- 4 e. CC |
48 |
47
|
a1i |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> 4 e. CC ) |
49 |
|
4ne0 |
|- 4 =/= 0 |
50 |
49
|
a1i |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> 4 =/= 0 ) |
51 |
38 48 50
|
divcan2d |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( 4 x. ( r / 4 ) ) = r ) |
52 |
46 51
|
eqtrd |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( 4 x. ( ( r / 2 ) / 2 ) ) = r ) |
53 |
52
|
oveq2d |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( ( vol* ` z ) + ( 4 x. ( ( r / 2 ) / 2 ) ) ) = ( ( vol* ` z ) + r ) ) |
54 |
36 53
|
breqtrd |
|- ( ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) /\ r e. RR+ ) -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( ( vol* ` z ) + r ) ) |
55 |
54
|
ralrimiva |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> A. r e. RR+ ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( ( vol* ` z ) + r ) ) |
56 |
|
inss1 |
|- ( z i^i U. ran ( (,) o. F ) ) C_ z |
57 |
56
|
a1i |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( z i^i U. ran ( (,) o. F ) ) C_ z ) |
58 |
|
ovolsscl |
|- ( ( ( z i^i U. ran ( (,) o. F ) ) C_ z /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) e. RR ) |
59 |
57 16 17 58
|
syl3anc |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) e. RR ) |
60 |
|
difssd |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( z \ U. ran ( (,) o. F ) ) C_ z ) |
61 |
|
ovolsscl |
|- ( ( ( z \ U. ran ( (,) o. F ) ) C_ z /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) e. RR ) |
62 |
60 16 17 61
|
syl3anc |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) e. RR ) |
63 |
59 62
|
readdcld |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) e. RR ) |
64 |
|
alrple |
|- ( ( ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) e. RR /\ ( vol* ` z ) e. RR ) -> ( ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( vol* ` z ) <-> A. r e. RR+ ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( ( vol* ` z ) + r ) ) ) |
65 |
63 17 64
|
syl2anc |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( vol* ` z ) <-> A. r e. RR+ ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( ( vol* ` z ) + r ) ) ) |
66 |
55 65
|
mpbird |
|- ( ( ph /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( vol* ` z ) ) |
67 |
66
|
expr |
|- ( ( ph /\ z e. ~P RR ) -> ( ( vol* ` z ) e. RR -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( vol* ` z ) ) ) |
68 |
67
|
ralrimiva |
|- ( ph -> A. z e. ~P RR ( ( vol* ` z ) e. RR -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( vol* ` z ) ) ) |
69 |
|
ismbl2 |
|- ( U. ran ( (,) o. F ) e. dom vol <-> ( U. ran ( (,) o. F ) C_ RR /\ A. z e. ~P RR ( ( vol* ` z ) e. RR -> ( ( vol* ` ( z i^i U. ran ( (,) o. F ) ) ) + ( vol* ` ( z \ U. ran ( (,) o. F ) ) ) ) <_ ( vol* ` z ) ) ) ) |
70 |
14 68 69
|
sylanbrc |
|- ( ph -> U. ran ( (,) o. F ) e. dom vol ) |