Step |
Hyp |
Ref |
Expression |
1 |
|
elxr |
|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) ) |
2 |
|
ioossre |
|- ( A (,) +oo ) C_ RR |
3 |
2
|
a1i |
|- ( A e. RR -> ( A (,) +oo ) C_ RR ) |
4 |
|
elpwi |
|- ( x e. ~P RR -> x C_ RR ) |
5 |
|
simplrl |
|- ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> x C_ RR ) |
6 |
|
simplrr |
|- ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> ( vol* ` x ) e. RR ) |
7 |
|
simpr |
|- ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> y e. RR+ ) |
8 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) ) |
9 |
8
|
ovolgelb |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR /\ y e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) |
10 |
5 6 7 9
|
syl3anc |
|- ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) |
11 |
|
eqid |
|- ( A (,) +oo ) = ( A (,) +oo ) |
12 |
|
simplll |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> A e. RR ) |
13 |
5
|
adantr |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> x C_ RR ) |
14 |
6
|
adantr |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> ( vol* ` x ) e. RR ) |
15 |
|
simplr |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> y e. RR+ ) |
16 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) ) ) |
17 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. ) ) ) |
18 |
|
simprl |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) |
19 |
|
elovolmlem |
|- ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> f : NN --> ( <_ i^i ( RR X. RR ) ) ) |
20 |
18 19
|
sylib |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) ) |
21 |
|
simprrl |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> x C_ U. ran ( (,) o. f ) ) |
22 |
|
simprrr |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) |
23 |
|
eqid |
|- ( 1st ` ( f ` n ) ) = ( 1st ` ( f ` n ) ) |
24 |
|
eqid |
|- ( 2nd ` ( f ` n ) ) = ( 2nd ` ( f ` n ) ) |
25 |
|
2fveq3 |
|- ( m = n -> ( 1st ` ( f ` m ) ) = ( 1st ` ( f ` n ) ) ) |
26 |
25
|
breq1d |
|- ( m = n -> ( ( 1st ` ( f ` m ) ) <_ A <-> ( 1st ` ( f ` n ) ) <_ A ) ) |
27 |
26 25
|
ifbieq2d |
|- ( m = n -> if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) = if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) ) |
28 |
|
2fveq3 |
|- ( m = n -> ( 2nd ` ( f ` m ) ) = ( 2nd ` ( f ` n ) ) ) |
29 |
27 28
|
breq12d |
|- ( m = n -> ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) <-> if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) ) ) |
30 |
29 27 28
|
ifbieq12d |
|- ( m = n -> if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) = if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) ) |
31 |
30 28
|
opeq12d |
|- ( m = n -> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. = <. if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) >. ) |
32 |
31
|
cbvmptv |
|- ( m e. NN |-> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) = ( n e. NN |-> <. if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) >. ) |
33 |
25 30
|
opeq12d |
|- ( m = n -> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. = <. ( 1st ` ( f ` n ) ) , if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) >. ) |
34 |
33
|
cbvmptv |
|- ( m e. NN |-> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. ) = ( n e. NN |-> <. ( 1st ` ( f ` n ) ) , if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) >. ) |
35 |
11 12 13 14 15 8 16 17 20 21 22 23 24 32 34
|
ioombl1lem4 |
|- ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) |
36 |
10 35
|
rexlimddv |
|- ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) |
37 |
36
|
ralrimiva |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> A. y e. RR+ ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) |
38 |
|
inss1 |
|- ( x i^i ( A (,) +oo ) ) C_ x |
39 |
|
ovolsscl |
|- ( ( ( x i^i ( A (,) +oo ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A (,) +oo ) ) ) e. RR ) |
40 |
38 39
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A (,) +oo ) ) ) e. RR ) |
41 |
40
|
adantl |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i ( A (,) +oo ) ) ) e. RR ) |
42 |
|
difss |
|- ( x \ ( A (,) +oo ) ) C_ x |
43 |
|
ovolsscl |
|- ( ( ( x \ ( A (,) +oo ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A (,) +oo ) ) ) e. RR ) |
44 |
42 43
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A (,) +oo ) ) ) e. RR ) |
45 |
44
|
adantl |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ ( A (,) +oo ) ) ) e. RR ) |
46 |
41 45
|
readdcld |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) e. RR ) |
47 |
|
simprr |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) e. RR ) |
48 |
|
alrple |
|- ( ( ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) e. RR /\ ( vol* ` x ) e. RR ) -> ( ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) <-> A. y e. RR+ ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) ) |
49 |
46 47 48
|
syl2anc |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) <-> A. y e. RR+ ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) ) |
50 |
37 49
|
mpbird |
|- ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) |
51 |
50
|
expr |
|- ( ( A e. RR /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) ) |
52 |
4 51
|
sylan2 |
|- ( ( A e. RR /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) ) |
53 |
52
|
ralrimiva |
|- ( A e. RR -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) ) |
54 |
|
ismbl2 |
|- ( ( A (,) +oo ) e. dom vol <-> ( ( A (,) +oo ) C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) ) ) |
55 |
3 53 54
|
sylanbrc |
|- ( A e. RR -> ( A (,) +oo ) e. dom vol ) |
56 |
|
oveq1 |
|- ( A = +oo -> ( A (,) +oo ) = ( +oo (,) +oo ) ) |
57 |
|
iooid |
|- ( +oo (,) +oo ) = (/) |
58 |
56 57
|
eqtrdi |
|- ( A = +oo -> ( A (,) +oo ) = (/) ) |
59 |
|
0mbl |
|- (/) e. dom vol |
60 |
58 59
|
eqeltrdi |
|- ( A = +oo -> ( A (,) +oo ) e. dom vol ) |
61 |
|
oveq1 |
|- ( A = -oo -> ( A (,) +oo ) = ( -oo (,) +oo ) ) |
62 |
|
ioomax |
|- ( -oo (,) +oo ) = RR |
63 |
61 62
|
eqtrdi |
|- ( A = -oo -> ( A (,) +oo ) = RR ) |
64 |
|
rembl |
|- RR e. dom vol |
65 |
63 64
|
eqeltrdi |
|- ( A = -oo -> ( A (,) +oo ) e. dom vol ) |
66 |
55 60 65
|
3jaoi |
|- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A (,) +oo ) e. dom vol ) |
67 |
1 66
|
sylbi |
|- ( A e. RR* -> ( A (,) +oo ) e. dom vol ) |