MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ioombl1lem4 Structured version   Unicode version

Theorem ioombl1lem4 22512
Description: Lemma for ioombl1 22513. (Contributed by Mario Carneiro, 16-Jun-2014.)
Hypotheses
Ref Expression
ioombl1.b  |-  B  =  ( A (,) +oo )
ioombl1.a  |-  ( ph  ->  A  e.  RR )
ioombl1.e  |-  ( ph  ->  E  C_  RR )
ioombl1.v  |-  ( ph  ->  ( vol* `  E )  e.  RR )
ioombl1.c  |-  ( ph  ->  C  e.  RR+ )
ioombl1.s  |-  S  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
ioombl1.t  |-  T  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  G ) )
ioombl1.u  |-  U  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  H ) )
ioombl1.f1  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
ioombl1.f2  |-  ( ph  ->  E  C_  U. ran  ( (,)  o.  F ) )
ioombl1.f3  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( ( vol* `  E )  +  C
) )
ioombl1.p  |-  P  =  ( 1st `  ( F `  n )
)
ioombl1.q  |-  Q  =  ( 2nd `  ( F `  n )
)
ioombl1.g  |-  G  =  ( n  e.  NN  |->  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) ,  Q >. )
ioombl1.h  |-  H  =  ( n  e.  NN  |->  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. )
Assertion
Ref Expression
ioombl1lem4  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  <_  ( ( vol* `  E )  +  C ) )
Distinct variable groups:    B, n    C, n    n, E    n, F    n, G    n, H    ph, n    S, n
Allowed substitution hints:    A( n)    P( n)    Q( n)    T( n)    U( n)

Proof of Theorem ioombl1lem4
Dummy variables  x  j  k  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3682 . . . . 5  |-  ( E  i^i  B )  C_  E
21a1i 11 . . . 4  |-  ( ph  ->  ( E  i^i  B
)  C_  E )
3 ioombl1.e . . . 4  |-  ( ph  ->  E  C_  RR )
4 ioombl1.v . . . 4  |-  ( ph  ->  ( vol* `  E )  e.  RR )
5 ovolsscl 22437 . . . 4  |-  ( ( ( E  i^i  B
)  C_  E  /\  E  C_  RR  /\  ( vol* `  E )  e.  RR )  -> 
( vol* `  ( E  i^i  B ) )  e.  RR )
62, 3, 4, 5syl3anc 1264 . . 3  |-  ( ph  ->  ( vol* `  ( E  i^i  B ) )  e.  RR )
7 difss 3592 . . . . 5  |-  ( E 
\  B )  C_  E
87a1i 11 . . . 4  |-  ( ph  ->  ( E  \  B
)  C_  E )
9 ovolsscl 22437 . . . 4  |-  ( ( ( E  \  B
)  C_  E  /\  E  C_  RR  /\  ( vol* `  E )  e.  RR )  -> 
( vol* `  ( E  \  B ) )  e.  RR )
108, 3, 4, 9syl3anc 1264 . . 3  |-  ( ph  ->  ( vol* `  ( E  \  B ) )  e.  RR )
116, 10readdcld 9677 . 2  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  e.  RR )
12 ioombl1.b . . 3  |-  B  =  ( A (,) +oo )
13 ioombl1.a . . 3  |-  ( ph  ->  A  e.  RR )
14 ioombl1.c . . 3  |-  ( ph  ->  C  e.  RR+ )
15 ioombl1.s . . 3  |-  S  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
16 ioombl1.t . . 3  |-  T  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  G ) )
17 ioombl1.u . . 3  |-  U  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  H ) )
18 ioombl1.f1 . . 3  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
19 ioombl1.f2 . . 3  |-  ( ph  ->  E  C_  U. ran  ( (,)  o.  F ) )
20 ioombl1.f3 . . 3  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( ( vol* `  E )  +  C
) )
21 ioombl1.p . . 3  |-  P  =  ( 1st `  ( F `  n )
)
22 ioombl1.q . . 3  |-  Q  =  ( 2nd `  ( F `  n )
)
23 ioombl1.g . . 3  |-  G  =  ( n  e.  NN  |->  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) ,  Q >. )
24 ioombl1.h . . 3  |-  H  =  ( n  e.  NN  |->  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. )
2512, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem2 22510 . 2  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
2614rpred 11348 . . 3  |-  ( ph  ->  C  e.  RR )
274, 26readdcld 9677 . 2  |-  ( ph  ->  ( ( vol* `  E )  +  C
)  e.  RR )
2812, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem1 22509 . . . . . . . . 9  |-  ( ph  ->  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  H : NN --> (  <_  i^i  ( RR  X.  RR ) ) ) )
2928simpld 460 . . . . . . . 8  |-  ( ph  ->  G : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
30 eqid 2422 . . . . . . . . 9  |-  ( ( abs  o.  -  )  o.  G )  =  ( ( abs  o.  -  )  o.  G )
3130, 16ovolsf 22423 . . . . . . . 8  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  T : NN --> ( 0 [,) +oo ) )
3229, 31syl 17 . . . . . . 7  |-  ( ph  ->  T : NN --> ( 0 [,) +oo ) )
33 frn 5752 . . . . . . 7  |-  ( T : NN --> ( 0 [,) +oo )  ->  ran  T  C_  ( 0 [,) +oo ) )
3432, 33syl 17 . . . . . 6  |-  ( ph  ->  ran  T  C_  (
0 [,) +oo )
)
35 rge0ssre 11747 . . . . . 6  |-  ( 0 [,) +oo )  C_  RR
3634, 35syl6ss 3476 . . . . 5  |-  ( ph  ->  ran  T  C_  RR )
37 1nn 10627 . . . . . . . 8  |-  1  e.  NN
38 fdm 5750 . . . . . . . . 9  |-  ( T : NN --> ( 0 [,) +oo )  ->  dom  T  =  NN )
3932, 38syl 17 . . . . . . . 8  |-  ( ph  ->  dom  T  =  NN )
4037, 39syl5eleqr 2514 . . . . . . 7  |-  ( ph  ->  1  e.  dom  T
)
41 ne0i 3767 . . . . . . 7  |-  ( 1  e.  dom  T  ->  dom  T  =/=  (/) )
4240, 41syl 17 . . . . . 6  |-  ( ph  ->  dom  T  =/=  (/) )
43 dm0rn0 5070 . . . . . . 7  |-  ( dom 
T  =  (/)  <->  ran  T  =  (/) )
4443necon3bii 2688 . . . . . 6  |-  ( dom 
T  =/=  (/)  <->  ran  T  =/=  (/) )
4542, 44sylib 199 . . . . 5  |-  ( ph  ->  ran  T  =/=  (/) )
4632ffvelrnda 6037 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  e.  ( 0 [,) +oo ) )
4735, 46sseldi 3462 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  e.  RR )
48 eqid 2422 . . . . . . . . . . . . 13  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
4948, 15ovolsf 22423 . . . . . . . . . . . 12  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) +oo ) )
5018, 49syl 17 . . . . . . . . . . 11  |-  ( ph  ->  S : NN --> ( 0 [,) +oo ) )
5150ffvelrnda 6037 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  e.  ( 0 [,) +oo ) )
5235, 51sseldi 3462 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  e.  RR )
5325adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
54 simpr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  NN )
55 nnuz 11201 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
5654, 55syl6eleq 2517 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  ( ZZ>= `  1 )
)
57 simpl 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  ph )
58 elfznn 11835 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... j )  ->  n  e.  NN )
5930ovolfsf 22422 . . . . . . . . . . . . . . 15  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  G ) : NN --> ( 0 [,) +oo ) )
6029, 59syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( abs  o.  -  )  o.  G
) : NN --> ( 0 [,) +oo ) )
6160ffvelrnda 6037 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  e.  ( 0 [,) +oo )
)
6235, 61sseldi 3462 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  e.  RR )
6357, 58, 62syl2an 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  G
) `  n )  e.  RR )
6448ovolfsf 22422 . . . . . . . . . . . . . . . 16  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,) +oo ) )
6518, 64syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,) +oo ) )
6665ffvelrnda 6037 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  e.  ( 0 [,) +oo )
)
67 elrege0 11745 . . . . . . . . . . . . . 14  |-  ( ( ( ( abs  o.  -  )  o.  F
) `  n )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  F ) `  n
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  n
) ) )
6866, 67sylib 199 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  F
) `  n )  e.  RR  /\  0  <_ 
( ( ( abs 
o.  -  )  o.  F ) `  n
) ) )
6968simpld 460 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  e.  RR )
7057, 58, 69syl2an 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  n )  e.  RR )
7128simprd 464 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
72 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs  o.  -  )  o.  H )  =  ( ( abs  o.  -  )  o.  H )
7372ovolfsf 22422 . . . . . . . . . . . . . . . . . 18  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  H ) : NN --> ( 0 [,) +oo ) )
7471, 73syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs  o.  -  )  o.  H
) : NN --> ( 0 [,) +oo ) )
7574ffvelrnda 6037 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  e.  ( 0 [,) +oo )
)
76 elrege0 11745 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( abs  o.  -  )  o.  H
) `  n )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  H ) `  n
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  H ) `  n
) ) )
7775, 76sylib 199 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  H
) `  n )  e.  RR  /\  0  <_ 
( ( ( abs 
o.  -  )  o.  H ) `  n
) ) )
7877simprd 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( ( abs 
o.  -  )  o.  H ) `  n
) )
7977simpld 460 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  e.  RR )
8062, 79addge01d 10208 . . . . . . . . . . . . . 14  |-  ( (
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
) ) ) )
8178, 80mpbid 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  <_  (
( ( ( abs 
o.  -  )  o.  G ) `  n
)  +  ( ( ( abs  o.  -  )  o.  H ) `  n ) ) )
8212, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem3 22511 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  G
) `  n )  +  ( ( ( abs  o.  -  )  o.  H ) `  n
) )  =  ( ( ( abs  o.  -  )  o.  F
) `  n )
)
8381, 82breqtrd 4448 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  <_  (
( ( abs  o.  -  )  o.  F
) `  n )
)
8457, 58, 83syl2an 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  G
) `  n )  <_  ( ( ( abs 
o.  -  )  o.  F ) `  n
) )
8556, 63, 70, 84serle 12274 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  G
) ) `  j
)  <_  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  j
) )
8616fveq1i 5882 . . . . . . . . . 10  |-  ( T `
 j )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  j )
