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

Theorem ioombl1lem4 22263
Description: Lemma for ioombl1 22264. (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 3659 . . . . 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 22189 . . . 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 1230 . . 3  |-  ( ph  ->  ( vol* `  ( E  i^i  B ) )  e.  RR )
7 difss 3570 . . . . 5  |-  ( E 
\  B )  C_  E
87a1i 11 . . . 4  |-  ( ph  ->  ( E  \  B
)  C_  E )
9 ovolsscl 22189 . . . 4  |-  ( ( ( E  \  B
)  C_  E  /\  E  C_  RR  /\  ( vol* `  E )  e.  RR )  -> 
( vol* `  ( E  \  B ) )  e.  RR )
108, 3, 4, 9syl3anc 1230 . . 3  |-  ( ph  ->  ( vol* `  ( E  \  B ) )  e.  RR )
116, 10readdcld 9653 . 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 22261 . 2  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
2614rpred 11304 . . 3  |-  ( ph  ->  C  e.  RR )
274, 26readdcld 9653 . 2  |-  ( ph  ->  ( ( vol* `  E )  +  C
)  e.  RR )
2812, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem1 22260 . . . . . . . . 9  |-  ( ph  ->  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  H : NN --> (  <_  i^i  ( RR  X.  RR ) ) ) )
2928simpld 457 . . . . . . . 8  |-  ( ph  ->  G : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
30 eqid 2402 . . . . . . . . 9  |-  ( ( abs  o.  -  )  o.  G )  =  ( ( abs  o.  -  )  o.  G )
3130, 16ovolsf 22176 . . . . . . . 8  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  T : NN --> ( 0 [,) +oo ) )
3229, 31syl 17 . . . . . . 7  |-  ( ph  ->  T : NN --> ( 0 [,) +oo ) )
33 frn 5720 . . . . . . 7  |-  ( T : NN --> ( 0 [,) +oo )  ->  ran  T  C_  ( 0 [,) +oo ) )
3432, 33syl 17 . . . . . 6  |-  ( ph  ->  ran  T  C_  (
0 [,) +oo )
)
35 rge0ssre 11682 . . . . . 6  |-  ( 0 [,) +oo )  C_  RR
3634, 35syl6ss 3454 . . . . 5  |-  ( ph  ->  ran  T  C_  RR )
37 1nn 10587 . . . . . . . 8  |-  1  e.  NN
38 fdm 5718 . . . . . . . . 9  |-  ( T : NN --> ( 0 [,) +oo )  ->  dom  T  =  NN )
3932, 38syl 17 . . . . . . . 8  |-  ( ph  ->  dom  T  =  NN )
4037, 39syl5eleqr 2497 . . . . . . 7  |-  ( ph  ->  1  e.  dom  T
)
41 ne0i 3744 . . . . . . 7  |-  ( 1  e.  dom  T  ->  dom  T  =/=  (/) )
4240, 41syl 17 . . . . . 6  |-  ( ph  ->  dom  T  =/=  (/) )
43 dm0rn0 5040 . . . . . . 7  |-  ( dom 
T  =  (/)  <->  ran  T  =  (/) )
4443necon3bii 2671 . . . . . 6  |-  ( dom 
T  =/=  (/)  <->  ran  T  =/=  (/) )
4542, 44sylib 196 . . . . 5  |-  ( ph  ->  ran  T  =/=  (/) )
4632ffvelrnda 6009 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  e.  ( 0 [,) +oo ) )
4735, 46sseldi 3440 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  e.  RR )
48 eqid 2402 . . . . . . . . . . . . 13  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
4948, 15ovolsf 22176 . . . . . . . . . . . 12  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) +oo ) )
5018, 49syl 17 . . . . . . . . . . 11  |-  ( ph  ->  S : NN --> ( 0 [,) +oo ) )
5150ffvelrnda 6009 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  e.  ( 0 [,) +oo ) )
5235, 51sseldi 3440 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  e.  RR )
5325adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
54 simpr 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  NN )
55 nnuz 11162 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
5654, 55syl6eleq 2500 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  ( ZZ>= `  1 )
)
57 simpl 455 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  ph )
58 elfznn 11768 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... j )  ->  n  e.  NN )
5930ovolfsf 22175 . . . . . . . . . . . . . . 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 6009 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  e.  ( 0 [,) +oo )
)
6235, 61sseldi 3440 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  e.  RR )
6357, 58, 62syl2an 475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  G
) `  n )  e.  RR )
6448ovolfsf 22175 . . . . . . . . . . . . . . . 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 6009 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  e.  ( 0 [,) +oo )
)
67 elrege0 11681 . . . . . . . . . . . . . 14  |-  ( ( ( ( abs  o.  -  )  o.  F
) `  n )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  F ) `  n
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  n
) ) )
6866, 67sylib 196 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  F
) `  n )  e.  RR  /\  0  <_ 
( ( ( abs 
o.  -  )  o.  F ) `  n
) ) )
6968simpld 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  e.  RR )
7057, 58, 69syl2an 475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  n )  e.  RR )
7128simprd 461 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
72 eqid 2402 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs  o.  -  )  o.  H )  =  ( ( abs  o.  -  )  o.  H )
7372ovolfsf 22175 . . . . . . . . . . . . . . . . . 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 6009 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  e.  ( 0 [,) +oo )
)
76 elrege0 11681 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( abs  o.  -  )  o.  H
) `  n )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  H ) `  n
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  H ) `  n
) ) )
7775, 76sylib 196 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  H
) `  n )  e.  RR  /\  0  <_ 
( ( ( abs 
o.  -  )  o.  H ) `  n
) ) )
7877simprd 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( ( abs 
o.  -  )  o.  H ) `  n
) )
7977simpld 457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  e.  RR )
8062, 79addge01d 10180 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 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 22262 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  G
) `  n )  +  ( ( ( abs  o.  -  )  o.  H ) `  n
) )  =  ( ( ( abs  o.  -  )  o.  F
) `  n )
)
8381, 82breqtrd 4419 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  <_  (
( ( abs  o.  -  )  o.  F
) `  n )
)
8457, 58, 83syl2an 475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  G
) `  n )  <_  ( ( ( abs 
o.  -  )  o.  F ) `  n
) )
8556, 63, 70, 84serle 12206 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  G
) ) `  j
)  <_  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  j
) )
8616fveq1i 5850 . . . . . . . . . 10  |-  ( T `
 j )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  j )
8715fveq1i 5850 . . . . . . . . . 10  |-  ( S `
 j )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  j )
