Step |
Hyp |
Ref |
Expression |
1 |
|
carageniuncl.o |
|- ( ph -> O e. OutMeas ) |
2 |
|
carageniuncl.s |
|- S = ( CaraGen ` O ) |
3 |
|
carageniuncl.3 |
|- ( ph -> M e. ZZ ) |
4 |
|
carageniuncl.z |
|- Z = ( ZZ>= ` M ) |
5 |
|
carageniuncl.e |
|- ( ph -> E : Z --> S ) |
6 |
|
eqid |
|- U. dom O = U. dom O |
7 |
5
|
ffvelrnda |
|- ( ( ph /\ n e. Z ) -> ( E ` n ) e. S ) |
8 |
|
elssuni |
|- ( ( E ` n ) e. S -> ( E ` n ) C_ U. S ) |
9 |
7 8
|
syl |
|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ U. S ) |
10 |
1 2
|
caragenuni |
|- ( ph -> U. S = U. dom O ) |
11 |
10
|
adantr |
|- ( ( ph /\ n e. Z ) -> U. S = U. dom O ) |
12 |
9 11
|
sseqtrd |
|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ U. dom O ) |
13 |
12
|
ralrimiva |
|- ( ph -> A. n e. Z ( E ` n ) C_ U. dom O ) |
14 |
|
iunss |
|- ( U_ n e. Z ( E ` n ) C_ U. dom O <-> A. n e. Z ( E ` n ) C_ U. dom O ) |
15 |
13 14
|
sylibr |
|- ( ph -> U_ n e. Z ( E ` n ) C_ U. dom O ) |
16 |
4
|
fvexi |
|- Z e. _V |
17 |
|
fvex |
|- ( E ` n ) e. _V |
18 |
16 17
|
iunex |
|- U_ n e. Z ( E ` n ) e. _V |
19 |
18
|
a1i |
|- ( ph -> U_ n e. Z ( E ` n ) e. _V ) |
20 |
|
elpwg |
|- ( U_ n e. Z ( E ` n ) e. _V -> ( U_ n e. Z ( E ` n ) e. ~P U. dom O <-> U_ n e. Z ( E ` n ) C_ U. dom O ) ) |
21 |
19 20
|
syl |
|- ( ph -> ( U_ n e. Z ( E ` n ) e. ~P U. dom O <-> U_ n e. Z ( E ` n ) C_ U. dom O ) ) |
22 |
15 21
|
mpbird |
|- ( ph -> U_ n e. Z ( E ` n ) e. ~P U. dom O ) |
23 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
24 |
1
|
adantr |
|- ( ( ph /\ a e. ~P U. dom O ) -> O e. OutMeas ) |
25 |
|
elpwi |
|- ( a e. ~P U. dom O -> a C_ U. dom O ) |
26 |
|
ssinss1 |
|- ( a C_ U. dom O -> ( a i^i U_ n e. Z ( E ` n ) ) C_ U. dom O ) |
27 |
25 26
|
syl |
|- ( a e. ~P U. dom O -> ( a i^i U_ n e. Z ( E ` n ) ) C_ U. dom O ) |
28 |
27
|
adantl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i U_ n e. Z ( E ` n ) ) C_ U. dom O ) |
29 |
24 6 28
|
omecl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) e. ( 0 [,] +oo ) ) |
30 |
23 29
|
sselid |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) e. RR* ) |
31 |
25
|
adantl |
|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. dom O ) |
32 |
31
|
ssdifssd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ U_ n e. Z ( E ` n ) ) C_ U. dom O ) |
33 |
24 6 32
|
omecl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) e. ( 0 [,] +oo ) ) |
34 |
23 33
|
sselid |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) e. RR* ) |
35 |
30 34
|
xaddcld |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* ) |
36 |
24 6 31
|
omecl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) e. ( 0 [,] +oo ) ) |
37 |
23 36
|
sselid |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) e. RR* ) |
38 |
|
pnfge |
|- ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ +oo ) |
39 |
35 38
|
syl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ +oo ) |
40 |
39
|
adantr |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) = +oo ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ +oo ) |
41 |
|
id |
|- ( ( O ` a ) = +oo -> ( O ` a ) = +oo ) |
42 |
41
|
eqcomd |
|- ( ( O ` a ) = +oo -> +oo = ( O ` a ) ) |
43 |
42
|
adantl |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) = +oo ) -> +oo = ( O ` a ) ) |
44 |
40 43
|
breqtrd |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) = +oo ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) ) |
45 |
|
simpl |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( ph /\ a e. ~P U. dom O ) ) |
46 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
47 |
|
0xr |
|- 0 e. RR* |
48 |
47
|
a1i |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> 0 e. RR* ) |
49 |
|
pnfxr |
|- +oo e. RR* |
50 |
49
|
a1i |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> +oo e. RR* ) |
51 |
45 36
|
syl |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) e. ( 0 [,] +oo ) ) |
52 |
41
|
necon3bi |
|- ( -. ( O ` a ) = +oo -> ( O ` a ) =/= +oo ) |
53 |
52
|
adantl |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) =/= +oo ) |
54 |
48 50 51 53
|
eliccelicod |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) e. ( 0 [,) +oo ) ) |
55 |
46 54
|
sselid |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) e. RR ) |
56 |
24
|
ad2antrr |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> O e. OutMeas ) |
57 |
31
|
ad2antrr |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> a C_ U. dom O ) |
58 |
|
simpr |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( O ` a ) e. RR ) |
59 |
58
|
adantr |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> ( O ` a ) e. RR ) |
60 |
3
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> M e. ZZ ) |
61 |
5
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> E : Z --> S ) |
62 |
|
simpr |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> x e. RR+ ) |
63 |
|
eqid |
|- ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) ) = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) ) |
64 |
|
fveq2 |
|- ( m = n -> ( E ` m ) = ( E ` n ) ) |
65 |
|
oveq2 |
|- ( m = n -> ( M ..^ m ) = ( M ..^ n ) ) |
66 |
65
|
iuneq1d |
|- ( m = n -> U_ i e. ( M ..^ m ) ( E ` i ) = U_ i e. ( M ..^ n ) ( E ` i ) ) |
67 |
64 66
|
difeq12d |
|- ( m = n -> ( ( E ` m ) \ U_ i e. ( M ..^ m ) ( E ` i ) ) = ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) ) |
68 |
67
|
cbvmptv |
|- ( m e. Z |-> ( ( E ` m ) \ U_ i e. ( M ..^ m ) ( E ` i ) ) ) = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) ) |
69 |
56 2 6 57 59 60 4 61 62 63 68
|
carageniuncllem2 |
|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) ) |
70 |
69
|
ralrimiva |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> A. x e. RR+ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) ) |
71 |
35
|
adantr |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* ) |
72 |
|
xralrple |
|- ( ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* /\ ( O ` a ) e. RR ) -> ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) <-> A. x e. RR+ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) ) ) |
73 |
71 58 72
|
syl2anc |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) <-> A. x e. RR+ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) ) ) |
74 |
70 73
|
mpbird |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) ) |
75 |
45 55 74
|
syl2anc |
|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) ) |
76 |
44 75
|
pm2.61dan |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) ) |
77 |
24 6 31
|
omelesplit |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) <_ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) ) |
78 |
35 37 76 77
|
xrletrid |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) = ( O ` a ) ) |
79 |
1 6 2 22 78
|
carageneld |
|- ( ph -> U_ n e. Z ( E ` n ) e. S ) |