8715fveq1i 5882 . . . . . . . . . 10  |-  ( S `
 j )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  j )
8885, 86, 873brtr4g 4456 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  <_ 
( S `  j
) )
89 1zzd 10975 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  ZZ )
90 eqidd 2423 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  =  ( ( ( abs  o.  -  )  o.  F
) `  n )
)
9168simprd 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( ( abs 
o.  -  )  o.  F ) `  n
) )
92 frn 5752 . . . . . . . . . . . . . . . . . . . . 21  |-  ( S : NN --> ( 0 [,) +oo )  ->  ran  S  C_  ( 0 [,) +oo ) )
9350, 92syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  S  C_  (
0 [,) +oo )
)
94 icossxr 11726 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 [,) +oo )  C_  RR*
9593, 94syl6ss 3476 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ran  S  C_  RR* )
9695adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ran  S  C_ 
RR* )
97 ffn 5746 . . . . . . . . . . . . . . . . . . . 20  |-  ( S : NN --> ( 0 [,) +oo )  ->  S  Fn  NN )
9850, 97syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  S  Fn  NN )
99 fnfvelrn 6034 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  Fn  NN  /\  k  e.  NN )  ->  ( S `  k
)  e.  ran  S
)
10098, 99sylan 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e. 
ran  S )
101 supxrub 11617 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  S  C_  RR*  /\  ( S `  k )  e.  ran  S )  -> 
( S `  k
)  <_  sup ( ran  S ,  RR* ,  <  ) )
10296, 100, 101syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  <_  sup ( ran  S ,  RR* ,  <  ) )
103102ralrimiva 2836 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. k  e.  NN  ( S `  k )  <_  sup ( ran  S ,  RR* ,  <  )
)
104 breq2 4427 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( ( S `
 k )  <_  x 
<->  ( S `  k
)  <_  sup ( ran  S ,  RR* ,  <  ) ) )
105104ralbidv 2861 . . . . . . . . . . . . . . . . 17  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( A. k  e.  NN  ( S `  k )  <_  x  <->  A. k  e.  NN  ( S `  k )  <_  sup ( ran  S ,  RR* ,  <  )
) )
106105rspcev 3182 . . . . . . . . . . . . . . . 16  |-  ( ( 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 )
10725, 103, 106syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E. x  e.  RR  A. k  e.  NN  ( S `  k )  <_  x )
10855, 15, 89, 90, 69, 91, 107isumsup2 13903 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  ~~>  sup ( ran  S ,  RR ,  <  )
)
10993, 35syl6ss 3476 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ran  S  C_  RR )
110 fdm 5750 . . . . . . . . . . . . . . . . . . 19  |-  ( S : NN --> ( 0 [,) +oo )  ->  dom  S  =  NN )
11150, 110syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  S  =  NN )
11237, 111syl5eleqr 2514 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  dom  S
)
113 ne0i 3767 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  dom  S  ->  dom  S  =/=  (/) )
114112, 113syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  S  =/=  (/) )
115 dm0rn0 5070 . . . . . . . . . . . . . . . . 17  |-  ( dom 
S  =  (/)  <->  ran  S  =  (/) )
116115necon3bii 2688 . . . . . . . . . . . . . . . 16  |-  ( dom 
S  =/=  (/)  <->  ran  S  =/=  (/) )
117114, 116sylib 199 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ran  S  =/=  (/) )
118 breq1 4426 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( S `  k )  ->  (
z  <_  x  <->  ( S `  k )  <_  x
) )
119118ralrn 6040 . . . . . . . . . . . . . . . . . 18  |-  ( S  Fn  NN  ->  ( A. z  e.  ran  S  z  <_  x  <->  A. k  e.  NN  ( S `  k )  <_  x
) )
12098, 119syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A. z  e. 
ran  S  z  <_  x  <->  A. k  e.  NN  ( S `  k )  <_  x ) )
121120rexbidv 2936 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E. x  e.  RR  A. z  e. 
ran  S  z  <_  x  <->  E. x  e.  RR  A. k  e.  NN  ( S `  k )  <_  x ) )
122107, 121mpbird 235 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E. x  e.  RR  A. z  e.  ran  S  z  <_  x )
123 supxrre 11620 . . . . . . . . . . . . . . 15  |-  ( ( 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 ,  <  ) )
124109, 117, 122, 123syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  =  sup ( ran  S ,  RR ,  <  )
)
125108, 124breqtrrd 4450 . . . . . . . . . . . . 13  |-  ( ph  ->  S  ~~>  sup ( ran  S ,  RR* ,  <  )
)
126125adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  S  ~~>  sup ( ran  S ,  RR* ,  <  ) )
12715, 126syl5eqbrr 4458 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  F )
)  ~~>  sup ( ran  S ,  RR* ,  <  )
)
12869adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  n )  e.  RR )
12991adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  NN )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  F ) `  n
) )
13055, 54, 127, 128, 129climserle 13725 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) )
13187, 130syl5eqbr 4457 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  <_  sup ( ran  S ,  RR* ,  <  ) )
13247, 52, 53, 88, 131letrd 9799 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  <_  sup ( ran  S ,  RR* ,  <  ) )
133132ralrimiva 2836 . . . . . . 7  |-  ( ph  ->  A. j  e.  NN  ( T `  j )  <_  sup ( ran  S ,  RR* ,  <  )
)
134 breq2 4427 . . . . . . . . 9  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( ( T `
 j )  <_  x 
<->  ( T `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) ) )
135134ralbidv 2861 . . . . . . . 8  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( A. j  e.  NN  ( T `  j )  <_  x  <->  A. j  e.  NN  ( T `  j )  <_  sup ( ran  S ,  RR* ,  <  )
) )
136135rspcev 3182 . . . . . . 7  |-  ( ( 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 )
13725, 133, 136syl2anc 665 . . . . . 6  |-  ( ph  ->  E. x  e.  RR  A. j  e.  NN  ( T `  j )  <_  x )
138 ffn 5746 . . . . . . . . 9  |-  ( T : NN --> ( 0 [,) +oo )  ->  T  Fn  NN )
13932, 138syl 17 . . . . . . . 8  |-  ( ph  ->  T  Fn  NN )
140 breq1 4426 . . . . . . . . 9  |-  ( z  =  ( T `  j )  ->  (
z  <_  x  <->  ( T `  j )  <_  x
) )
141140ralrn 6040 . . . . . . . 8  |-  ( T  Fn  NN  ->  ( A. z  e.  ran  T  z  <_  x  <->  A. j  e.  NN  ( T `  j )  <_  x
) )
142139, 141syl 17 . . . . . . 7  |-  ( ph  ->  ( A. z  e. 
ran  T  z  <_  x  <->  A. j  e.  NN  ( T `  j )  <_  x ) )
143142rexbidv 2936 . . . . . 6  |-  ( ph  ->  ( E. x  e.  RR  A. z  e. 
ran  T  z  <_  x  <->  E. x  e.  RR  A. j  e.  NN  ( T `  j )  <_  x ) )
144137, 143mpbird 235 . . . . 5  |-  ( ph  ->  E. x  e.  RR  A. z  e.  ran  T  z  <_  x )
145 suprcl 10576 . . . . 5  |-  ( ( ran  T  C_  RR  /\ 
ran  T  =/=  (/)  /\  E. x  e.  RR  A. z  e.  ran  T  z  <_  x )  ->  sup ( ran  T ,  RR ,  <  )  e.  RR )
14636, 45, 144, 145syl3anc 1264 . . . 4  |-  ( ph  ->  sup ( ran  T ,  RR ,  <  )  e.  RR )
14772, 17ovolsf 22423 . . . . . . . 8  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  U : NN --> ( 0 [,) +oo ) )
14871, 147syl 17 . . . . . . 7  |-  ( ph  ->  U : NN --> ( 0 [,) +oo ) )
149 frn 5752 . . . . . . 7  |-  ( U : NN --> ( 0 [,) +oo )  ->  ran  U  C_  ( 0 [,) +oo ) )
150148, 149syl 17 . . . . . 6  |-  ( ph  ->  ran  U  C_  (
0 [,) +oo )
)
151150, 35syl6ss 3476 . . . . 5  |-  ( ph  ->  ran  U  C_  RR )
152 fdm 5750 . . . . . . . . 9  |-  ( U : NN --> ( 0 [,) +oo )  ->  dom  U  =  NN )
153148, 152syl 17 . . . . . . . 8  |-  ( ph  ->  dom  U  =  NN )
15437, 153syl5eleqr 2514 . . . . . . 7  |-  ( ph  ->  1  e.  dom  U
)
155 ne0i 3767 . . . . . . 7  |-  ( 1  e.  dom  U  ->  dom  U  =/=  (/) )
156154, 155syl 17 . . . . . 6  |-  ( ph  ->  dom  U  =/=  (/) )
157 dm0rn0 5070 . . . . . . 7  |-  ( dom 
U  =  (/)  <->  ran  U  =  (/) )
158157necon3bii 2688 . . . . . 6  |-  ( dom 
U  =/=  (/)  <->  ran  U  =/=  (/) )
159156, 158sylib 199 . . . . 5  |-  ( ph  ->  ran  U  =/=  (/) )
160148ffvelrnda 6037 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  e.  ( 0 [,) +oo ) )
16135, 160sseldi 3462 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  e.  RR )
16257, 58, 79syl2an 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  H
) `  n )  e.  RR )
163 elrege0 11745 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( abs  o.  -  )  o.  G
) `  n )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  G ) `  n
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  G ) `  n
) ) )
16461, 163sylib 199 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  G
) `  n )  e.  RR  /\  0  <_ 
( ( ( abs 
o.  -  )  o.  G ) `  n
) ) )
165164simprd 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( ( abs 
o.  -  )  o.  G ) `  n
) )
16679, 62addge02d 10209 . . . . . . . . . . . . . 14  |-  ( (
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
) ) ) )
167165, 166mpbid 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  <_  (
( ( ( abs 
o.  -  )  o.  G ) `  n
)  +  ( ( ( abs  o.  -  )  o.  H ) `  n ) ) )
168167, 82breqtrd 4448 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  <_  (
( ( abs  o.  -  )  o.  F
) `  n )
)
16957, 58, 168syl2an 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  H
) `  n )  <_  ( ( ( abs 
o.  -  )  o.  F ) `  n
) )
17056, 162, 70, 169serle 12274 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  j
)  <_  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  j
) )
17117fveq1i 5882 . . . . . . . . . 10  |-  ( U `
 j )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  j )
172170, 171, 873brtr4g 4456 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  <_ 
( S `  j
) )
173161, 52, 53, 172, 131letrd 9799 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  <_  sup ( ran  S ,  RR* ,  <  ) )
174173ralrimiva 2836 . . . . . . 7  |-  ( ph  ->  A. j  e.  NN  ( U `  j )  <_  sup ( ran  S ,  RR* ,  <  )
)
175 breq2 4427 . . . . . . . . 9  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( ( U `
 j )  <_  x 
<->  ( U `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) ) )
176175ralbidv 2861 . . . . . . . 8  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( A. j  e.  NN  ( U `  j )  <_  x  <->  A. j  e.  NN  ( U `  j )  <_  sup ( ran  S ,  RR* ,  <  )
) )
177176rspcev 3182 . . . . . . 7  |-  ( ( 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 )
17825, 174, 177syl2anc 665 . . . . . 6  |-  ( ph  ->  E. x  e.  RR  A. j  e.  NN  ( U `  j )  <_  x )
179 ffn 5746 . . . . . . . . 9  |-  ( U : NN --> ( 0 [,) +oo )  ->  U  Fn  NN )
180148, 179syl 17 . . . . . . . 8  |-  ( ph  ->  U  Fn  NN )
181 breq1 4426 . . . . . . . . 9  |-  ( z  =  ( U `  j )  ->  (
z  <_  x  <->  ( U `  j )  <_  x
) )
182181ralrn 6040 . . . . . . . 8  |-  ( U  Fn  NN  ->  ( A. z  e.  ran  U  z  <_  x  <->  A. j  e.  NN  ( U `  j )  <_  x
) )
183180, 182syl 17 . . . . . . 7  |-  ( ph  ->  ( A. z  e. 
ran  U  z  <_  x  <->  A. j  e.  NN  ( U `  j )  <_  x ) )
184183rexbidv 2936 . . . . . 6  |-  ( ph  ->  ( E. x  e.  RR  A. z  e. 
ran  U  z  <_  x  <->  E. x  e.  RR  A. j  e.  NN  ( U `  j )  <_  x ) )
185178, 184mpbird 235 . . . . 5  |-  ( ph  ->  E. x  e.  RR  A. z  e.  ran  U  z  <_  x )
186 suprcl 10576 . . . . 5  |-  ( ( ran  U  C_  RR  /\ 
ran  U  =/=  (/)  /\  E. x  e.  RR  A. z  e.  ran  U  z  <_  x )  ->  sup ( ran  U ,  RR ,  <  )  e.  RR )
187151, 159, 185, 186syl3anc 1264 . . . 4  |-  ( ph  ->  sup ( ran  U ,  RR ,  <  )  e.  RR )
188 ssralv 3525 . . . . . . . . . 10  |-  ( ( 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
) ) ) ) )
1891, 188ax-mp 5 . . . . . . . . 9  |-  ( 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
) ) ) )
19021breq1i 4430 . . . . . . . . . . . . 13  |-  ( P  <  x  <->  ( 1st `  ( F `  n
) )  <  x
)
191 ovolfcl 22417 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 )
) ) )
19218, 191sylan 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( 1st `  ( F `
 n ) )  e.  RR  /\  ( 2nd `  ( F `  n ) )  e.  RR  /\  ( 1st `  ( F `  n
) )  <_  ( 2nd `  ( F `  n ) ) ) )
193192simp1d 1017 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( F `  n
) )  e.  RR )
19421, 193syl5eqel 2511 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  P  e.  RR )
195194adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  P  e.  RR )
1961, 3syl5ss 3475 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E  i^i  B
)  C_  RR )
197196sselda 3464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( E  i^i  B ) )  ->  x  e.  RR )
198197adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  x  e.  RR )
199 ltle 9729 . . . . . . . . . . . . . . 15  |-  ( ( P  e.  RR  /\  x  e.  RR )  ->  ( P  <  x  ->  P  <_  x )
)
200195, 198, 199syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( P  <  x  ->  P  <_  x ) )
201 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
202 opex 4685 . . . . . . . . . . . . . . . . . . . 20  |-  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) ,  Q >.  e. 
_V
20323fvmpt2 5973 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 >. )
204201, 202, 203sylancl 666 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( G `
 n )  = 
<. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) ,  Q >. )
205204fveq2d 5885 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( G `  n
) )  =  ( 1st `  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) ,  Q >. ) )
20613adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  A  e.  RR )
207206, 194ifcld 3954 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  if ( P  <_  A ,  A ,  P )  e.  RR )
208192simp2d 1018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( F `  n
) )  e.  RR )
20922, 208syl5eqel 2511 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  Q  e.  RR )
210207, 209ifcld 3954 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
)  e.  RR )
211 op1stg 6819 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
212210, 209, 211syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( (
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
) )
213205, 212eqtrd 2463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( G `  n
) )  =  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) )
214213ad2ant2r 751 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) )
215210ad2ant2r 751 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
216207ad2ant2r 751 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  if ( P  <_  A ,  A ,  P )  e.  RR )
217196ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  ( E  i^i  B )  C_  RR )
218 simplr 760 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  x  e.  ( E  i^i  B ) )
219217, 218sseldd 3465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  x  e.  RR )
220209ad2ant2r 751 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  Q  e.  RR )
221 min1 11490 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 )
)
222216, 220, 221syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
)
22313ad2antrr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  A  e.  RR )
224 inss2 3683 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E  i^i  B )  C_  B
225224sseli 3460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( E  i^i  B )  ->  x  e.  B )
226225ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  x  e.  B
)
22713rexrd 9697 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A  e.  RR* )
228 pnfxr 11419 . . . . . . . . . . . . . . . . . . . . . . . 24  |- +oo  e.  RR*
229 elioo2 11684 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\ +oo  e.  RR* )  ->  (
x  e.  ( A (,) +oo )  <->  ( x  e.  RR  /\  A  < 
x  /\  x  < +oo ) ) )
230227, 228, 229sylancl 666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( x  e.  ( A (,) +oo )  <->  ( x  e.  RR  /\  A  <  x  /\  x  < +oo ) ) )
23112eleq2i 2499 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  B  <->  x  e.  ( A (,) +oo )
)
232 ltpnf 11429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  x  < +oo )
233232adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  A  <  x )  ->  x  < +oo )
234233pm4.71i 636 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  A  <  x )  <->  ( (
x  e.  RR  /\  A  <  x )  /\  x  < +oo ) )
235 df-3an 984 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  A  <  x  /\  x  < +oo )  <->  ( (
x  e.  RR  /\  A  <  x )  /\  x  < +oo ) )
236234, 235bitr4i 255 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  A  <  x )  <->  ( x  e.  RR  /\  A  < 
x  /\  x  < +oo ) )
237230, 231, 2363bitr4g 291 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  B  <->  ( x  e.  RR  /\  A  <  x ) ) )
238 simpr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  A  <  x )  ->  A  <  x )
239237, 238syl6bi 231 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  B  ->  A  <  x ) )
240239ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  ( x  e.  B  ->  A  <  x ) )
241226, 240mpd 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  A  <  x
)
242223, 219, 241ltled 9790 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  A  <_  x
)
243 simprr 764 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  P  <_  x
)
244 breq1 4426 . . . . . . . . . . . . . . . . . . 19  |-  ( A  =  if ( P  <_  A ,  A ,  P )  ->  ( A  <_  x  <->  if ( P  <_  A ,  A ,  P )  <_  x
) )
245 breq1 4426 . . . . . . . . . . . . . . . . . . 19  |-  ( P  =  if ( P  <_  A ,  A ,  P )  ->  ( P  <_  x  <->  if ( P  <_  A ,  A ,  P )  <_  x
) )
246244, 245ifboth 3947 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  <_  x  /\  P  <_  x )  ->  if ( P  <_  A ,  A ,  P )  <_  x )
247242, 243, 246syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  if ( P  <_  A ,  A ,  P )  <_  x
)
248215, 216, 219, 222, 247letrd 9799 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
)
249214, 248eqbrtrd 4444 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  ( 1st `  ( G `  n )
)  <_  x )
250249expr 618 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( P  <_  x  ->  ( 1st `  ( G `  n ) )  <_  x ) )
251200, 250syld 45 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( P  <  x  ->  ( 1st `  ( G `  n ) )  <_  x ) )
252190, 251syl5bir 221 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( F `  n )
)  <  x  ->  ( 1st `  ( G `
 n ) )  <_  x ) )