8885, 86, 873brtr4g 4427 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  <_ 
( S `  j
) )
89 1zzd 10936 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  ZZ )
90 eqidd 2403 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  =  ( ( ( abs  o.  -  )  o.  F
) `  n )
)
9168simprd 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( ( abs 
o.  -  )  o.  F ) `  n
) )
92 frn 5720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( S : NN --> ( 0 [,) +oo )  ->  ran  S  C_  ( 0 [,) +oo ) )
9350, 92syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  S  C_  (
0 [,) +oo )
)
94 icossxr 11663 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 [,) +oo )  C_  RR*
9593, 94syl6ss 3454 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ran  S  C_  RR* )
9695adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ran  S  C_ 
RR* )
97 ffn 5714 . . . . . . . . . . . . . . . . . . . 20  |-  ( S : NN --> ( 0 [,) +oo )  ->  S  Fn  NN )
9850, 97syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  S  Fn  NN )
99 fnfvelrn 6006 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  Fn  NN  /\  k  e.  NN )  ->  ( S `  k
)  e.  ran  S
)
10098, 99sylan 469 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e. 
ran  S )
101 supxrub 11569 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  S  C_  RR*  /\  ( S `  k )  e.  ran  S )  -> 
( S `  k
)  <_  sup ( ran  S ,  RR* ,  <  ) )
10296, 100, 101syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  <_  sup ( ran  S ,  RR* ,  <  ) )
103102ralrimiva 2818 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. k  e.  NN  ( S `  k )  <_  sup ( ran  S ,  RR* ,  <  )
)
104 breq2 4399 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( ( S `
 k )  <_  x 
