Step |
Hyp |
Ref |
Expression |
1 |
|
r19.26 |
|- ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) <-> ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) ) |
2 |
|
eqid |
|- seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) = seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) |
3 |
|
eqid |
|- ( n e. NN |-> ( vol ` A ) ) = ( n e. NN |-> ( vol ` A ) ) |
4 |
2 3
|
voliun |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
5 |
1 4
|
sylanbr |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
6 |
5
|
an32s |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ A. n e. NN ( vol ` A ) e. RR ) -> ( vol ` U_ n e. NN A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
7 |
|
nfra1 |
|- F/ n A. n e. NN A e. dom vol |
8 |
|
nfra1 |
|- F/ n A. n e. NN ( vol ` A ) e. RR |
9 |
7 8
|
nfan |
|- F/ n ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) |
10 |
|
simpr |
|- ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> n e. NN ) |
11 |
|
rspa |
|- ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> A e. dom vol ) |
12 |
|
volf |
|- vol : dom vol --> ( 0 [,] +oo ) |
13 |
12
|
ffvelrni |
|- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) ) |
14 |
11 13
|
syl |
|- ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,] +oo ) ) |
15 |
3
|
fvmpt2 |
|- ( ( n e. NN /\ ( vol ` A ) e. ( 0 [,] +oo ) ) -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) ) |
16 |
10 14 15
|
syl2anc |
|- ( ( A. n e. NN A e. dom vol /\ n e. NN ) -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) ) |
17 |
16
|
adantlr |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) ) |
18 |
17
|
ex |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> ( n e. NN -> ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) ) ) |
19 |
9 18
|
ralrimi |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> A. n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = ( vol ` A ) ) |
20 |
9 19
|
esumeq2d |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = sum* n e. NN ( vol ` A ) ) |
21 |
|
simpr |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> A. n e. NN ( vol ` A ) e. RR ) |
22 |
21
|
r19.21bi |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) e. RR ) |
23 |
14
|
adantlr |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,] +oo ) ) |
24 |
|
0xr |
|- 0 e. RR* |
25 |
|
pnfxr |
|- +oo e. RR* |
26 |
|
elicc1 |
|- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( vol ` A ) e. ( 0 [,] +oo ) <-> ( ( vol ` A ) e. RR* /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) <_ +oo ) ) ) |
27 |
24 25 26
|
mp2an |
|- ( ( vol ` A ) e. ( 0 [,] +oo ) <-> ( ( vol ` A ) e. RR* /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) <_ +oo ) ) |
28 |
27
|
simp2bi |
|- ( ( vol ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( vol ` A ) ) |
29 |
23 28
|
syl |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> 0 <_ ( vol ` A ) ) |
30 |
|
ltpnf |
|- ( ( vol ` A ) e. RR -> ( vol ` A ) < +oo ) |
31 |
22 30
|
syl |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) < +oo ) |
32 |
|
0re |
|- 0 e. RR |
33 |
|
elico2 |
|- ( ( 0 e. RR /\ +oo e. RR* ) -> ( ( vol ` A ) e. ( 0 [,) +oo ) <-> ( ( vol ` A ) e. RR /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) < +oo ) ) ) |
34 |
32 25 33
|
mp2an |
|- ( ( vol ` A ) e. ( 0 [,) +oo ) <-> ( ( vol ` A ) e. RR /\ 0 <_ ( vol ` A ) /\ ( vol ` A ) < +oo ) ) |
35 |
22 29 31 34
|
syl3anbrc |
|- ( ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,) +oo ) ) |
36 |
9 35 3
|
fmptdf |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> ( n e. NN |-> ( vol ` A ) ) : NN --> ( 0 [,) +oo ) ) |
37 |
|
nfmpt1 |
|- F/_ n ( n e. NN |-> ( vol ` A ) ) |
38 |
37
|
esumfsupre |
|- ( ( n e. NN |-> ( vol ` A ) ) : NN --> ( 0 [,) +oo ) -> sum* n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
39 |
36 38
|
syl |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( ( n e. NN |-> ( vol ` A ) ) ` n ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
40 |
20 39
|
eqtr3d |
|- ( ( A. n e. NN A e. dom vol /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( vol ` A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
41 |
40
|
adantlr |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ A. n e. NN ( vol ` A ) e. RR ) -> sum* n e. NN ( vol ` A ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` A ) ) ) , RR* , < ) ) |
42 |
6 41
|
eqtr4d |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ A. n e. NN ( vol ` A ) e. RR ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) ) |
43 |
|
simpr |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. n e. NN ( vol ` A ) = +oo ) |
44 |
|
nfv |
|- F/ k ( vol ` A ) = +oo |
45 |
|
nfcv |
|- F/_ n vol |
46 |
|
nfcsb1v |
|- F/_ n [_ k / n ]_ A |
47 |
45 46
|
nffv |
|- F/_ n ( vol ` [_ k / n ]_ A ) |
48 |
47
|
nfeq1 |
|- F/ n ( vol ` [_ k / n ]_ A ) = +oo |
49 |
|
csbeq1a |
|- ( n = k -> A = [_ k / n ]_ A ) |
50 |
49
|
fveqeq2d |
|- ( n = k -> ( ( vol ` A ) = +oo <-> ( vol ` [_ k / n ]_ A ) = +oo ) ) |
51 |
44 48 50
|
cbvrexw |
|- ( E. n e. NN ( vol ` A ) = +oo <-> E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo ) |
52 |
43 51
|
sylib |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo ) |
53 |
46
|
nfel1 |
|- F/ n [_ k / n ]_ A e. dom vol |
54 |
49
|
eleq1d |
|- ( n = k -> ( A e. dom vol <-> [_ k / n ]_ A e. dom vol ) ) |
55 |
53 54
|
rspc |
|- ( k e. NN -> ( A. n e. NN A e. dom vol -> [_ k / n ]_ A e. dom vol ) ) |
56 |
55
|
impcom |
|- ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A e. dom vol ) |
57 |
|
iunmbl |
|- ( A. n e. NN A e. dom vol -> U_ n e. NN A e. dom vol ) |
58 |
57
|
adantr |
|- ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> U_ n e. NN A e. dom vol ) |
59 |
|
nfcv |
|- F/_ n NN |
60 |
|
nfcv |
|- F/_ n k |
61 |
59 60 46 49
|
ssiun2sf |
|- ( k e. NN -> [_ k / n ]_ A C_ U_ n e. NN A ) |
62 |
61
|
adantl |
|- ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A C_ U_ n e. NN A ) |
63 |
|
volss |
|- ( ( [_ k / n ]_ A e. dom vol /\ U_ n e. NN A e. dom vol /\ [_ k / n ]_ A C_ U_ n e. NN A ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) |
64 |
56 58 62 63
|
syl3anc |
|- ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) |
65 |
64
|
adantlr |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) |
66 |
65
|
adantlr |
|- ( ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) /\ k e. NN ) -> ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) |
67 |
66
|
ralrimiva |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> A. k e. NN ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) |
68 |
|
r19.29r |
|- ( ( E. k e. NN ( vol ` [_ k / n ]_ A ) = +oo /\ A. k e. NN ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> E. k e. NN ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) ) |
69 |
52 67 68
|
syl2anc |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. k e. NN ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) ) |
70 |
|
breq1 |
|- ( ( vol ` [_ k / n ]_ A ) = +oo -> ( ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) <-> +oo <_ ( vol ` U_ n e. NN A ) ) ) |
71 |
70
|
biimpa |
|- ( ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> +oo <_ ( vol ` U_ n e. NN A ) ) |
72 |
71
|
reximi |
|- ( E. k e. NN ( ( vol ` [_ k / n ]_ A ) = +oo /\ ( vol ` [_ k / n ]_ A ) <_ ( vol ` U_ n e. NN A ) ) -> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) ) |
73 |
69 72
|
syl |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) ) |
74 |
|
1nn |
|- 1 e. NN |
75 |
|
ne0i |
|- ( 1 e. NN -> NN =/= (/) ) |
76 |
|
r19.9rzv |
|- ( NN =/= (/) -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) ) ) |
77 |
74 75 76
|
mp2b |
|- ( +oo <_ ( vol ` U_ n e. NN A ) <-> E. k e. NN +oo <_ ( vol ` U_ n e. NN A ) ) |
78 |
73 77
|
sylibr |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> +oo <_ ( vol ` U_ n e. NN A ) ) |
79 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
80 |
12
|
ffvelrni |
|- ( U_ n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. ( 0 [,] +oo ) ) |
81 |
79 80
|
sseldi |
|- ( U_ n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. RR* ) |
82 |
57 81
|
syl |
|- ( A. n e. NN A e. dom vol -> ( vol ` U_ n e. NN A ) e. RR* ) |
83 |
82
|
ad2antrr |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( vol ` U_ n e. NN A ) e. RR* ) |
84 |
|
xgepnf |
|- ( ( vol ` U_ n e. NN A ) e. RR* -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> ( vol ` U_ n e. NN A ) = +oo ) ) |
85 |
83 84
|
syl |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( +oo <_ ( vol ` U_ n e. NN A ) <-> ( vol ` U_ n e. NN A ) = +oo ) ) |
86 |
78 85
|
mpbid |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( vol ` U_ n e. NN A ) = +oo ) |
87 |
|
nfdisj1 |
|- F/ n Disj_ n e. NN A |
88 |
7 87
|
nfan |
|- F/ n ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) |
89 |
|
nfre1 |
|- F/ n E. n e. NN ( vol ` A ) = +oo |
90 |
88 89
|
nfan |
|- F/ n ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) |
91 |
|
nnex |
|- NN e. _V |
92 |
91
|
a1i |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> NN e. _V ) |
93 |
14
|
3ad2antr3 |
|- ( ( A. n e. NN A e. dom vol /\ ( Disj_ n e. NN A /\ E. n e. NN ( vol ` A ) = +oo /\ n e. NN ) ) -> ( vol ` A ) e. ( 0 [,] +oo ) ) |
94 |
93
|
3anassrs |
|- ( ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) /\ n e. NN ) -> ( vol ` A ) e. ( 0 [,] +oo ) ) |
95 |
90 92 94 43
|
esumpinfval |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> sum* n e. NN ( vol ` A ) = +oo ) |
96 |
86 95
|
eqtr4d |
|- ( ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) /\ E. n e. NN ( vol ` A ) = +oo ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) ) |
97 |
|
exmid |
|- ( A. n e. NN ( vol ` A ) e. RR \/ -. A. n e. NN ( vol ` A ) e. RR ) |
98 |
|
rexnal |
|- ( E. n e. NN -. ( vol ` A ) e. RR <-> -. A. n e. NN ( vol ` A ) e. RR ) |
99 |
98
|
orbi2i |
|- ( ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN -. ( vol ` A ) e. RR ) <-> ( A. n e. NN ( vol ` A ) e. RR \/ -. A. n e. NN ( vol ` A ) e. RR ) ) |
100 |
97 99
|
mpbir |
|- ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN -. ( vol ` A ) e. RR ) |
101 |
|
r19.29 |
|- ( ( A. n e. NN A e. dom vol /\ E. n e. NN -. ( vol ` A ) e. RR ) -> E. n e. NN ( A e. dom vol /\ -. ( vol ` A ) e. RR ) ) |
102 |
|
xrge0nre |
|- ( ( ( vol ` A ) e. ( 0 [,] +oo ) /\ -. ( vol ` A ) e. RR ) -> ( vol ` A ) = +oo ) |
103 |
13 102
|
sylan |
|- ( ( A e. dom vol /\ -. ( vol ` A ) e. RR ) -> ( vol ` A ) = +oo ) |
104 |
103
|
reximi |
|- ( E. n e. NN ( A e. dom vol /\ -. ( vol ` A ) e. RR ) -> E. n e. NN ( vol ` A ) = +oo ) |
105 |
101 104
|
syl |
|- ( ( A. n e. NN A e. dom vol /\ E. n e. NN -. ( vol ` A ) e. RR ) -> E. n e. NN ( vol ` A ) = +oo ) |
106 |
105
|
ex |
|- ( A. n e. NN A e. dom vol -> ( E. n e. NN -. ( vol ` A ) e. RR -> E. n e. NN ( vol ` A ) = +oo ) ) |
107 |
106
|
orim2d |
|- ( A. n e. NN A e. dom vol -> ( ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN -. ( vol ` A ) e. RR ) -> ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN ( vol ` A ) = +oo ) ) ) |
108 |
100 107
|
mpi |
|- ( A. n e. NN A e. dom vol -> ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN ( vol ` A ) = +oo ) ) |
109 |
108
|
adantr |
|- ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) -> ( A. n e. NN ( vol ` A ) e. RR \/ E. n e. NN ( vol ` A ) = +oo ) ) |
110 |
42 96 109
|
mpjaodan |
|- ( ( A. n e. NN A e. dom vol /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sum* n e. NN ( vol ` A ) ) |