25322breq2i 4431 . . . . . . . . . . . . . 14  |-  ( x  <  Q  <->  x  <  ( 2nd `  ( F `
 n ) ) )
254209adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  Q  e.  RR )
255 ltle 9729 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR  /\  Q  e.  RR )  ->  ( x  <  Q  ->  x  <_  Q )
)
256198, 254, 255syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <  Q  ->  x  <_  Q ) )
257253, 256syl5bir 221 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <  ( 2nd `  ( F `  n
) )  ->  x  <_  Q ) )
258204fveq2d 5885 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( G `  n
) )  =  ( 2nd `  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) ,  Q >. ) )
259 op2ndg 6820 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
260210, 209, 259syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) ,  Q >. )  =  Q )
261258, 260eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( G `  n
) )  =  Q )
262261adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( 2nd `  ( G `  n ) )  =  Q )
263262breq2d 4435 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <_  ( 2nd `  ( G `  n
) )  <->  x  <_  Q ) )
264257, 263sylibrd 237 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <  ( 2nd `  ( F `  n
) )  ->  x  <_  ( 2nd `  ( G `  n )
) ) )
265252, 264anim12d 565 . . . . . . . . . . 11  |-  ( ( ( 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 )
) ) ) )
266265reximdva 2897 . . . . . . . . . 10  |-  ( (
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
) ) ) ) )
267266ralimdva 2830 . . . . . . . . 9  |-  ( 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 )
) ) ) )
268189, 267syl5 33 . . . . . . . 8  |-  ( 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 )
) ) ) )
269 ovolfioo 22418 . . . . . . . . 9  |-  ( ( 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 )
) ) ) )
2703, 18, 269syl2anc 665 . . . . . . . 8  |-  ( ph  ->  ( E  C_  U. ran  ( (,)  o.  F )  <->  A. x  e.  E  E. n  e.  NN  ( ( 1st `  ( F `  n )
)  <  x  /\  x  <  ( 2nd `  ( F `  n )
) ) ) )
271 ovolficc 22419 . . . . . . . . 9  |-  ( ( ( 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
) ) ) ) )
272196, 29, 271syl2anc 665 . . . . . . . 8  |-  ( 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
) ) ) ) )
273268, 270, 2723imtr4d 271 . . . . . . 7  |-  ( ph  ->  ( E  C_  U. ran  ( (,)  o.  F )  ->  ( E  i^i  B )  C_  U. ran  ( [,]  o.  G ) ) )
27419, 273mpd 15 . . . . . 6  |-  ( ph  ->  ( E  i^i  B
)  C_  U. ran  ( [,]  o.  G ) )
27516ovollb2 22440 . . . . . 6  |-  ( ( 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* ,  <  ) )
27629, 274, 275syl2anc 665 . . . . 5  |-  ( ph  ->  ( vol* `  ( E  i^i  B ) )  <_  sup ( ran  T ,  RR* ,  <  ) )
277 supxrre 11620 . . . . . 6  |-  ( ( 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 ,  <  ) )
27836, 45, 144, 277syl3anc 1264 . . . . 5  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  =  sup ( ran  T ,  RR ,  <  )
)
279276, 278breqtrd 4448 . . . 4  |-  ( ph  ->  ( vol* `  ( E  i^i  B ) )  <_  sup ( ran  T ,  RR ,  <  ) )
280 ssralv 3525 . . . . . . . . . 10  |-  ( ( 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
) ) ) ) )
2817, 280ax-mp 5 . . . . . . . . 9  |-  ( 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
) ) ) )
282194adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  P  e.  RR )
2837, 3syl5ss 3475 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E  \  B
)  C_  RR )
284283sselda 3464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( E  \  B ) )  ->  x  e.  RR )
285284adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  x  e.  RR )
286282, 285, 199syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  ( P  <  x  ->  P  <_  x ) )
287190, 286syl5bir 221 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( F `  n )
)  <  x  ->  P  <_  x ) )
288 opex 4685 . . . . . . . . . . . . . . . . . 18  |-  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >.  e.  _V
28924fvmpt2 5973 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) >. )
290201, 288, 289sylancl 666 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( H `
 n )  = 
<. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. )
291290fveq2d 5885 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( H `  n
) )  =  ( 1st `  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. ) )
292 op1stg 6819 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
293194, 210, 292syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. )  =  P )
294291, 293eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( H `  n
) )  =  P )
295294adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  ( 1st `  ( H `  n ) )  =  P )
296295breq1d 4433 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( H `  n )
)  <_  x  <->  P  <_  x ) )
297287, 296sylibrd 237 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( F `  n )
)  <  x  ->  ( 1st `  ( H `
 n ) )  <_  x ) )