<->  ( S `  k
)  <_  sup ( ran  S ,  RR* ,  <  ) ) )
105104ralbidv 2843 . . . . . . . . . . . . . . . . 17  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( A. k  e.  NN  ( S `  k )  <_  x  <->  A. k  e.  NN  ( S `  k )  <_  sup ( ran  S ,  RR* ,  <  )
) )
106105rspcev 3160 . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E. x  e.  RR  A. k  e.  NN  ( S `  k )  <_  x )
10855, 15, 89, 90, 69, 91, 107isumsup2 13809 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  ~~>  sup ( ran  S ,  RR ,  <  )
)
10993, 35syl6ss 3454 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ran  S  C_  RR )
110 fdm 5718 . . . . . . . . . . . . . . . . . . 19  |-  ( S : NN --> ( 0 [,) +oo )  ->  dom  S  =  NN )
11150, 110syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  S  =  NN )
11237, 111syl5eleqr 2497 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  dom  S
)
113 ne0i 3744 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  dom  S  ->  dom  S  =/=  (/) )
114112, 113syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  S  =/=  (/) )
115 dm0rn0 5040 . . . . . . . . . . . . . . . . 17  |-  ( dom 
S  =  (/)  <->  ran  S  =  (/) )
116115necon3bii 2671 . . . . . . . . . . . . . . . 16  |-  ( dom 
S  =/=  (/)  <->  ran  S  =/=  (/) )
117114, 116sylib 196 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ran  S  =/=  (/) )
118 breq1 4398 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( S `  k )  ->  (
z  <_  x  <->  ( S `  k )  <_  x
) )
119118ralrn 6012 . . . . . . . . . . . . . . . . . 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 2918 . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E. x  e.  RR  A. z  e.  ran  S  z  <_  x )
123 supxrre 11572 . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . 14  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  =  sup ( ran  S ,  RR ,  <  )
)
125108, 124breqtrrd 4421 . . . . . . . . . . . . 13  |-  ( ph  ->  S  ~~>  sup ( ran  S ,  RR* ,  <  )
)
126125adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  S  ~~>  sup ( ran  S ,  RR* ,  <  ) )
12715, 126syl5eqbrr 4429 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  F )
)  ~~>  sup ( ran  S ,  RR* ,  <  )
)
12869adantlr 713 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  n )  e.  RR )
12991adantlr 713 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  NN )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  F ) `  n
) )
13055, 54, 127, 128, 129climserle 13634 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) )
13187, 130syl5eqbr 4428 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  <_  sup ( ran  S ,  RR* ,  <  ) )
13247, 52, 53, 88, 131letrd 9773 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  <_  sup ( ran  S ,  RR* ,  <  ) )
133132ralrimiva 2818 . . . . . . 7  |-  ( ph  ->  A. j  e.  NN  ( T `  j )  <_  sup ( ran  S ,  RR* ,  <  )
)
134 breq2 4399 . . . . . . . . 9  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( ( T `
 j )  <_  x 
<->  ( T `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) ) )
135134ralbidv 2843 . . . . . . . 8  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( A. j  e.  NN  ( T `  j )  <_  x  <->  A. j  e.  NN  ( T `  j )  <_  sup ( ran  S ,  RR* ,  <  )
) )
136135rspcev 3160 . . . . . . 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 659 . . . . . 6  |-  ( ph  ->  E. x  e.  RR  A. j  e.  NN  ( T `  j )  <_  x )
138 ffn 5714 . . . . . . . . 9  |-  ( T : NN --> ( 0 [,) +oo )  ->  T  Fn  NN )
13932, 138syl 17 . . . . . . . 8  |-  ( ph  ->  T  Fn  NN )
140 breq1 4398 . . . . . . . . 9  |-  ( z  =  ( T `  j )  ->  (
z  <_  x  <->  ( T `  j )  <_  x
) )
141140ralrn 6012 . . . . . . . 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 2918 . . . . . 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 232 . . . . 5  |-  ( ph  ->  E. x  e.  RR  A. z  e.  ran  T  z  <_  x )
145 suprcl 10543 . . . . 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 1230 . . . 4  |-  ( ph  ->  sup ( ran  T ,  RR ,  <  )  e.  RR )
14772, 17ovolsf 22176 . . . . . . . 8  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  U : NN --> ( 0 [,) +oo ) )
14871, 147syl 17 . . . . . . 7  |-  ( ph  ->  U : NN --> ( 0 [,) +oo ) )
149 frn 5720 . . . . . . 7  |-  ( U : NN --> ( 0 [,) +oo )  ->  ran  U  C_  ( 0 [,) +oo ) )
150148, 149syl 17 . . . . . 6  |-  ( ph  ->  ran  U  C_  (
0 [,) +oo )
)
151150, 35syl6ss 3454 . . . . 5  |-  ( ph  ->  ran  U  C_  RR )
152 fdm 5718 . . . . . . . . 9  |-  ( U : NN --> ( 0 [,) +oo )  ->  dom  U  =  NN )
153148, 152syl 17 . . . . . . . 8  |-  ( ph  ->  dom  U  =  NN )
15437, 153syl5eleqr 2497 . . . . . . 7  |-  ( ph  ->  1  e.  dom  U
)
155 ne0i 3744 . . . . . . 7  |-  ( 1  e.  dom  U  ->  dom  U  =/=  (/) )
156154, 155syl 17 . . . . . 6  |-  ( ph  ->  dom  U  =/=  (/) )
157 dm0rn0 5040 . . . . . . 7  |-  ( dom 
U  =  (/)  <->  ran  U  =  (/) )
158157necon3bii 2671 . . . . . 6  |-  ( dom 
U  =/=  (/)  <->  ran  U  =/=  (/) )
159156, 158sylib 196 . . . . 5  |-  ( ph  ->  ran  U  =/=  (/) )
160148ffvelrnda 6009 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  e.  ( 0 [,) +oo ) )
16135, 160sseldi 3440 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  e.  RR )
16257, 58, 79syl2an 475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  H
) `  n )  e.  RR )
163 elrege0 11681 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( abs  o.  -  )  o.  G
) `  n )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  G ) `  n
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  G ) `  n
) ) )
16461, 163sylib 196 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( ( abs  o.  -  )  o.  G
) `  n )  e.  RR  /\  0  <_ 
( ( ( abs 
o.  -  )  o.  G ) `  n
) ) )
165164simprd 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( ( abs 
o.  -  )  o.  G ) `  n
) )
16679, 62addge02d 10181 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  <_  (
( ( ( abs 
o.  -  )  o.  G ) `  n
)  +  ( ( ( abs  o.  -  )  o.  H ) `  n ) ) )
168167, 82breqtrd 4419 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  <_  (
( ( abs  o.  -  )  o.  F
) `  n )
)
16957, 58, 168syl2an 475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  H
) `  n )  <_  ( ( ( abs 
o.  -  )  o.  F ) `  n
) )
17056, 162, 70, 169serle 12206 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  j
)  <_  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  j
) )
17117fveq1i 5850 . . . . . . . . . 10  |-  ( U `
 j )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  j )
