Step |
Hyp |
Ref |
Expression |
1 |
|
ioombl1.b |
|- B = ( A (,) +oo ) |
2 |
|
ioombl1.a |
|- ( ph -> A e. RR ) |
3 |
|
ioombl1.e |
|- ( ph -> E C_ RR ) |
4 |
|
ioombl1.v |
|- ( ph -> ( vol* ` E ) e. RR ) |
5 |
|
ioombl1.c |
|- ( ph -> C e. RR+ ) |
6 |
|
ioombl1.s |
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) ) |
7 |
|
ioombl1.t |
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) ) |
8 |
|
ioombl1.u |
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) ) |
9 |
|
ioombl1.f1 |
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
10 |
|
ioombl1.f2 |
|- ( ph -> E C_ U. ran ( (,) o. F ) ) |
11 |
|
ioombl1.f3 |
|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) ) |
12 |
|
ioombl1.p |
|- P = ( 1st ` ( F ` n ) ) |
13 |
|
ioombl1.q |
|- Q = ( 2nd ` ( F ` n ) ) |
14 |
|
ioombl1.g |
|- G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) |
15 |
|
ioombl1.h |
|- H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) |
16 |
|
inss1 |
|- ( E i^i B ) C_ E |
17 |
|
ovolsscl |
|- ( ( ( E i^i B ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i B ) ) e. RR ) |
18 |
16 3 4 17
|
mp3an2i |
|- ( ph -> ( vol* ` ( E i^i B ) ) e. RR ) |
19 |
|
difss |
|- ( E \ B ) C_ E |
20 |
|
ovolsscl |
|- ( ( ( E \ B ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ B ) ) e. RR ) |
21 |
19 3 4 20
|
mp3an2i |
|- ( ph -> ( vol* ` ( E \ B ) ) e. RR ) |
22 |
18 21
|
readdcld |
|- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) e. RR ) |
23 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
ioombl1lem2 |
|- ( ph -> sup ( ran S , RR* , < ) e. RR ) |
24 |
5
|
rpred |
|- ( ph -> C e. RR ) |
25 |
4 24
|
readdcld |
|- ( ph -> ( ( vol* ` E ) + C ) e. RR ) |
26 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
ioombl1lem1 |
|- ( ph -> ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) ) |
27 |
26
|
simpld |
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
28 |
|
eqid |
|- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G ) |
29 |
28 7
|
ovolsf |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) ) |
30 |
27 29
|
syl |
|- ( ph -> T : NN --> ( 0 [,) +oo ) ) |
31 |
30
|
frnd |
|- ( ph -> ran T C_ ( 0 [,) +oo ) ) |
32 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
33 |
31 32
|
sstrdi |
|- ( ph -> ran T C_ RR ) |
34 |
|
1nn |
|- 1 e. NN |
35 |
30
|
fdmd |
|- ( ph -> dom T = NN ) |
36 |
34 35
|
eleqtrrid |
|- ( ph -> 1 e. dom T ) |
37 |
36
|
ne0d |
|- ( ph -> dom T =/= (/) ) |
38 |
|
dm0rn0 |
|- ( dom T = (/) <-> ran T = (/) ) |
39 |
38
|
necon3bii |
|- ( dom T =/= (/) <-> ran T =/= (/) ) |
40 |
37 39
|
sylib |
|- ( ph -> ran T =/= (/) ) |
41 |
30
|
ffvelrnda |
|- ( ( ph /\ j e. NN ) -> ( T ` j ) e. ( 0 [,) +oo ) ) |
42 |
32 41
|
sselid |
|- ( ( ph /\ j e. NN ) -> ( T ` j ) e. RR ) |
43 |
|
eqid |
|- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F ) |
44 |
43 6
|
ovolsf |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) ) |
45 |
9 44
|
syl |
|- ( ph -> S : NN --> ( 0 [,) +oo ) ) |
46 |
45
|
ffvelrnda |
|- ( ( ph /\ j e. NN ) -> ( S ` j ) e. ( 0 [,) +oo ) ) |
47 |
32 46
|
sselid |
|- ( ( ph /\ j e. NN ) -> ( S ` j ) e. RR ) |
48 |
23
|
adantr |
|- ( ( ph /\ j e. NN ) -> sup ( ran S , RR* , < ) e. RR ) |
49 |
|
simpr |
|- ( ( ph /\ j e. NN ) -> j e. NN ) |
50 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
51 |
49 50
|
eleqtrdi |
|- ( ( ph /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) ) |
52 |
|
simpl |
|- ( ( ph /\ j e. NN ) -> ph ) |
53 |
|
elfznn |
|- ( n e. ( 1 ... j ) -> n e. NN ) |
54 |
28
|
ovolfsf |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) ) |
55 |
27 54
|
syl |
|- ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) ) |
56 |
55
|
ffvelrnda |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) ) |
57 |
32 56
|
sselid |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR ) |
58 |
52 53 57
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR ) |
59 |
43
|
ovolfsf |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) ) |
60 |
9 59
|
syl |
|- ( ph -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) ) |
61 |
60
|
ffvelrnda |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) ) |
62 |
|
elrege0 |
|- ( ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) ) |
63 |
61 62
|
sylib |
|- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) ) |
64 |
63
|
simpld |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR ) |
65 |
52 53 64
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR ) |
66 |
26
|
simprd |
|- ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) ) |
67 |
|
eqid |
|- ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H ) |
68 |
67
|
ovolfsf |
|- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) ) |
69 |
66 68
|
syl |
|- ( ph -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) ) |
70 |
69
|
ffvelrnda |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) ) |
71 |
|
elrege0 |
|- ( ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) ) |
72 |
70 71
|
sylib |
|- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) ) |
73 |
72
|
simprd |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) |
74 |
72
|
simpld |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR ) |
75 |
57 74
|
addge01d |
|- ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( ( abs o. - ) o. H ) ` n ) <-> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) ) |
76 |
73 75
|
mpbid |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) |
77 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
ioombl1lem3 |
|- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( ( abs o. - ) o. F ) ` n ) ) |
78 |
76 77
|
breqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) ) |
79 |
52 53 78
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) ) |
80 |
51 58 65 79
|
serle |
|- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) ) |
81 |
7
|
fveq1i |
|- ( T ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) |
82 |
6
|
fveq1i |
|- ( S ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) |
83 |
80 81 82
|
3brtr4g |
|- ( ( ph /\ j e. NN ) -> ( T ` j ) <_ ( S ` j ) ) |
84 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
85 |
|
eqidd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( abs o. - ) o. F ) ` n ) ) |
86 |
63
|
simprd |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) |
87 |
45
|
frnd |
|- ( ph -> ran S C_ ( 0 [,) +oo ) ) |
88 |
|
icossxr |
|- ( 0 [,) +oo ) C_ RR* |
89 |
87 88
|
sstrdi |
|- ( ph -> ran S C_ RR* ) |
90 |
89
|
adantr |
|- ( ( ph /\ k e. NN ) -> ran S C_ RR* ) |
91 |
45
|
ffnd |
|- ( ph -> S Fn NN ) |
92 |
|
fnfvelrn |
|- ( ( S Fn NN /\ k e. NN ) -> ( S ` k ) e. ran S ) |
93 |
91 92
|
sylan |
|- ( ( ph /\ k e. NN ) -> ( S ` k ) e. ran S ) |
94 |
|
supxrub |
|- ( ( ran S C_ RR* /\ ( S ` k ) e. ran S ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) ) |
95 |
90 93 94
|
syl2anc |
|- ( ( ph /\ k e. NN ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) ) |
96 |
95
|
ralrimiva |
|- ( ph -> A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) ) |
97 |
|
brralrspcev |
|- ( ( sup ( ran S , RR* , < ) e. RR /\ A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. k e. NN ( S ` k ) <_ x ) |
98 |
23 96 97
|
syl2anc |
|- ( ph -> E. x e. RR A. k e. NN ( S ` k ) <_ x ) |
99 |
50 6 84 85 64 86 98
|
isumsup2 |
|- ( ph -> S ~~> sup ( ran S , RR , < ) ) |
100 |
87 32
|
sstrdi |
|- ( ph -> ran S C_ RR ) |
101 |
45
|
fdmd |
|- ( ph -> dom S = NN ) |
102 |
34 101
|
eleqtrrid |
|- ( ph -> 1 e. dom S ) |
103 |
102
|
ne0d |
|- ( ph -> dom S =/= (/) ) |
104 |
|
dm0rn0 |
|- ( dom S = (/) <-> ran S = (/) ) |
105 |
104
|
necon3bii |
|- ( dom S =/= (/) <-> ran S =/= (/) ) |
106 |
103 105
|
sylib |
|- ( ph -> ran S =/= (/) ) |
107 |
|
breq1 |
|- ( z = ( S ` k ) -> ( z <_ x <-> ( S ` k ) <_ x ) ) |
108 |
107
|
ralrn |
|- ( S Fn NN -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) ) |
109 |
91 108
|
syl |
|- ( ph -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) ) |
110 |
109
|
rexbidv |
|- ( ph -> ( E. x e. RR A. z e. ran S z <_ x <-> E. x e. RR A. k e. NN ( S ` k ) <_ x ) ) |
111 |
98 110
|
mpbird |
|- ( ph -> E. x e. RR A. z e. ran S z <_ x ) |
112 |
|
supxrre |
|- ( ( ran S C_ RR /\ ran S =/= (/) /\ E. x e. RR A. z e. ran S z <_ x ) -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) ) |
113 |
100 106 111 112
|
syl3anc |
|- ( ph -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) ) |
114 |
99 113
|
breqtrrd |
|- ( ph -> S ~~> sup ( ran S , RR* , < ) ) |
115 |
114
|
adantr |
|- ( ( ph /\ j e. NN ) -> S ~~> sup ( ran S , RR* , < ) ) |
116 |
6 115
|
eqbrtrrid |
|- ( ( ph /\ j e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. F ) ) ~~> sup ( ran S , RR* , < ) ) |
117 |
64
|
adantlr |
|- ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR ) |
118 |
86
|
adantlr |
|- ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) |
119 |
50 49 116 117 118
|
climserle |
|- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) <_ sup ( ran S , RR* , < ) ) |
120 |
82 119
|
eqbrtrid |
|- ( ( ph /\ j e. NN ) -> ( S ` j ) <_ sup ( ran S , RR* , < ) ) |
121 |
42 47 48 83 120
|
letrd |
|- ( ( ph /\ j e. NN ) -> ( T ` j ) <_ sup ( ran S , RR* , < ) ) |
122 |
121
|
ralrimiva |
|- ( ph -> A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) ) |
123 |
|
brralrspcev |
|- ( ( sup ( ran S , RR* , < ) e. RR /\ A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. j e. NN ( T ` j ) <_ x ) |
124 |
23 122 123
|
syl2anc |
|- ( ph -> E. x e. RR A. j e. NN ( T ` j ) <_ x ) |
125 |
30
|
ffnd |
|- ( ph -> T Fn NN ) |
126 |
|
breq1 |
|- ( z = ( T ` j ) -> ( z <_ x <-> ( T ` j ) <_ x ) ) |
127 |
126
|
ralrn |
|- ( T Fn NN -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) ) |
128 |
125 127
|
syl |
|- ( ph -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) ) |
129 |
128
|
rexbidv |
|- ( ph -> ( E. x e. RR A. z e. ran T z <_ x <-> E. x e. RR A. j e. NN ( T ` j ) <_ x ) ) |
130 |
124 129
|
mpbird |
|- ( ph -> E. x e. RR A. z e. ran T z <_ x ) |
131 |
33 40 130
|
suprcld |
|- ( ph -> sup ( ran T , RR , < ) e. RR ) |
132 |
67 8
|
ovolsf |
|- ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) ) |
133 |
66 132
|
syl |
|- ( ph -> U : NN --> ( 0 [,) +oo ) ) |
134 |
133
|
frnd |
|- ( ph -> ran U C_ ( 0 [,) +oo ) ) |
135 |
134 32
|
sstrdi |
|- ( ph -> ran U C_ RR ) |
136 |
133
|
fdmd |
|- ( ph -> dom U = NN ) |
137 |
34 136
|
eleqtrrid |
|- ( ph -> 1 e. dom U ) |
138 |
137
|
ne0d |
|- ( ph -> dom U =/= (/) ) |
139 |
|
dm0rn0 |
|- ( dom U = (/) <-> ran U = (/) ) |
140 |
139
|
necon3bii |
|- ( dom U =/= (/) <-> ran U =/= (/) ) |
141 |
138 140
|
sylib |
|- ( ph -> ran U =/= (/) ) |
142 |
133
|
ffvelrnda |
|- ( ( ph /\ j e. NN ) -> ( U ` j ) e. ( 0 [,) +oo ) ) |
143 |
32 142
|
sselid |
|- ( ( ph /\ j e. NN ) -> ( U ` j ) e. RR ) |
144 |
52 53 74
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR ) |
145 |
|
elrege0 |
|- ( ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) ) |
146 |
56 145
|
sylib |
|- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) ) |
147 |
146
|
simprd |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) |
148 |
74 57
|
addge02d |
|- ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( ( abs o. - ) o. G ) ` n ) <-> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) ) |
149 |
147 148
|
mpbid |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) |
150 |
149 77
|
breqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) ) |
151 |
52 53 150
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) ) |
152 |
51 144 65 151
|
serle |
|- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) ) |
153 |
8
|
fveq1i |
|- ( U ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) |
154 |
152 153 82
|
3brtr4g |
|- ( ( ph /\ j e. NN ) -> ( U ` j ) <_ ( S ` j ) ) |
155 |
143 47 48 154 120
|
letrd |
|- ( ( ph /\ j e. NN ) -> ( U ` j ) <_ sup ( ran S , RR* , < ) ) |
156 |
155
|
ralrimiva |
|- ( ph -> A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) ) |
157 |
|
brralrspcev |
|- ( ( sup ( ran S , RR* , < ) e. RR /\ A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. j e. NN ( U ` j ) <_ x ) |
158 |
23 156 157
|
syl2anc |
|- ( ph -> E. x e. RR A. j e. NN ( U ` j ) <_ x ) |
159 |
133
|
ffnd |
|- ( ph -> U Fn NN ) |
160 |
|
breq1 |
|- ( z = ( U ` j ) -> ( z <_ x <-> ( U ` j ) <_ x ) ) |
161 |
160
|
ralrn |
|- ( U Fn NN -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) ) |
162 |
159 161
|
syl |
|- ( ph -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) ) |
163 |
162
|
rexbidv |
|- ( ph -> ( E. x e. RR A. z e. ran U z <_ x <-> E. x e. RR A. j e. NN ( U ` j ) <_ x ) ) |
164 |
158 163
|
mpbird |
|- ( ph -> E. x e. RR A. z e. ran U z <_ x ) |
165 |
135 141 164
|
suprcld |
|- ( ph -> sup ( ran U , RR , < ) e. RR ) |
166 |
|
ssralv |
|- ( ( E i^i B ) C_ E -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) ) |
167 |
16 166
|
ax-mp |
|- ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) |
168 |
12
|
breq1i |
|- ( P < x <-> ( 1st ` ( F ` n ) ) < x ) |
169 |
|
ovolfcl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) ) |
170 |
9 169
|
sylan |
|- ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) ) |
171 |
170
|
simp1d |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR ) |
172 |
12 171
|
eqeltrid |
|- ( ( ph /\ n e. NN ) -> P e. RR ) |
173 |
172
|
adantlr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> P e. RR ) |
174 |
16 3
|
sstrid |
|- ( ph -> ( E i^i B ) C_ RR ) |
175 |
174
|
sselda |
|- ( ( ph /\ x e. ( E i^i B ) ) -> x e. RR ) |
176 |
175
|
adantr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> x e. RR ) |
177 |
|
ltle |
|- ( ( P e. RR /\ x e. RR ) -> ( P < x -> P <_ x ) ) |
178 |
173 176 177
|
syl2anc |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) ) |
179 |
|
simpr |
|- ( ( ph /\ n e. NN ) -> n e. NN ) |
180 |
|
opex |
|- <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V |
181 |
14
|
fvmpt2 |
|- ( ( n e. NN /\ <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) |
182 |
179 180 181
|
sylancl |
|- ( ( ph /\ n e. NN ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) |
183 |
182
|
fveq2d |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) ) |
184 |
2
|
adantr |
|- ( ( ph /\ n e. NN ) -> A e. RR ) |
185 |
184 172
|
ifcld |
|- ( ( ph /\ n e. NN ) -> if ( P <_ A , A , P ) e. RR ) |
186 |
170
|
simp2d |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR ) |
187 |
13 186
|
eqeltrid |
|- ( ( ph /\ n e. NN ) -> Q e. RR ) |
188 |
185 187
|
ifcld |
|- ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) |
189 |
|
op1stg |
|- ( ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR /\ Q e. RR ) -> ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
190 |
188 187 189
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
191 |
183 190
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
192 |
191
|
ad2ant2r |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
193 |
188
|
ad2ant2r |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) |
194 |
185
|
ad2ant2r |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) e. RR ) |
195 |
174
|
ad2antrr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( E i^i B ) C_ RR ) |
196 |
|
simplr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. ( E i^i B ) ) |
197 |
195 196
|
sseldd |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. RR ) |
198 |
187
|
ad2ant2r |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> Q e. RR ) |
199 |
|
min1 |
|- ( ( if ( P <_ A , A , P ) e. RR /\ Q e. RR ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ if ( P <_ A , A , P ) ) |
200 |
194 198 199
|
syl2anc |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ if ( P <_ A , A , P ) ) |
201 |
2
|
ad2antrr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A e. RR ) |
202 |
|
elinel2 |
|- ( x e. ( E i^i B ) -> x e. B ) |
203 |
202
|
ad2antlr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. B ) |
204 |
2
|
rexrd |
|- ( ph -> A e. RR* ) |
205 |
|
pnfxr |
|- +oo e. RR* |
206 |
|
elioo2 |
|- ( ( A e. RR* /\ +oo e. RR* ) -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) ) |
207 |
204 205 206
|
sylancl |
|- ( ph -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) ) |
208 |
1
|
eleq2i |
|- ( x e. B <-> x e. ( A (,) +oo ) ) |
209 |
|
ltpnf |
|- ( x e. RR -> x < +oo ) |
210 |
209
|
adantr |
|- ( ( x e. RR /\ A < x ) -> x < +oo ) |
211 |
210
|
pm4.71i |
|- ( ( x e. RR /\ A < x ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) ) |
212 |
|
df-3an |
|- ( ( x e. RR /\ A < x /\ x < +oo ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) ) |
213 |
211 212
|
bitr4i |
|- ( ( x e. RR /\ A < x ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) |
214 |
207 208 213
|
3bitr4g |
|- ( ph -> ( x e. B <-> ( x e. RR /\ A < x ) ) ) |
215 |
|
simpr |
|- ( ( x e. RR /\ A < x ) -> A < x ) |
216 |
214 215
|
syl6bi |
|- ( ph -> ( x e. B -> A < x ) ) |
217 |
216
|
ad2antrr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( x e. B -> A < x ) ) |
218 |
203 217
|
mpd |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A < x ) |
219 |
201 197 218
|
ltled |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A <_ x ) |
220 |
|
simprr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> P <_ x ) |
221 |
|
breq1 |
|- ( A = if ( P <_ A , A , P ) -> ( A <_ x <-> if ( P <_ A , A , P ) <_ x ) ) |
222 |
|
breq1 |
|- ( P = if ( P <_ A , A , P ) -> ( P <_ x <-> if ( P <_ A , A , P ) <_ x ) ) |
223 |
221 222
|
ifboth |
|- ( ( A <_ x /\ P <_ x ) -> if ( P <_ A , A , P ) <_ x ) |
224 |
219 220 223
|
syl2anc |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) <_ x ) |
225 |
193 194 197 200 224
|
letrd |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ x ) |
226 |
192 225
|
eqbrtrd |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) <_ x ) |
227 |
226
|
expr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P <_ x -> ( 1st ` ( G ` n ) ) <_ x ) ) |
228 |
178 227
|
syld |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> ( 1st ` ( G ` n ) ) <_ x ) ) |
229 |
168 228
|
syl5bir |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( G ` n ) ) <_ x ) ) |
230 |
13
|
breq2i |
|- ( x < Q <-> x < ( 2nd ` ( F ` n ) ) ) |
231 |
187
|
adantlr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> Q e. RR ) |
232 |
|
ltle |
|- ( ( x e. RR /\ Q e. RR ) -> ( x < Q -> x <_ Q ) ) |
233 |
176 231 232
|
syl2anc |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) ) |
234 |
230 233
|
syl5bir |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ Q ) ) |
235 |
182
|
fveq2d |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) ) |
236 |
|
op2ndg |
|- ( ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR /\ Q e. RR ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q ) |
237 |
188 187 236
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q ) |
238 |
235 237
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q ) |
239 |
238
|
adantlr |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q ) |
240 |
239
|
breq2d |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x <_ ( 2nd ` ( G ` n ) ) <-> x <_ Q ) ) |
241 |
234 240
|
sylibrd |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( G ` n ) ) ) ) |
242 |
229 241
|
anim12d |
|- ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) ) |
243 |
242
|
reximdva |
|- ( ( ph /\ x e. ( E i^i B ) ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) ) |
244 |
243
|
ralimdva |
|- ( ph -> ( A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) ) |
245 |
167 244
|
syl5 |
|- ( ph -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) ) |
246 |
|
ovolfioo |
|- ( ( E C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) ) |
247 |
3 9 246
|
syl2anc |
|- ( ph -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) ) |
248 |
|
ovolficc |
|- ( ( ( E i^i B ) C_ RR /\ G : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( E i^i B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) ) |
249 |
174 27 248
|
syl2anc |
|- ( ph -> ( ( E i^i B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) ) |
250 |
245 247 249
|
3imtr4d |
|- ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E i^i B ) C_ U. ran ( [,] o. G ) ) ) |
251 |
10 250
|
mpd |
|- ( ph -> ( E i^i B ) C_ U. ran ( [,] o. G ) ) |
252 |
7
|
ovollb2 |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E i^i B ) C_ U. ran ( [,] o. G ) ) -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) ) |
253 |
27 251 252
|
syl2anc |
|- ( ph -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) ) |
254 |
|
supxrre |
|- ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) ) |
255 |
33 40 130 254
|
syl3anc |
|- ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) ) |
256 |
253 255
|
breqtrd |
|- ( ph -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR , < ) ) |
257 |
|
ssralv |
|- ( ( E \ B ) C_ E -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) ) |
258 |
19 257
|
ax-mp |
|- ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) |
259 |
172
|
adantlr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> P e. RR ) |
260 |
19 3
|
sstrid |
|- ( ph -> ( E \ B ) C_ RR ) |
261 |
260
|
sselda |
|- ( ( ph /\ x e. ( E \ B ) ) -> x e. RR ) |
262 |
261
|
adantr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> x e. RR ) |
263 |
259 262 177
|
syl2anc |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) ) |
264 |
168 263
|
syl5bir |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> P <_ x ) ) |
265 |
|
opex |
|- <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V |
266 |
15
|
fvmpt2 |
|- ( ( n e. NN /\ <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) |
267 |
179 265 266
|
sylancl |
|- ( ( ph /\ n e. NN ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) |
268 |
267
|
fveq2d |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) ) |
269 |
|
op1stg |
|- ( ( P e. RR /\ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P ) |
270 |
172 188 269
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P ) |
271 |
268 270
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P ) |
272 |
271
|
adantlr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P ) |
273 |
272
|
breq1d |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( H ` n ) ) <_ x <-> P <_ x ) ) |
274 |
264 273
|
sylibrd |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( H ` n ) ) <_ x ) ) |
275 |
187
|
adantlr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> Q e. RR ) |
276 |
262 275 232
|
syl2anc |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) ) |
277 |
260
|
ad2antrr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( E \ B ) C_ RR ) |
278 |
|
simplr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. ( E \ B ) ) |
279 |
277 278
|
sseldd |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. RR ) |
280 |
2
|
ad2antrr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A e. RR ) |
281 |
172
|
ad2ant2r |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> P e. RR ) |
282 |
280 281
|
ifcld |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> if ( P <_ A , A , P ) e. RR ) |
283 |
|
eldifn |
|- ( x e. ( E \ B ) -> -. x e. B ) |
284 |
283
|
ad2antlr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. x e. B ) |
285 |
279
|
biantrurd |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> ( x e. RR /\ A < x ) ) ) |
286 |
214
|
ad2antrr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( x e. B <-> ( x e. RR /\ A < x ) ) ) |
287 |
285 286
|
bitr4d |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> x e. B ) ) |
288 |
284 287
|
mtbird |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. A < x ) |
289 |
279 280 288
|
nltled |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ A ) |
290 |
|
max2 |
|- ( ( P e. RR /\ A e. RR ) -> A <_ if ( P <_ A , A , P ) ) |
291 |
281 280 290
|
syl2anc |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A <_ if ( P <_ A , A , P ) ) |
292 |
279 280 282 289 291
|
letrd |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( P <_ A , A , P ) ) |
293 |
|
simprr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ Q ) |
294 |
|
breq2 |
|- ( if ( P <_ A , A , P ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( x <_ if ( P <_ A , A , P ) <-> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) ) |
295 |
|
breq2 |
|- ( Q = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( x <_ Q <-> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) ) |
296 |
294 295
|
ifboth |
|- ( ( x <_ if ( P <_ A , A , P ) /\ x <_ Q ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
297 |
292 293 296
|
syl2anc |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
298 |
267
|
fveq2d |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) ) |
299 |
|
op2ndg |
|- ( ( P e. RR /\ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) -> ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
300 |
172 188 299
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
301 |
298 300
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
302 |
301
|
ad2ant2r |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) |
303 |
297 302
|
breqtrrd |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ ( 2nd ` ( H ` n ) ) ) |
304 |
303
|
expr |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x <_ Q -> x <_ ( 2nd ` ( H ` n ) ) ) ) |
305 |
276 304
|
syld |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ ( 2nd ` ( H ` n ) ) ) ) |
306 |
230 305
|
syl5bir |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( H ` n ) ) ) ) |
307 |
274 306
|
anim12d |
|- ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) ) |
308 |
307
|
reximdva |
|- ( ( ph /\ x e. ( E \ B ) ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) ) |
309 |
308
|
ralimdva |
|- ( ph -> ( A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) ) |
310 |
258 309
|
syl5 |
|- ( ph -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) ) |
311 |
|
ovolficc |
|- ( ( ( E \ B ) C_ RR /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( E \ B ) C_ U. ran ( [,] o. H ) <-> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) ) |
312 |
260 66 311
|
syl2anc |
|- ( ph -> ( ( E \ B ) C_ U. ran ( [,] o. H ) <-> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) ) |
313 |
310 247 312
|
3imtr4d |
|- ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E \ B ) C_ U. ran ( [,] o. H ) ) ) |
314 |
10 313
|
mpd |
|- ( ph -> ( E \ B ) C_ U. ran ( [,] o. H ) ) |
315 |
8
|
ovollb2 |
|- ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E \ B ) C_ U. ran ( [,] o. H ) ) -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) ) |
316 |
66 314 315
|
syl2anc |
|- ( ph -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) ) |
317 |
|
supxrre |
|- ( ( ran U C_ RR /\ ran U =/= (/) /\ E. x e. RR A. z e. ran U z <_ x ) -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) ) |
318 |
135 141 164 317
|
syl3anc |
|- ( ph -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) ) |
319 |
316 318
|
breqtrd |
|- ( ph -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR , < ) ) |
320 |
18 21 131 165 256 319
|
le2addd |
|- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) ) |
321 |
|
eqidd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( ( abs o. - ) o. G ) ` n ) ) |
322 |
50 7 84 321 57 147 124
|
isumsup2 |
|- ( ph -> T ~~> sup ( ran T , RR , < ) ) |
323 |
|
seqex |
|- seq 1 ( + , ( ( abs o. - ) o. F ) ) e. _V |
324 |
6 323
|
eqeltri |
|- S e. _V |
325 |
324
|
a1i |
|- ( ph -> S e. _V ) |
326 |
|
eqidd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( ( ( abs o. - ) o. H ) ` n ) ) |
327 |
50 8 84 326 74 73 158
|
isumsup2 |
|- ( ph -> U ~~> sup ( ran U , RR , < ) ) |
328 |
42
|
recnd |
|- ( ( ph /\ j e. NN ) -> ( T ` j ) e. CC ) |
329 |
143
|
recnd |
|- ( ( ph /\ j e. NN ) -> ( U ` j ) e. CC ) |
330 |
57
|
recnd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC ) |
331 |
52 53 330
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC ) |
332 |
74
|
recnd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC ) |
333 |
52 53 332
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC ) |
334 |
77
|
eqcomd |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) |
335 |
52 53 334
|
syl2an |
|- ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) |
336 |
51 331 333 335
|
seradd |
|- ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) ) ) |
337 |
81 153
|
oveq12i |
|- ( ( T ` j ) + ( U ` j ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) ) |
338 |
336 82 337
|
3eqtr4g |
|- ( ( ph /\ j e. NN ) -> ( S ` j ) = ( ( T ` j ) + ( U ` j ) ) ) |
339 |
50 84 322 325 327 328 329 338
|
climadd |
|- ( ph -> S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) ) |
340 |
|
climuni |
|- ( ( S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) /\ S ~~> sup ( ran S , RR* , < ) ) -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) ) |
341 |
339 114 340
|
syl2anc |
|- ( ph -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) ) |
342 |
320 341
|
breqtrd |
|- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ sup ( ran S , RR* , < ) ) |
343 |
22 23 25 342 11
|
letrd |
|- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( ( vol* ` E ) + C ) ) |