298209adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  Q  e.  RR )
299285, 298, 255syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <  Q  ->  x  <_  Q ) )
300283ad2antrr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( E  \  B )  C_  RR )
301 simplr 760 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  e.  ( E  \  B ) )
302300, 301sseldd 3465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  e.  RR )
30313ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  A  e.  RR )
304194ad2ant2r 751 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  P  e.  RR )
305303, 304ifcld 3954 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  if ( P  <_  A ,  A ,  P )  e.  RR )
306 eldifn 3588 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( E  \  B )  ->  -.  x  e.  B )
307306ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  -.  x  e.  B )
308302biantrurd 510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( A  < 
x  <->  ( x  e.  RR  /\  A  < 
x ) ) )
309237ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( x  e.  B  <->  ( x  e.  RR  /\  A  < 
x ) ) )
310308, 309bitr4d 259 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( A  < 
x  <->  x  e.  B
) )
311307, 310mtbird 302 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  -.  A  <  x )
312302, 303lenltd 9788 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( x  <_  A 
<->  -.  A  <  x
) )
313311, 312mpbird 235 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  A
)
314 max2 11489 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  RR  /\  A  e.  RR )  ->  A  <_  if ( P  <_  A ,  A ,  P ) )
315304, 303, 314syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  A  <_  if ( P  <_  A ,  A ,  P )
)
316302, 303, 305, 313, 315letrd 9799 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  if ( P  <_  A ,  A ,  P )
)
317 simprr 764 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  Q
)
318 breq2 4427 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) )
319 breq2 4427 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) )
320318, 319ifboth 3947 . . . . . . . . . . . . . . . . 17  |-  ( ( x  <_  if ( P  <_  A ,  A ,  P )  /\  x  <_  Q )  ->  x  <_  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) )
321316, 317, 320syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) )
322290fveq2d 5885 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( H `  n
) )  =  ( 2nd `  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. ) )
323 op2ndg 6820 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
324194, 210, 323syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( (
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
) )
325322, 324eqtrd 2463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( H `  n
) )  =  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) )
326325ad2ant2r 751 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) )
327321, 326breqtrrd 4450 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  ( 2nd `  ( H `  n ) ) )
328327expr 618 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <_  Q  ->  x  <_  ( 2nd `  ( H `  n )
) ) )
329299, 328syld 45 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <  Q  ->  x  <_  ( 2nd `  ( H `  n )
) ) )
330253, 329syl5bir 221 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <  ( 2nd `  ( F `  n
) )  ->  x  <_  ( 2nd `  ( H `  n )
) ) )
331297, 330anim12d 565 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( ( 1st `  ( F `  n )
)  <  x  /\  x  <  ( 2nd `  ( F `  n )
) )  ->  (
( 1st `  ( H `  n )
)  <_  x  /\  x  <_  ( 2nd `  ( H `  n )
) ) ) )
332331reximdva 2897 . . . . . . . . . 10  |-  ( (
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
) ) ) ) )
333332ralimdva 2830 . . . . . . . . 9  |-  ( 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 )
) ) ) )
334281, 333syl5 33 . . . . . . . 8  |-  ( 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 )
) ) ) )
335 ovolficc 22419 . . . . . . . . 9  |-  ( ( ( 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 )
) ) ) )
336283, 71, 335syl2anc 665 . . . . . . . 8  |-  ( 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 )
) ) ) )
337334, 270, 3363imtr4d 271 . . . . . . 7  |-  ( ph  ->  ( E  C_  U. ran  ( (,)  o.  F )  ->  ( E  \  B )  C_  U. ran  ( [,]  o.  H ) ) )
33819, 337mpd 15 . . . . . 6  |-  ( ph  ->  ( E  \  B
)  C_  U. ran  ( [,]  o.  H ) )
33917ovollb2 22440 . . . . . 6  |-  ( ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  ( E  \  B )  C_  U.
ran  ( [,]  o.  H ) )  -> 
( vol* `  ( E  \  B ) )  <_  sup ( ran  U ,  RR* ,  <  ) )
34071, 338, 339syl2anc 665 . . . . 5  |-  ( ph  ->  ( vol* `  ( E  \  B ) )  <_  sup ( ran  U ,  RR* ,  <  ) )
341 supxrre 11620 . . . . . 6  |-  ( ( 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 ,  <  ) )
342151, 159, 185, 341syl3anc 1264 . . . . 5  |-  ( ph  ->  sup ( ran  U ,  RR* ,  <  )  =  sup ( ran  U ,  RR ,  <  )
)
343340, 342breqtrd 4448 . . . 4  |-  ( ph  ->  ( vol* `  ( E  \  B ) )  <_  sup ( ran  U ,  RR ,  <  ) )
3446, 10, 146, 187, 279, 343le2addd 10239 . . 3  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  <_  ( sup ( ran  T ,  RR ,  <  )  +  sup ( ran  U ,  RR ,  <  ) ) )
345 eqidd 2423 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  =  ( ( ( abs  o.  -  )  o.  G
) `  n )
)
34655, 16, 89, 345, 62, 165, 137isumsup2 13903 . . . . 5  |-  ( ph  ->  T  ~~>  sup ( ran  T ,  RR ,  <  )
)
347 seqex 12221 . . . . . . 7  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  F )
)  e.  _V
34815, 347eqeltri 2503 . . . . . 6  |-  S  e. 
_V
349348a1i 11 . . . . 5  |-  ( ph  ->  S  e.  _V )
350 eqidd 2423 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  =  ( ( ( abs  o.  -  )  o.  H
) `  n )
)
35155, 17, 89, 350, 79, 78, 178isumsup2 13903 . . . . 5  |-  ( ph  ->  U  ~~>  sup ( ran  U ,  RR ,  <  )
)
35247recnd 9676 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  e.  CC )
353161recnd 9676 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  e.  CC )
35462recnd 9676 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  e.  CC )
35557, 58, 354syl2an 479 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  G
) `  n )  e.  CC )
35679recnd 9676 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  e.  CC )
35757, 58, 356syl2an 479 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  H
) `  n )  e.  CC )
35882eqcomd 2430 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  =  ( ( ( ( abs 
o.  -  )  o.  G ) `  n
)  +  ( ( ( abs  o.  -  )  o.  H ) `  n ) ) )
35957, 58, 358syl2an 479 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  n )  =  ( ( ( ( abs  o.  -  )  o.  G ) `  n )  +  ( ( ( abs  o.  -  )  o.  H
) `  n )
) )
36056, 355, 357, 359seradd 12261 . . . . . 6  |-  ( (
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 ) ) )
36186, 171oveq12i 6317 . . . . . 6  |-  ( ( T `  j )  +  ( U `  j ) )  =  ( (  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  G )
) `  j )  +  (  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  H )
) `  j )
)
362360, 87, 3613eqtr4g 2488 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  =  ( ( T `  j )  +  ( U `  j ) ) )
36355, 89, 346, 349, 351, 352, 353, 362climadd 13694 . . . 4  |-  ( ph  ->  S  ~~>  ( sup ( ran  T ,  RR ,  <  )  +  sup ( ran  U ,  RR ,  <  ) ) )
364 climuni 13615 . . . 4  |-  ( ( 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* ,  <  ) )
365363, 125, 364syl2anc 665 . . 3  |-  ( ph  ->  ( sup ( ran 
T ,  RR ,  <  )  +  sup ( ran  U ,  RR ,  <  ) )  =  sup ( ran  S ,  RR* ,  <  ) )
366344, 365breqtrd 4448 . 2  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  <_  sup ( ran  S ,  RR* ,  <  ) )
36711, 25, 27, 366, 20letrd 9799 1  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  <_  ( ( vol* `  E )  +  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   _Vcvv 3080    \ cdif 3433    i^i cin 3435    C_ wss 3436   (/)c0 3761   ifcif 3911   <.cop 4004   U.cuni 4219   class class class wbr 4423    |-> cmpt 4482    X. cxp 4851   dom cdm 4853   ran crn 4854    o. ccom 4857    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6305   1stc1st 6805   2ndc2nd 6806   supcsup 7963   CCcc 9544   RRcr 9545   0cc0 9546   1c1 9547    + caddc 9549   +oocpnf 9679   RR*cxr 9681    < clt 9682    <_ cle 9683    - cmin 9867   NNcn 10616   ZZ>=cuz 11166   RR+crp 11309   (,)cioo 11642   [,)cico 11644   [,]cicc 11645   ...cfz 11791    seqcseq 12219   abscabs 13297    ~~> cli 13547   vol*covol 22411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-inf2 8155  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623  ax-pre-sup 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-oadd 7197  df-er 7374  df-map 7485  df-pm 7486  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-sup 7965  df-inf 7966  df-oi 8034  df-card 8381  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-n0 10877  df-z 10945  df-uz 11167  df-q 11272  df-rp 11310  df-ioo 11646  df-ico 11648  df-icc 11649  df-fz 11792  df-fzo 11923  df-fl 12034  df-seq 12220  df-exp 12279  df-hash 12522  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-clim 13551  df-rlim 13552  df-sum 13752  df-ovol 22414
This theorem is referenced by:  ioombl1  22513
  Copyright terms: Public domain W3C validator