172170, 171, 873brtr4g 4427 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  <_ 
( S `  j
) )
173161, 52, 53, 172, 131letrd 9773 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  <_  sup ( ran  S ,  RR* ,  <  ) )
174173ralrimiva 2818 . . . . . . 7  |-  ( ph  ->  A. j  e.  NN  ( U `  j )  <_  sup ( ran  S ,  RR* ,  <  )
)
175 breq2 4399 . . . . . . . . 9  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( ( U `
 j )  <_  x 
<->  ( U `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) ) )
176175ralbidv 2843 . . . . . . . 8  |-  ( x  =  sup ( ran 
S ,  RR* ,  <  )  ->  ( A. j  e.  NN  ( U `  j )  <_  x  <->  A. j  e.  NN  ( U `  j )  <_  sup ( ran  S ,  RR* ,  <  )
) )
177176rspcev 3160 . . . . . . 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 659 . . . . . 6  |-  ( ph  ->  E. x  e.  RR  A. j  e.  NN  ( U `  j )  <_  x )
179 ffn 5714 . . . . . . . . 9  |-  ( U : NN --> ( 0 [,) +oo )  ->  U  Fn  NN )
180148, 179syl 17 . . . . . . . 8  |-  ( ph  ->  U  Fn  NN )
181 breq1 4398 . . . . . . . . 9  |-  ( z  =  ( U `  j )  ->  (
z  <_  x  <->  ( U `  j )  <_  x
) )
182181ralrn 6012 . . . . . . . 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 2918 . . . . . 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 232 . . . . 5  |-  ( ph  ->  E. x  e.  RR  A. z  e.  ran  U  z  <_  x )
186 suprcl 10543 . . . . 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 1230 . . . 4  |-  ( ph  ->  sup ( ran  U ,  RR ,  <  )  e.  RR )
188 ssralv 3503 . . . . . . . . . 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 4402 . . . . . . . . . . . . 13  |-  ( P  <  x  <->  ( 1st `  ( F `  n
) )  <  x
)
191 ovolfcl 22170 . . . . . . . . . . . . . . . . . . 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 469 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( 1st `  ( F `
 n ) )  e.  RR  /\  ( 2nd `  ( F `  n ) )  e.  RR  /\  ( 1st `  ( F `  n
) )  <_  ( 2nd `  ( F `  n ) ) ) )
193192simp1d 1009 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( F `  n
) )  e.  RR )
19421, 193syl5eqel 2494 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  P  e.  RR )
195194adantlr 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  P  e.  RR )
1961, 3syl5ss 3453 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E  i^i  B
)  C_  RR )
197196sselda 3442 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( E  i^i  B ) )  ->  x  e.  RR )
198197adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  x  e.  RR )
199 ltle 9704 . . . . . . . . . . . . . . 15  |-  ( ( P  e.  RR  /\  x  e.  RR )  ->  ( P  <  x  ->  P  <_  x )
)
200195, 198, 199syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( P  <  x  ->  P  <_  x ) )
201 simpr 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
202 opex 4655 . . . . . . . . . . . . . . . . . . . 20  |-  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) ,  Q >.  e. 
_V
20323fvmpt2 5941 . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( G `
 n )  = 
<. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) ,  Q >. )
205204fveq2d 5853 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( G `  n
) )  =  ( 1st `  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) ,  Q >. ) )
20613adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  A  e.  RR )
207206, 194ifcld 3928 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  if ( P  <_  A ,  A ,  P )  e.  RR )
208192simp2d 1010 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( F `  n
) )  e.  RR )
20922, 208syl5eqel 2494 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  Q  e.  RR )
210207, 209ifcld 3928 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
)  e.  RR )
211 op1stg 6796 . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( G `  n
) )  =  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) )
214213ad2ant2r 745 . . . . . . . . . . . . . . . 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 745 . . . . . . . . . . . . . . . . 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 745 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  if ( P  <_  A ,  A ,  P )  e.  RR )
217196ad2antrr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  ( E  i^i  B )  C_  RR )
218 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  x  e.  ( E  i^i  B ) )
219217, 218sseldd 3443 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  x  e.  RR )
220209ad2ant2r 745 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  Q  e.  RR )
221 min1 11442 . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  A  e.  RR )
224 inss2 3660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E  i^i  B )  C_  B
225224sseli 3438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( E  i^i  B )  ->  x  e.  B )
226225ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  x  e.  B
)
22713rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A  e.  RR* )
228 pnfxr 11374 . . . . . . . . . . . . . . . . . . . . . . . 24  |- +oo  e.  RR*
229 elioo2 11623 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\ +oo  e.  RR* )  ->  (
x  e.  ( A (,) +oo )  <->  ( x  e.  RR  /\  A  < 
x  /\  x  < +oo ) ) )
230227, 228, 229sylancl 660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( x  e.  ( A (,) +oo )  <->  ( x  e.  RR  /\  A  <  x  /\  x  < +oo ) ) )
23112eleq2i 2480 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  B  <->  x  e.  ( A (,) +oo )
)
232 ltpnf 11384 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  x  < +oo )
233232adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  A  <  x )  ->  x  < +oo )
234233pm4.71i 630 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  A  <  x )  <->  ( (
x  e.  RR  /\  A  <  x )  /\  x  < +oo ) )
235 df-3an 976 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  A  <  x  /\  x  < +oo )  <->  ( (
x  e.  RR  /\  A  <  x )  /\  x  < +oo ) )
236234, 235bitr4i 252 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  A  <  x )  <->  ( x  e.  RR  /\  A  < 
x  /\  x  < +oo ) )
237230, 231, 2363bitr4g 288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  B  <->  ( x  e.  RR  /\  A  <  x ) ) )
238 simpr 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  A  <  x )  ->  A  <  x )
239237, 238syl6bi 228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  B  ->  A  <  x ) )
240239ad2antrr 724 . . . . . . . . . . . . . . . . . . . 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 9765 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  A  <_  x
)
243 simprr 758 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  P  <_  x
)
244 breq1 4398 . . . . . . . . . . . . . . . . . . 19  |-  ( A  =  if ( P  <_  A ,  A ,  P )  ->  ( A  <_  x  <->  if ( P  <_  A ,  A ,  P )  <_  x
) )
245 breq1 4398 . . . . . . . . . . . . . . . . . . 19  |-  ( P  =  if ( P  <_  A ,  A ,  P )  ->  ( P  <_  x  <->  if ( P  <_  A ,  A ,  P )  <_  x
) )
246244, 245ifboth 3921 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  <_  x  /\  P  <_  x )  ->  if ( P  <_  A ,  A ,  P )  <_  x )
247242, 243, 246syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  if ( P  <_  A ,  A ,  P )  <_  x
)
248215, 216, 219, 222, 247letrd 9773 . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  (
n  e.  NN  /\  P  <_  x ) )  ->  ( 1st `  ( G `  n )
)  <_  x )
250249expr 613 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( P  <_  x  ->  ( 1st `  ( G `  n ) )  <_  x ) )
251200, 250syld 42 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( P  <  x  ->  ( 1st `  ( G `  n ) )  <_  x ) )
252190, 251syl5bir 218 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( F `  n )
)  <  x  ->  ( 1st `  ( G `
 n ) )  <_  x ) )
25322breq2i 4403 . . . . . . . . . . . . . 14  |-  ( x  <  Q  <->  x  <  ( 2nd `  ( F `
 n ) ) )
254209adantlr 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  Q  e.  RR )
255 ltle 9704 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR  /\  Q  e.  RR )  ->  ( x  <  Q  ->  x  <_  Q )
)
256198, 254, 255syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <  Q  ->  x  <_  Q ) )
257253, 256syl5bir 218 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <  ( 2nd `  ( F `  n
) )  ->  x  <_  Q ) )
258204fveq2d 5853 . . . . . . . . . . . . . . . 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 6797 . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  <. if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q ) ,  Q >. )  =  Q )
261258, 260eqtrd 2443 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( G `  n
) )  =  Q )
262261adantlr 713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  ( 2nd `  ( G `  n ) )  =  Q )
263262breq2d 4407 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <_  ( 2nd `  ( G `  n
) )  <->  x  <_  Q ) )
264257, 263sylibrd 234 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  i^i  B
) )  /\  n  e.  NN )  ->  (
x  <  ( 2nd `  ( F `  n
) )  ->  x  <_  ( 2nd `  ( G `  n )
) ) )
265252, 264anim12d 561 . . . . . . . . . . 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 2879 . . . . . . . . . 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 2812 . . . . . . . . 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 30 . . . . . . . 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 22171 . . . . . . . . 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 659 . . . . . . . 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 22172 . . . . . . . . 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 659 . . . . . . . 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 268 . . . . . . 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 22192 . . . . . 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 659 . . . . 5  |-  ( ph  ->  ( vol* `  ( E  i^i  B ) )  <_  sup ( ran  T ,  RR* ,  <  ) )
277 supxrre 11572 . . . . . 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 1230 . . . . 5  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  =  sup ( ran  T ,  RR ,  <  )
)
279276, 278breqtrd 4419 . . . 4  |-  ( ph  ->  ( vol* `  ( E  i^i  B ) )  <_  sup ( ran  T ,  RR ,  <  ) )
280 ssralv 3503 . . . . . . . . . 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 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  P  e.  RR )
2837, 3syl5ss 3453 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E  \  B
)  C_  RR )
284283sselda 3442 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( E  \  B ) )  ->  x  e.  RR )
285284adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  x  e.  RR )
286282, 285, 199syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  ( P  <  x  ->  P  <_  x ) )
287190, 286syl5bir 218 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( F `  n )
)  <  x  ->  P  <_  x ) )
288 opex 4655 . . . . . . . . . . . . . . . . . 18  |-  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >.  e.  _V
28924fvmpt2 5941 . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( H `
 n )  = 
<. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. )
291290fveq2d 5853 . . . . . . . . . . . . . . . 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 6796 . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  <. P ,  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) >. )  =  P )
294291, 293eqtrd 2443 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1st `  ( H `  n
) )  =  P )
295294adantlr 713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  ( 1st `  ( H `  n ) )  =  P )
296295breq1d 4405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( H `  n )
)  <_  x  <->  P  <_  x ) )
297287, 296sylibrd 234 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
( 1st `  ( F `  n )
)  <  x  ->  ( 1st `  ( H `
 n ) )  <_  x ) )
298209adantlr 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  Q  e.  RR )
299285, 298, 255syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <  Q  ->  x  <_  Q ) )
300283ad2antrr 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( E  \  B )  C_  RR )
301 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  e.  ( E  \  B ) )
302300, 301sseldd 3443 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  e.  RR )
30313ad2antrr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  A  e.  RR )
304194ad2ant2r 745 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  P  e.  RR )
305303, 304ifcld 3928 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  if ( P  <_  A ,  A ,  P )  e.  RR )
306 eldifn 3566 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( E  \  B )  ->  -.  x  e.  B )
307306ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  -.  x  e.  B )
308302biantrurd 506 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( A  < 
x  <->  ( x  e.  RR  /\  A  < 
x ) ) )
309237ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( x  e.  B  <->  ( x  e.  RR  /\  A  < 
x ) ) )
310308, 309bitr4d 256 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( A  < 
x  <->  x  e.  B
) )
311307, 310mtbird 299 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  -.  A  <  x )
312302, 303lenltd 9763 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  ( x  <_  A 
<->  -.  A  <  x
) )
313311, 312mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  A
)
314 max2 11441 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  RR  /\  A  e.  RR )  ->  A  <_  if ( P  <_  A ,  A ,  P ) )
315304, 303, 314syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  A  <_  if ( P  <_  A ,  A ,  P )
)
316302, 303, 305, 313, 315letrd 9773 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  if ( P  <_  A ,  A ,  P )
)
317 simprr 758 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  Q
)
318 breq2 4399 . . . . . . . . . . . . . . . . . 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 4399 . . . . . . . . . . . . . . . . . 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 3921 . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . 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 5853 . . . . . . . . . . . . . . . . . 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 6797 . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2nd `  ( H `  n
) )  =  if ( if ( P  <_  A ,  A ,  P )  <_  Q ,  if ( P  <_  A ,  A ,  P ) ,  Q
) )
326325ad2ant2r 745 . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  (
n  e.  NN  /\  x  <_  Q ) )  ->  x  <_  ( 2nd `  ( H `  n ) ) )
328327expr 613 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <_  Q  ->  x  <_  ( 2nd `  ( H `  n )
) ) )
329299, 328syld 42 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <  Q  ->  x  <_  ( 2nd `  ( H `  n )
) ) )
330253, 329syl5bir 218 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( E  \  B
) )  /\  n  e.  NN )  ->  (
x  <  ( 2nd `  ( F `  n
) )  ->  x  <_  ( 2nd `  ( H `  n )
) ) )
331297, 330anim12d 561 . . . . . . . . . . 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 2879 . . . . . . . . . 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 2812 . . . . . . . . 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 30 . . . . . . . 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 22172 . . . . . . . . 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 659 . . . . . . . 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 268 . . . . . . 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 22192 . . . . . 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 659 . . . . 5  |-  ( ph  ->  ( vol* `  ( E  \  B ) )  <_  sup ( ran  U ,  RR* ,  <  ) )
341 supxrre 11572 . . . . . 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 1230 . . . . 5  |-  ( ph  ->  sup ( ran  U ,  RR* ,  <  )  =  sup ( ran  U ,  RR ,  <  )
)
343340, 342breqtrd 4419 . . . 4  |-  ( ph  ->  ( vol* `  ( E  \  B ) )  <_  sup ( ran  U ,  RR ,  <  ) )
3446, 10, 146, 187, 279, 343le2addd 10210 . . 3  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  <_  ( sup ( ran  T ,  RR ,  <  )  +  sup ( ran  U ,  RR ,  <  ) ) )
345 eqidd 2403 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  =  ( ( ( abs  o.  -  )  o.  G
) `  n )
)
34655, 16, 89, 345, 62, 165, 137isumsup2 13809 . . . . 5  |-  ( ph  ->  T  ~~>  sup ( ran  T ,  RR ,  <  )
)
347 seqex 12153 . . . . . . 7  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  F )
)  e.  _V
34815, 347eqeltri 2486 . . . . . 6  |-  S  e. 
_V
349348a1i 11 . . . . 5  |-  ( ph  ->  S  e.  _V )
350 eqidd 2403 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  =  ( ( ( abs  o.  -  )  o.  H
) `  n )
)
35155, 17, 89, 350, 79, 78, 178isumsup2 13809 . . . . 5  |-  ( ph  ->  U  ~~>  sup ( ran  U ,  RR ,  <  )
)
35247recnd 9652 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( T `
 j )  e.  CC )
353161recnd 9652 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( U `
 j )  e.  CC )
35462recnd 9652 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  n )  e.  CC )
35557, 58, 354syl2an 475 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  G
) `  n )  e.  CC )
35679recnd 9652 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  n )  e.  CC )
35757, 58, 356syl2an 475 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  n  e.  ( 1 ... j
) )  ->  (
( ( abs  o.  -  )  o.  H
) `  n )  e.  CC )
35882eqcomd 2410 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  n )  =  ( ( ( ( abs 
o.  -  )  o.  G ) `  n
)  +  ( ( ( abs  o.  -  )  o.  H ) `  n ) ) )
35957, 58, 358syl2an 475 . . . . . . 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 12193 . . . . . 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 6290 . . . . . 6  |-  ( ( T `  j )  +  ( U `  j ) )  =  ( (  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  G )
) `  j )  +  (  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  H )
) `  j )
)
362360, 87, 3613eqtr4g 2468 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( S `
 j )  =  ( ( T `  j )  +  ( U `  j ) ) )
36355, 89, 346, 349, 351, 352, 353, 362climadd 13603 . . . 4  |-  ( ph  ->  S  ~~>  ( sup ( ran  T ,  RR ,  <  )  +  sup ( ran  U ,  RR ,  <  ) ) )
364 climuni 13524 . . . 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 659 . . 3  |-  ( ph  ->  ( sup ( ran 
T ,  RR ,  <  )  +  sup ( ran  U ,  RR ,  <  ) )  =  sup ( ran  S ,  RR* ,  <  ) )
366344, 365breqtrd 4419 . 2  |-  ( ph  ->  ( ( vol* `  ( E  i^i  B
) )  +  ( vol* `  ( E  \  B ) ) )  <_  sup ( ran  S ,  RR* ,  <  ) )
36711, 25, 27, 366, 20letrd 9773 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 184    /\ wa 367    /\ w3a 974    = wceq 1405    e. wcel 1842    =/= wne 2598   A.wral 2754   E.wrex 2755   _Vcvv 3059    \ cdif 3411    i^i cin 3413    C_ wss 3414   (/)c0 3738   ifcif 3885   <.cop 3978   U.cuni 4191   class class class wbr 4395    |-> cmpt 4453    X. cxp 4821   dom cdm 4823   ran crn 4824    o. ccom 4827    Fn wfn 5564   -->wf 5565   ` cfv 5569  (class class class)co 6278   1stc1st 6782   2ndc2nd 6783   supcsup 7934   CCcc 9520   RRcr 9521   0cc0 9522   1c1 9523    + caddc 9525   +oocpnf 9655   RR*cxr 9657    < clt 9658    <_ cle 9659    - cmin 9841   NNcn 10576   ZZ>=cuz 11127   RR+crp 11265   (,)cioo 11582   [,)cico 11584   [,]cicc 11585   ...cfz 11726    seqcseq 12151   abscabs 13216    ~~> cli 13456   vol*covol 22166
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-inf2 8091  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599  ax-pre-sup 9600
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-1st 6784  df-2nd 6785  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-oadd 7171  df-er 7348  df-map 7459  df-pm 7460  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-sup 7935  df-oi 7969  df-card 8352  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-div 10248  df-nn 10577  df-2 10635  df-3 10636  df-n0 10837  df-z 10906  df-uz 11128  df-q 11228  df-rp 11266  df-ioo 11586  df-ico 11588  df-icc 11589  df-fz 11727  df-fzo 11855  df-fl 11966  df-seq 12152  df-exp 12211  df-hash 12453  df-cj 13081  df-re 13082  df-im 13083  df-sqrt 13217  df-abs 13218  df-clim 13460  df-rlim 13461  df-sum 13658  df-ovol 22168
This theorem is referenced by:  ioombl1  22264
  Copyright terms: Public domain W3C validator