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

Theorem itg2monolem1 19105
Description: Lemma for itg2mono 19108. We show that for any constant  t less than one,  t  x.  S.1 H is less than  S, and so  S.1 H  <_  S, which is one half of the equality in itg2mono 19108. Consider the sequence  A ( n )  =  { x  |  t  x.  H  <_  F ( n ) }. This is an increasing sequence of measurable sets whose union is  RR, and so  H  |`  A ( n ) has an integral which equals  S.1 H in the limit, by itg1climres 19069. Then by taking the limit in  ( t  x.  H )  |`  A ( n )  <_  F
( n ), we get  t  x.  S.1 H  <_  S as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
itg2mono.1  |-  G  =  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  ) )
itg2mono.2  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e. MblFn
)
itg2mono.3  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n ) : RR --> ( 0 [,) 
+oo ) )
itg2mono.4  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  o R  <_  ( F `  ( n  +  1 ) ) )
itg2mono.5  |-  ( (
ph  /\  x  e.  RR )  ->  E. y  e.  RR  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
)
itg2mono.6  |-  S  =  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) ,  RR* ,  <  )
itg2mono.7  |-  ( ph  ->  T  e.  ( 0 (,) 1 ) )
itg2mono.8  |-  ( ph  ->  H  e.  dom  S.1 )
itg2mono.9  |-  ( ph  ->  H  o R  <_  G )
itg2mono.10  |-  ( ph  ->  S  e.  RR )
itg2mono.11  |-  A  =  ( n  e.  NN  |->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  n ) `  x ) } )
Assertion
Ref Expression
itg2monolem1  |-  ( ph  ->  ( T  x.  ( S.1 `  H ) )  <_  S )
Distinct variable groups:    x, A    x, n, y, G    n, H, x, y    n, F, x, y    ph, n, x, y    S, n, x, y    T, n, x, y
Allowed substitution hints:    A( y, n)

Proof of Theorem itg2monolem1
Dummy variables  j 
k  m  z  w are mutually distinct and distinct from all other variables.
<
StepHypRef Expression
1 nnuz 10263 . 2  |-  NN  =  ( ZZ>= `  1 )
2 1z 10053 . . 3  |-  1  e.  ZZ
32a1i 10 . 2  |-  ( ph  ->  1  e.  ZZ )
4 readdcl 8820 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  +  y )  e.  RR )
54adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
x  e.  RR  /\  y  e.  RR )
)  ->  ( x  +  y )  e.  RR )
6 itg2mono.3 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n ) : RR --> ( 0 [,) 
+oo ) )
7 0re 8838 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
8 pnfxr 10455 . . . . . . . . . . . . . . . . 17  |-  +oo  e.  RR*
9 icossre 10730 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
107, 8, 9mp2an 653 . . . . . . . . . . . . . . . 16  |-  ( 0 [,)  +oo )  C_  RR
11 fss 5397 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  n
) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F `
 n ) : RR --> RR )
126, 10, 11sylancl 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n ) : RR --> RR )
13 itg2mono.8 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  e.  dom  S.1 )
14 itg2mono.7 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  e.  ( 0 (,) 1 ) )
15 0xr 8878 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR*
16 1re 8837 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR
17 rexr 8877 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  e.  RR  ->  1  e.  RR* )
1816, 17ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR*
19 elioo2 10697 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  RR*  /\  1  e.  RR* )  ->  ( T  e.  ( 0 (,) 1 )  <->  ( T  e.  RR  /\  0  < 
T  /\  T  <  1 ) ) )
2015, 18, 19mp2an 653 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T  e.  ( 0 (,) 1 )  <->  ( T  e.  RR  /\  0  < 
T  /\  T  <  1 ) )
2114, 20sylib 188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( T  e.  RR  /\  0  <  T  /\  T  <  1 ) )
2221simp1d 967 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  e.  RR )
2322renegcld 9210 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
-u T  e.  RR )
2413, 23i1fmulc 19058 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( RR  X.  { -u T } )  o F  x.  H
)  e.  dom  S.1 )
2524adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  e. 
dom  S.1 )
26 i1ff 19031 . . . . . . . . . . . . . . . 16  |-  ( ( ( RR  X.  { -u T } )  o F  x.  H )  e.  dom  S.1  ->  ( ( RR  X.  { -u T } )  o F  x.  H ) : RR --> RR )
2725, 26syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H ) : RR --> RR )
28 reex 8828 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
2928a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  RR  e.  _V )
30 inidm 3378 . . . . . . . . . . . . . . 15  |-  ( RR 
i^i  RR )  =  RR
315, 12, 27, 29, 29, 30off 6093 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) : RR --> RR )
3231adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) : RR --> RR )
33 ffn 5389 . . . . . . . . . . . . 13  |-  ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) : RR --> RR  ->  ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )  Fn  RR )
3432, 33syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) )  Fn  RR )
35 elpreima 5645 . . . . . . . . . . . 12  |-  ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) )  Fn  RR  ->  ( x  e.  ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  <->  ( x  e.  RR  /\  ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  (  -oo (,) 0 ) ) ) )
3634, 35syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  e.  ( `' ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  <->  ( x  e.  RR  /\  ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  (  -oo (,) 0 ) ) ) )
37 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  x  e.  RR )
3837biantrurd 494 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  (  -oo (,) 0
)  <->  ( x  e.  RR  /\  ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  (  -oo (,) 0 ) ) ) )
3936, 38bitr4d 247 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  e.  ( `' ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  <->  ( (
( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  (  -oo (,) 0 ) ) )
40 ffvelrn 5663 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) : RR --> RR  /\  x  e.  RR )  ->  ( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  RR )
4131, 40sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  RR )
4241biantrurd 494 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  <  0  <->  ( ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  RR  /\  ( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  <  0 ) ) )
43 elioomnf 10738 . . . . . . . . . . . 12  |-  ( 0  e.  RR*  ->  ( ( ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  (  -oo (,) 0
)  <->  ( ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  RR  /\  ( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  <  0 ) ) )
4415, 43ax-mp 8 . . . . . . . . . . 11  |-  ( ( ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  (  -oo (,) 0
)  <->  ( ( ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) `  x
)  e.  RR  /\  ( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  <  0 ) )
4542, 44syl6rbbr 255 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  (  -oo (,) 0
)  <->  ( ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `  x )  <  0 ) )
46 ffn 5389 . . . . . . . . . . . . . . 15  |-  ( ( F `  n ) : RR --> RR  ->  ( F `  n )  Fn  RR )
4712, 46syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  Fn  RR )
48 ffn 5389 . . . . . . . . . . . . . . 15  |-  ( ( ( RR  X.  { -u T } )  o F  x.  H ) : RR --> RR  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  Fn  RR )
4927, 48syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  Fn  RR )
50 eqidd 2284 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
) `  x )  =  ( ( F `
 n ) `  x ) )
5123adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  -u T  e.  RR )
52 i1ff 19031 . . . . . . . . . . . . . . . . . . 19  |-  ( H  e.  dom  S.1  ->  H : RR --> RR )
5313, 52syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H : RR --> RR )
54 ffn 5389 . . . . . . . . . . . . . . . . . 18  |-  ( H : RR --> RR  ->  H  Fn  RR )
5553, 54syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  H  Fn  RR )
5655adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  H  Fn  RR )
57 eqidd 2284 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  =  ( H `  x ) )
5829, 51, 56, 57ofc1 6100 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( RR  X.  { -u T } )  o F  x.  H
) `  x )  =  ( -u T  x.  ( H `  x
) ) )
5922recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  CC )
6059ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  T  e.  CC )
61 ffvelrn 5663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( H : RR --> RR  /\  x  e.  RR )  ->  ( H `  x
)  e.  RR )
6253, 61sylan 457 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( H `
 x )  e.  RR )
6362adantlr 695 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  e.  RR )
6463recnd 8861 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  e.  CC )
6560, 64mulneg1d 9232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( -u T  x.  ( H `
 x ) )  =  -u ( T  x.  ( H `  x ) ) )
6658, 65eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( RR  X.  { -u T } )  o F  x.  H
) `  x )  =  -u ( T  x.  ( H `  x ) ) )
6747, 49, 29, 29, 30, 50, 66ofval 6087 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) `
 x )  =  ( ( ( F `
 n ) `  x )  +  -u ( T  x.  ( H `  x )
) ) )
68 ffvelrn 5663 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  n
) : RR --> RR  /\  x  e.  RR )  ->  ( ( F `  n ) `  x
)  e.  RR )
6912, 68sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
) `  x )  e.  RR )
7069recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
) `  x )  e.  CC )
7122adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
7271, 62remulcld 8863 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  RR )
7372adantlr 695 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  RR )
7473recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  CC )
7570, 74negsubd 9163 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n ) `  x
)  +  -u ( T  x.  ( H `  x ) ) )  =  ( ( ( F `  n ) `
 x )  -  ( T  x.  ( H `  x )
) ) )
7667, 75eqtrd 2315 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) `
 x )  =  ( ( ( F `
 n ) `  x )  -  ( T  x.  ( H `  x ) ) ) )
7776breq1d 4033 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  <  0  <->  ( ( ( F `  n ) `
 x )  -  ( T  x.  ( H `  x )
) )  <  0
) )
787a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  0  e.  RR )
7969, 73, 78ltsubaddd 9368 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n ) `  x )  -  ( T  x.  ( H `  x ) ) )  <  0  <->  ( ( F `  n ) `  x )  <  (
0  +  ( T  x.  ( H `  x ) ) ) ) )
8074addid2d 9013 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
0  +  ( T  x.  ( H `  x ) ) )  =  ( T  x.  ( H `  x ) ) )
8180breq2d 4035 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n ) `  x
)  <  ( 0  +  ( T  x.  ( H `  x ) ) )  <->  ( ( F `  n ) `  x )  <  ( T  x.  ( H `  x ) ) ) )
8277, 79, 813bitrd 270 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) `
 x )  <  0  <->  ( ( F `
 n ) `  x )  <  ( T  x.  ( H `  x ) ) ) )
8339, 45, 823bitrd 270 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  e.  ( `' ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  <->  ( ( F `  n ) `  x )  <  ( T  x.  ( H `  x ) ) ) )
8483notbid 285 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( -.  x  e.  ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  <->  -.  (
( F `  n
) `  x )  <  ( T  x.  ( H `  x )
) ) )
85 eldif 3162 . . . . . . . . . 10  |-  ( x  e.  ( RR  \ 
( `' ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) " (  -oo (,) 0 ) ) )  <-> 
( x  e.  RR  /\ 
-.  x  e.  ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) ) ) )
8685baib 871 . . . . . . . . 9  |-  ( x  e.  RR  ->  (
x  e.  ( RR 
\  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) ) )  <->  -.  x  e.  ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) ) ) )
8786adantl 452 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  e.  ( RR 
\  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) ) )  <->  -.  x  e.  ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) ) ) )
8873, 69lenltd 8965 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  n ) `  x )  <->  -.  (
( F `  n
) `  x )  <  ( T  x.  ( H `  x )
) ) )
8984, 87, 883bitr4d 276 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  e.  ( RR 
\  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) ) )  <->  ( T  x.  ( H `  x ) )  <_  ( ( F `  n ) `  x ) ) )
9089rabbi2dva 3377 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( RR 
i^i  ( RR  \ 
( `' ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) " (  -oo (,) 0 ) ) ) )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  n ) `  x
) } )
91 rembl 18898 . . . . . . 7  |-  RR  e.  dom  vol
92 itg2mono.2 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e. MblFn
)
93 i1fmbf 19030 . . . . . . . . . . 11  |-  ( ( ( RR  X.  { -u T } )  o F  x.  H )  e.  dom  S.1  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  e. MblFn )
9425, 93syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  e. MblFn
)
9592, 94mbfadd 19016 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )  e. MblFn )
96 mbfima 18987 . . . . . . . . 9  |-  ( ( ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) )  e. MblFn  /\  ( ( F `  n )  o F  +  (
( RR  X.  { -u T } )  o F  x.  H ) ) : RR --> RR )  ->  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) )  e.  dom  vol )
9795, 31, 96syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( `' ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  e. 
dom  vol )
98 cmmbl 18892 . . . . . . . 8  |-  ( ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  e. 
dom  vol  ->  ( RR  \  ( `' ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) " (  -oo (,) 0 ) ) )  e.  dom  vol )
9997, 98syl 15 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( RR 
\  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) ) )  e.  dom  vol )
100 inmbl 18899 . . . . . . 7  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  ( `' ( ( F `
 n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) ) )  e.  dom  vol )  ->  ( RR  i^i  ( RR  \  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) ) ) )  e.  dom  vol )
10191, 99, 100sylancr 644 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( RR 
i^i  ( RR  \ 
( `' ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) " (  -oo (,) 0 ) ) ) )  e.  dom  vol )
10290, 101eqeltrrd 2358 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  n ) `  x
) }  e.  dom  vol )
103 itg2mono.11 . . . . 5  |-  A  =  ( n  e.  NN  |->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  n ) `  x ) } )
104102, 103fmptd 5684 . . . 4  |-  ( ph  ->  A : NN --> dom  vol )
105 itg2mono.4 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  o R  <_  ( F `  ( n  +  1 ) ) )
106105ralrimiva 2626 . . . . . . . . . . 11  |-  ( ph  ->  A. n  e.  NN  ( F `  n )  o R  <_  ( F `  ( n  +  1 ) ) )
107 fveq2 5525 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  ( F `  n )  =  ( F `  j ) )
108 oveq1 5865 . . . . . . . . . . . . . 14  |-  ( n  =  j  ->  (
n  +  1 )  =  ( j  +  1 ) )
109108fveq2d 5529 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  ( F `  ( n  +  1 ) )  =  ( F `  ( j  +  1 ) ) )
110107, 109breq12d 4036 . . . . . . . . . . . 12  |-  ( n  =  j  ->  (
( F `  n
)  o R  <_ 
( F `  (
n  +  1 ) )  <->  ( F `  j )  o R  <_  ( F `  ( j  +  1 ) ) ) )
111110cbvralv 2764 . . . . . . . . . . 11  |-  ( A. n  e.  NN  ( F `  n )  o R  <_  ( F `
 ( n  + 
1 ) )  <->  A. j  e.  NN  ( F `  j )  o R  <_  ( F `  ( j  +  1 ) ) )
112106, 111sylib 188 . . . . . . . . . 10  |-  ( ph  ->  A. j  e.  NN  ( F `  j )  o R  <_  ( F `  ( j  +  1 ) ) )
113112r19.21bi 2641 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j )  o R  <_  ( F `  ( j  +  1 ) ) )
1146ralrimiva 2626 . . . . . . . . . . . . 13  |-  ( ph  ->  A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,)  +oo ) )
115107feq1d 5379 . . . . . . . . . . . . . 14  |-  ( n  =  j  ->  (
( F `  n
) : RR --> ( 0 [,)  +oo )  <->  ( F `  j ) : RR --> ( 0 [,)  +oo ) ) )
116115cbvralv 2764 . . . . . . . . . . . . 13  |-  ( A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,) 
+oo )  <->  A. j  e.  NN  ( F `  j ) : RR --> ( 0 [,)  +oo ) )
117114, 116sylib 188 . . . . . . . . . . . 12  |-  ( ph  ->  A. j  e.  NN  ( F `  j ) : RR --> ( 0 [,)  +oo ) )
118117r19.21bi 2641 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j ) : RR --> ( 0 [,) 
+oo ) )
119 ffn 5389 . . . . . . . . . . 11  |-  ( ( F `  j ) : RR --> ( 0 [,)  +oo )  ->  ( F `  j )  Fn  RR )
120118, 119syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j )  Fn  RR )
121 peano2nn 9758 . . . . . . . . . . . 12  |-  ( j  e.  NN  ->  (
j  +  1 )  e.  NN )
122 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( n  =  ( j  +  1 )  ->  ( F `  n )  =  ( F `  ( j  +  1 ) ) )
123122feq1d 5379 . . . . . . . . . . . . 13  |-  ( n  =  ( j  +  1 )  ->  (
( F `  n
) : RR --> ( 0 [,)  +oo )  <->  ( F `  ( j  +  1 ) ) : RR --> ( 0 [,)  +oo ) ) )
124123rspccva 2883 . . . . . . . . . . . 12  |-  ( ( A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,)  +oo )  /\  (
j  +  1 )  e.  NN )  -> 
( F `  (
j  +  1 ) ) : RR --> ( 0 [,)  +oo ) )
125114, 121, 124syl2an 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 ( j  +  1 ) ) : RR --> ( 0 [,) 
+oo ) )
126 ffn 5389 . . . . . . . . . . 11  |-  ( ( F `  ( j  +  1 ) ) : RR --> ( 0 [,)  +oo )  ->  ( F `  ( j  +  1 ) )  Fn  RR )
127125, 126syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 ( j  +  1 ) )  Fn  RR )
12828a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  RR  e.  _V )
129 eqidd 2284 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  =  ( ( F `
 j ) `  x ) )
130 eqidd 2284 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  (
j  +  1 ) ) `  x )  =  ( ( F `
 ( j  +  1 ) ) `  x ) )
131120, 127, 128, 128, 30, 129, 130ofrfval 6086 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( F `  j )  o R  <_  ( F `  ( j  +  1 ) )  <->  A. x  e.  RR  ( ( F `  j ) `  x
)  <_  ( ( F `  ( j  +  1 ) ) `
 x ) ) )
132113, 131mpbid 201 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  A. x  e.  RR  ( ( F `
 j ) `  x )  <_  (
( F `  (
j  +  1 ) ) `  x ) )
133132r19.21bi 2641 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  <_  ( ( F `  ( j  +  1 ) ) `  x
) )
13422ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  T  e.  RR )
13553adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  H : RR
--> RR )
136135, 61sylan 457 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  e.  RR )
137134, 136remulcld 8863 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  RR )
138 fss 5397 . . . . . . . . . 10  |-  ( ( ( F `  j
) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F `
 j ) : RR --> RR )
139118, 10, 138sylancl 643 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j ) : RR --> RR )
140 ffvelrn 5663 . . . . . . . . 9  |-  ( ( ( F `  j
) : RR --> RR  /\  x  e.  RR )  ->  ( ( F `  j ) `  x
)  e.  RR )
141139, 140sylan 457 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  e.  RR )
142 fss 5397 . . . . . . . . . 10  |-  ( ( ( F `  (
j  +  1 ) ) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F `
 ( j  +  1 ) ) : RR --> RR )
143125, 10, 142sylancl 643 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 ( j  +  1 ) ) : RR --> RR )
144 ffvelrn 5663 . . . . . . . . 9  |-  ( ( ( F `  (
j  +  1 ) ) : RR --> RR  /\  x  e.  RR )  ->  ( ( F `  ( j  +  1 ) ) `  x
)  e.  RR )
145143, 144sylan 457 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  (
j  +  1 ) ) `  x )  e.  RR )
146 letr 8914 . . . . . . . 8  |-  ( ( ( T  x.  ( H `  x )
)  e.  RR  /\  ( ( F `  j ) `  x
)  e.  RR  /\  ( ( F `  ( j  +  1 ) ) `  x
)  e.  RR )  ->  ( ( ( T  x.  ( H `
 x ) )  <_  ( ( F `
 j ) `  x )  /\  (
( F `  j
) `  x )  <_  ( ( F `  ( j  +  1 ) ) `  x
) )  ->  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) ) )
147137, 141, 145, 146syl3anc 1182 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x )  /\  (
( F `  j
) `  x )  <_  ( ( F `  ( j  +  1 ) ) `  x
) )  ->  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) ) )
148133, 147mpan2d 655 . . . . . 6  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x )  ->  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) ) )
149148ss2rabdv 3254 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) }  C_  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) } )
150107fveq1d 5527 . . . . . . . . 9  |-  ( n  =  j  ->  (
( F `  n
) `  x )  =  ( ( F `
 j ) `  x ) )
151150breq2d 4035 . . . . . . . 8  |-  ( n  =  j  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  n ) `  x )  <->  ( T  x.  ( H `  x
) )  <_  (
( F `  j
) `  x )
) )
152151rabbidv 2780 . . . . . . 7  |-  ( n  =  j  ->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  n ) `  x
) }  =  {
x  e.  RR  | 
( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) } )
15328rabex 4165 . . . . . . 7  |-  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) }  e.  _V
154152, 103, 153fvmpt 5602 . . . . . 6  |-  ( j  e.  NN  ->  ( A `  j )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) } )
155154adantl 452 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 j )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) } )
156121adantl 452 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( j  +  1 )  e.  NN )
157122fveq1d 5527 . . . . . . . . 9  |-  ( n  =  ( j  +  1 )  ->  (
( F `  n
) `  x )  =  ( ( F `
 ( j  +  1 ) ) `  x ) )
158157breq2d 4035 . . . . . . . 8  |-  ( n  =  ( j  +  1 )  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  n ) `  x )  <->  ( T  x.  ( H `  x
) )  <_  (
( F `  (
j  +  1 ) ) `  x ) ) )
159158rabbidv 2780 . . . . . . 7  |-  ( n  =  ( j  +  1 )  ->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  n ) `  x
) }  =  {
x  e.  RR  | 
( T  x.  ( H `  x )
)  <_  ( ( F `  ( j  +  1 ) ) `
 x ) } )
16028rabex 4165 . . . . . . 7  |-  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) }  e.  _V
161159, 103, 160fvmpt 5602 . . . . . 6  |-  ( ( j  +  1 )  e.  NN  ->  ( A `  ( j  +  1 ) )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) } )
162156, 161syl 15 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 ( j  +  1 ) )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  ( j  +  1 ) ) `
 x ) } )
163149, 155, 1623sstr4d 3221 . . . 4  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 j )  C_  ( A `  ( j  +  1 ) ) )
16472adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  e.  RR )
16562adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( H `  x
)  e.  RR )
16669an32s 779 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  (
( F `  n
) `  x )  e.  RR )
167 eqid 2283 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) )
168166, 167fmptd 5684 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) : NN --> RR )
169 frn 5395 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) : NN --> RR  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  C_  RR )
170168, 169syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  C_  RR )
171 1nn 9757 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  NN
172 fdm 5393 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) : NN --> RR  ->  dom  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  NN )
173168, 172syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  dom  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =  NN )
174171, 173syl5eleqr 2370 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  1  e. 
dom  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) )
175 ne0i 3461 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  dom  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  ->  dom  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) )  =/=  (/) )
176174, 175syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  dom  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =/=  (/) )
177 dm0rn0 4895 . . . . . . . . . . . . . . . . . 18  |-  ( dom  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  (/)  <->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  (/) )
178177necon3bii 2478 . . . . . . . . . . . . . . . . 17  |-  ( dom  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =/=  (/)  <->  ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  =/=  (/) )
179176, 178sylib 188 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =/=  (/) )
180 itg2mono.5 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  E. y  e.  RR  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
)
181 ffn 5389 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) : NN --> RR  ->  ( n  e.  NN  |->  ( ( F `  n
) `  x )
)  Fn  NN )
182168, 181syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  Fn  NN )
183 breq1 4026 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  ( ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) `
 m )  -> 
( z  <_  y  <->  ( ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  <_  y )
)
184183ralrn 5668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
)  Fn  NN  ->  ( A. z  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) z  <_ 
y  <->  A. m  e.  NN  ( ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) `  m )  <_  y
) )
185182, 184syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( A. z  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) z  <_  y  <->  A. m  e.  NN  ( ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) `
 m )  <_ 
y ) )
186 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( F `  n )  =  ( F `  m ) )
187186fveq1d 5527 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( F `  n
) `  x )  =  ( ( F `
 m ) `  x ) )
188 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  m ) `
 x )  e. 
_V
189187, 167, 188fvmpt 5602 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN  ->  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  =  ( ( F `  m ) `
 x ) )
190189breq1d 4033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN  ->  (
( ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) `  m )  <_  y  <->  ( ( F `  m
) `  x )  <_  y ) )
191190ralbiia 2575 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. m  e.  NN  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  <_  y  <->  A. m  e.  NN  ( ( F `
 m ) `  x )  <_  y
)
192187breq1d 4033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
( ( F `  n ) `  x
)  <_  y  <->  ( ( F `  m ) `  x )  <_  y
) )
193192cbvralv 2764 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. n  e.  NN  (
( F `  n
) `  x )  <_  y  <->  A. m  e.  NN  ( ( F `  m ) `  x
)  <_  y )
194191, 193bitr4i 243 . . . . . . . . . . . . . . . . . . 19  |-  ( A. m  e.  NN  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  <_  y  <->  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
)
195185, 194syl6bb 252 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( A. z  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) z  <_  y  <->  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
) )
196195rexbidv 2564 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( E. y  e.  RR  A. z  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) z  <_  y  <->  E. y  e.  RR  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
) )
197180, 196mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  E. y  e.  RR  A. z  e. 
ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) z  <_  y )
198 suprcl 9714 . . . . . . . . . . . . . . . 16  |-  ( ( ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) )  C_  RR  /\  ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  =/=  (/)  /\  E. y  e.  RR  A. z  e. 
ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) z  <_  y )  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  )  e.  RR )
199170, 179, 197, 198syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  )  e.  RR )
200199adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  )  e.  RR )
20121simp3d 969 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  <  1 )
202201adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  T  <  1 )
20322adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  T  e.  RR )
20416a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
1  e.  RR )
205 simprr 733 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
0  <  ( H `  x ) )
206 ltmul1 9606 . . . . . . . . . . . . . . . . 17  |-  ( ( T  e.  RR  /\  1  e.  RR  /\  (
( H `  x
)  e.  RR  /\  0  <  ( H `  x ) ) )  ->  ( T  <  1  <->  ( T  x.  ( H `  x ) )  <  ( 1  x.  ( H `  x ) ) ) )
207203, 204, 165, 205, 206syl112anc 1186 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  <  1  <->  ( T  x.  ( H `
 x ) )  <  ( 1  x.  ( H `  x
) ) ) )
208202, 207mpbid 201 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  <  ( 1  x.  ( H `  x ) ) )
209165recnd 8861 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( H `  x
)  e.  CC )
210209mulid2d 8853 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( 1  x.  ( H `  x )
)  =  ( H `
 x ) )
211208, 210breqtrd 4047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  <  ( H `  x ) )
212 itg2mono.9 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  o R  <_  G )
213 itg2mono.1 . . . . . . . . . . . . . . . . . . . . 21  |-  G  =  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  ) )
214199, 213fmptd 5684 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  G : RR --> RR )
215 ffn 5389 . . . . . . . . . . . . . . . . . . . 20  |-  ( G : RR --> RR  ->  G  Fn  RR )
216214, 215syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  G  Fn  RR )
21728a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  e.  _V )
218 eqidd 2284 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  RR )  ->  ( H `
 y )  =  ( H `  y
) )
219 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
( F `  n
) `  x )  =  ( ( F `
 n ) `  y ) )
220219mpteq2dv 4107 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =  ( n  e.  NN  |->  ( ( F `  n ) `
 y ) ) )
221220rneqd 4906 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  ran  ( n  e.  NN  |->  ( ( F `  n ) `  y
) ) )
222221supeq1d 7199 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) ,  RR ,  <  )  =  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
223 ltso 8903 . . . . . . . . . . . . . . . . . . . . . 22  |-  <  Or  RR
224223supex 7214 . . . . . . . . . . . . . . . . . . . . 21  |-  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  y
) ) ,  RR ,  <  )  e.  _V
225222, 213, 224fvmpt 5602 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR  ->  ( G `  y )  =  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
226225adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  RR )  ->  ( G `
 y )  =  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
22755, 216, 217, 217, 30, 218, 226ofrfval 6086 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( H  o R  <_  G  <->  A. y  e.  RR  ( H `  y )  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `
 n ) `  y ) ) ,  RR ,  <  )
) )
228212, 227mpbid 201 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. y  e.  RR  ( H `  y )  <_  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
229 fveq2 5525 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
230229, 222breq12d 4036 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( H `  x
)  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  )  <->  ( H `  y )  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `
 n ) `  y ) ) ,  RR ,  <  )
) )
231230cbvralv 2764 . . . . . . . . . . . . . . . . 17  |-  ( A. x  e.  RR  ( H `  x )  <_  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
) ,  RR ,  <  )  <->  A. y  e.  RR  ( H `  y )  <_  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
232228, 231sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. x  e.  RR  ( H `  x )  <_  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
) ,  RR ,  <  ) )
233232r19.21bi 2641 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( H `
 x )  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  ) )
234233adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( H `  x
)  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  ) )
235164, 165, 200, 211, 234ltletrd 8976 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  <  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  ) )
236170adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  C_  RR )
237179adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =/=  (/) )
238197adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. y  e.  RR  A. z  e.  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
) z  <_  y
)
239 suprlub 9716 . . . . . . . . . . . . . 14  |-  ( ( ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) 
C_  RR  /\  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =/=  (/)  /\  E. y  e.  RR  A. z  e.  ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) z  <_  y )  /\  ( T  x.  ( H `  x )
)  e.  RR )  ->  ( ( T  x.  ( H `  x ) )  <  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  )  <->  E. w  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ( T  x.  ( H `  x ) )  < 
w ) )
240236, 237, 238, 164, 239syl31anc 1185 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( ( T  x.  ( H `  x ) )  <  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  )  <->  E. w  e.  ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) ( T  x.  ( H `
 x ) )  <  w ) )
241235, 240mpbid 201 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. w  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ( T  x.  ( H `  x ) )  < 
w )
242182adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( n  e.  NN  |->  ( ( F `  n ) `  x
) )  Fn  NN )
243 breq2 4027 . . . . . . . . . . . . . . 15  |-  ( w  =  ( ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) `
 j )  -> 
( ( T  x.  ( H `  x ) )  <  w  <->  ( T  x.  ( H `  x
) )  <  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  j
) ) )
244243rexrn 5667 . . . . . . . . . . . . . 14  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
)  Fn  NN  ->  ( E. w  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ( T  x.  ( H `  x ) )  < 
w  <->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <  ( (
n  e.  NN  |->  ( ( F `  n
) `  x )
) `  j )
) )
245242, 244syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( E. w  e. 
ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) ( T  x.  ( H `
 x ) )  <  w  <->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) `  j )
) )
246 fvex 5539 . . . . . . . . . . . . . . . 16  |-  ( ( F `  j ) `
 x )  e. 
_V
247150, 167, 246fvmpt 5602 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  j
)  =  ( ( F `  j ) `
 x ) )
248247breq2d 4035 . . . . . . . . . . . . . 14  |-  ( j  e.  NN  ->  (
( T  x.  ( H `  x )
)  <  ( (
n  e.  NN  |->  ( ( F `  n
) `  x )
) `  j )  <->  ( T  x.  ( H `
 x ) )  <  ( ( F `
 j ) `  x ) ) )
249248rexbiia 2576 . . . . . . . . . . . . 13  |-  ( E. j  e.  NN  ( T  x.  ( H `  x ) )  < 
( ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) `  j )  <->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <  ( ( F `  j ) `
 x ) )
250245, 249syl6bb 252 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( E. w  e. 
ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) ( T  x.  ( H `
 x ) )  <  w  <->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <  ( ( F `  j ) `
 x ) ) )
251241, 250mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <  ( ( F `  j ) `  x ) )
252203, 165remulcld 8863 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  e.  RR )
253252adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  0  <  ( H `  x ) ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  e.  RR )
254118adantlr 695 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  ( F `  j ) : RR --> ( 0 [,) 
+oo ) )
255 simplr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  x  e.  RR )
256 ffvelrn 5663 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  j
) : RR --> ( 0 [,)  +oo )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  e.  ( 0 [,)  +oo ) )
257254, 255, 256syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( F `  j
) `  x )  e.  ( 0 [,)  +oo ) )
258 elrege0 10746 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  j
) `  x )  e.  ( 0 [,)  +oo ) 
<->  ( ( ( F `
 j ) `  x )  e.  RR  /\  0  <_  ( ( F `  j ) `  x ) ) )
259257, 258sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( ( F `  j ) `  x
)  e.  RR  /\  0  <_  ( ( F `
 j ) `  x ) ) )
260259simpld 445 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( F `  j
) `  x )  e.  RR )
261260adantlrr 701 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  0  <  ( H `  x ) ) )  /\  j  e.  NN )  ->  ( ( F `
 j ) `  x )  e.  RR )
262 ltle 8910 . . . . . . . . . . . . 13  |-  ( ( ( T  x.  ( H `  x )
)  e.  RR  /\  ( ( F `  j ) `  x
)  e.  RR )  ->  ( ( T  x.  ( H `  x ) )  < 
( ( F `  j ) `  x
)  ->  ( T  x.  ( H `  x
) )  <_  (
( F `  j
) `  x )
) )
263253, 261, 262syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR  /\  0  <  ( H `  x ) ) )  /\  j  e.  NN )  ->  ( ( T  x.  ( H `  x ) )  < 
( ( F `  j ) `  x
)  ->  ( T  x.  ( H `  x
) )  <_  (
( F `  j
) `  x )
) )
264263reximdva 2655 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( E. j  e.  NN  ( T  x.  ( H `  x ) )  <  ( ( F `  j ) `
 x )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) ) )
265251, 264mpd 14 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) )
266265anassrs 629 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  0  <  ( H `  x
) )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
267 ne0i 3461 . . . . . . . . . . . 12  |-  ( 1  e.  NN  ->  NN  =/=  (/) )
268171, 267ax-mp 8 . . . . . . . . . . 11  |-  NN  =/=  (/)
26972adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  -> 
( T  x.  ( H `  x )
)  e.  RR )
270269adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  e.  RR )
2717a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  0  e.  RR )
272259adantlrr 701 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( ( ( F `  j ) `
 x )  e.  RR  /\  0  <_ 
( ( F `  j ) `  x
) ) )
273272simpld 445 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( ( F `
 j ) `  x )  e.  RR )
274 simplrr 737 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( H `  x )  <_  0
)
27562adantrr 697 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  -> 
( H `  x
)  e.  RR )
276275adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( H `  x )  e.  RR )
27722ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  T  e.  RR )
27821simp2d 968 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <  T )
279278ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  0  <  T
)
280 lemul2 9609 . . . . . . . . . . . . . . . 16  |-  ( ( ( H `  x
)  e.  RR  /\  0  e.  RR  /\  ( T  e.  RR  /\  0  <  T ) )  -> 
( ( H `  x )  <_  0  <->  ( T  x.  ( H `
 x ) )  <_  ( T  x.  0 ) ) )
281276, 271, 277, 279, 280syl112anc 1186 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( ( H `
 x )  <_ 
0  <->  ( T  x.  ( H `  x ) )  <_  ( T  x.  0 ) ) )
282274, 281mpbid 201 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  <_  ( T  x.  0 ) )
283277recnd 8861 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  T  e.  CC )
284283mul01d 9011 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  0 )  =  0 )
285282, 284breqtrd 4047 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  <_  0 )
286272simprd 449 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  0  <_  (
( F `  j
) `  x )
)
287270, 271, 273, 285, 286letrd 8973 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
288287ralrimiva 2626 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  ->  A. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) )
289 r19.2z 3543 . . . . . . . . . . 11  |-  ( ( NN  =/=  (/)  /\  A. j  e.  NN  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
290268, 288, 289sylancr 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) )
291290anassrs 629 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( H `  x )  <_  0 )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
2927a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  0  e.  RR )
293266, 291, 292, 62ltlecasei 8928 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
294293ralrimiva 2626 . . . . . . 7  |-  ( ph  ->  A. x  e.  RR  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) )
295 rabid2 2717 . . . . . . 7  |-  ( RR  =  { x  e.  RR  |  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) }  <->  A. x  e.  RR  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
296294, 295sylibr 203 . . . . . 6  |-  ( ph  ->  RR  =  { x  e.  RR  |  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) } )
297 iunrab 3949 . . . . . 6  |-  U_ j  e.  NN  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) }  =  {
x  e.  RR  |  E. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) }
298296, 297syl6eqr 2333 . . . . 5  |-  ( ph  ->  RR  =  U_ j  e.  NN  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) } )
299155iuneq2dv 3926 . . . . 5  |-  ( ph  ->  U_ j  e.  NN  ( A `  j )  =  U_ j  e.  NN  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) } )
300 ffn 5389 . . . . . . 7  |-  ( A : NN --> dom  vol  ->  A  Fn  NN )
301104, 300syl 15 . . . . . 6  |-  ( ph  ->  A  Fn  NN )
302 fniunfv 5773 . . . . . 6  |-  ( A  Fn  NN  ->  U_ j  e.  NN  ( A `  j )  =  U. ran  A )
303301, 302syl 15 . . . . 5  |-  ( ph  ->  U_ j  e.  NN  ( A `  j )  =  U. ran  A
)
304298, 299, 3033eqtr2rd 2322 . . . 4  |-  ( ph  ->  U. ran  A  =  RR )
305 eqid 2283 . . . 4  |-  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) )
306104, 163, 304, 13, 305itg1climres 19069 . . 3  |-  ( ph  ->  ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) )  ~~>  ( S.1 `  H ) )
307 nnex 9752 . . . . 5  |-  NN  e.  _V
308307mptex 5746 . . . 4  |-  ( j  e.  NN  |->  ( T  x.  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )  e.  _V
309308a1i 10 . . 3  |-  ( ph  ->  ( j  e.  NN  |->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )  e. 
_V )
310 fveq2 5525 . . . . . . . . . . 11  |-  ( j  =  k  ->  ( A `  j )  =  ( A `  k ) )
311310eleq2d 2350 . . . . . . . . . 10  |-  ( j  =  k  ->  (
x  e.  ( A `
 j )  <->  x  e.  ( A `  k ) ) )
312311ifbid 3583 . . . . . . . . 9  |-  ( j  =  k  ->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 )  =  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )
313312mpteq2dv 4107 . . . . . . . 8  |-  ( j  =  k  ->  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) )
314313fveq2d 5529 . . . . . . 7  |-  ( j  =  k  ->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) )  =  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) ) )
315 eqid 2283 . . . . . . 7  |-  ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) )  =  ( j  e.  NN  |->  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) )
316 fvex 5539 . . . . . . 7  |-  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) )  e. 
_V
317314, 315, 316fvmpt 5602 . . . . . 6  |-  ( k  e.  NN  ->  (
( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k )  =  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) ) ) )
318317adantl 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k )  =  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) ) ) )
31913adantr 451 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  H  e. 
dom  S.1 )
320 ffvelrn 5663 . . . . . . . 8  |-  ( ( A : NN --> dom  vol  /\  k  e.  NN )  ->  ( A `  k )  e.  dom  vol )
321104, 320sylan 457 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( A `
 k )  e. 
dom  vol )
322 eqid 2283 . . . . . . . 8  |-  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )
323322i1fres 19060 . . . . . . 7  |-  ( ( H  e.  dom  S.1  /\  ( A `  k
)  e.  dom  vol )  ->  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) )  e.  dom  S.1 )
324319, 321, 323syl2anc 642 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )  e.  dom  S.1 )
325 itg1cl 19040 . . . . . 6  |-  ( ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) )  e.  dom  S.1 
->  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) )  e.  RR )
326324, 325syl 15 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) )  e.  RR )
327318, 326eqeltrd 2357 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k )  e.  RR )
328327recnd 8861 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k )  e.  CC )
329314oveq2d 5874 . . . . . 6  |-  ( j  =  k  ->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) )  =  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) ) ) ) )
330 eqid 2283 . . . . . 6  |-  ( j  e.  NN  |->  ( T  x.  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )  =  ( j  e.  NN  |->  ( T  x.  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )
331 ovex 5883 . . . . . 6  |-  ( T  x.  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) ) )  e.  _V
332329, 330, 331fvmpt 5602 . . . . 5  |-  ( k  e.  NN  ->  (
( j  e.  NN  |->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) ) `  k )  =  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) ) ) )
333317oveq2d 5874 . . . . 5  |-  ( k  e.  NN  ->  ( T  x.  ( (
j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k ) )  =  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) ) ) )
334332, 333eqtr4d 2318 . . . 4  |-  ( k  e.  NN  ->  (
( j  e.  NN  |->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) ) `  k )  =  ( T  x.  ( ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k ) ) )
335334adantl 452 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) ) `  k )  =  ( T  x.  ( ( j  e.  NN  |->  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) `
 k ) ) )
3361, 3, 306, 59, 309, 328, 335climmulc2 12110 . 2  |-  ( ph  ->  ( j  e.  NN  |->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )  ~~>  ( T  x.  ( S.1 `  H
) ) )
337 rexr 8877 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  RR* )
338337anim1i 551 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
339 elrege0 10746 . . . . . . . . 9  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
340 elxrge0 10747 . . . . . . . . 9  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
341338, 339, 3403imtr4i 257 . . . . . . . 8  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
342341ssriv 3184 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
343 fss 5397 . . . . . . 7  |-  ( ( ( F `  n
) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  ( F `  n ) : RR --> ( 0 [,] 
+oo ) )
3446, 342, 343sylancl 643 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n ) : RR --> ( 0 [,] 
+oo ) )
345 itg2mono.10 . . . . . . 7  |-  ( ph  ->  S  e.  RR )
346345adantr 451 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  S  e.  RR )
347 itg2cl 19087 . . . . . . . . . . . 12  |-  ( ( F `  n ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( F `  n ) )  e. 
RR* )
348344, 347syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  RR* )
349 eqid 2283 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  ( S.2 `  ( F `  n
) ) )  =  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )
350348, 349fmptd 5684 . . . . . . . . . 10  |-  ( ph  ->  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) : NN --> RR* )
351 frn 5395 . . . . . . . . . 10  |-  ( ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) : NN --> RR*  ->  ran  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )  C_  RR* )
352350, 351syl 15 . . . . . . . . 9  |-  ( ph  ->  ran  ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) )  C_  RR* )
353352adantr 451 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )  C_  RR* )
354 fvex 5539 . . . . . . . . . . 11  |-  ( S.2 `  ( F `  n
) )  e.  _V
355354elabrex 5765 . . . . . . . . . 10  |-  ( n  e.  NN  ->  ( S.2 `  ( F `  n ) )  e. 
{ x  |  E. n  e.  NN  x  =  ( S.2 `  ( F `  n )
) } )
356355adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  {
x  |  E. n  e.  NN  x  =  ( S.2 `  ( F `
 n ) ) } )
357349rnmpt 4925 . . . . . . . . 9  |-  ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )  =  { x  |  E. n  e.  NN  x  =  ( S.2 `  ( F `  n
) ) }
358356, 357syl6eleqr 2374 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  ran  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) )
359 supxrub 10643 . . . . . . . 8  |-  ( ( ran  ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) )  C_  RR*  /\  ( S.2 `  ( F `  n ) )  e. 
ran  ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) )  -> 
( S.2 `  ( F `
 n ) )  <_  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) ,  RR* ,  <  ) )
360353, 358, 359syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  <_  sup ( ran  ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) ,  RR* ,  <  ) )
361 itg2mono.6 . . . . . . 7  |-  S  =  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) ,  RR* ,  <  )
362360, 361syl6breqr 4063 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  <_  S
)
363 itg2lecl 19093 . . . . . 6  |-  ( ( ( F `  n
) : RR --> ( 0 [,]  +oo )  /\  S  e.  RR  /\  ( S.2 `  ( F `  n
) )  <_  S
)  ->  ( S.2 `  ( F `  n
) )  e.  RR )
364344, 346, 362, 363syl3anc 1182 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  RR )
365364, 349fmptd 5684 . . . 4  |-  ( ph  ->  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) : NN --> RR )
366344ralrimiva 2626 . . . . . . . . . 10  |-  ( ph  ->  A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,]  +oo ) )
367 fveq2 5525 . . . . . . . . . . . 12  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
368367feq1d 5379 . . . . . . . . . . 11  |-  ( n  =  k  ->  (
( F `  n
) : RR --> ( 0 [,]  +oo )  <->  ( F `  k ) : RR --> ( 0 [,]  +oo ) ) )
369368cbvralv 2764 . . . . . . . . . 10  |-  ( A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,] 
+oo )  <->  A. k  e.  NN  ( F `  k ) : RR --> ( 0 [,]  +oo ) )
370366, 369sylib 188 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  NN  ( F `  k ) : RR --> ( 0 [,]  +oo ) )
371 peano2nn 9758 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
n  +  1 )  e.  NN )
372 fveq2 5525 . . . . . . . . . . 11  |-  ( k  =  ( n  + 
1 )  ->  ( F `  k )  =  ( F `  ( n  +  1
) ) )
373372feq1d 5379 . . . . . . . . . 10  |-  ( k  =  ( n  + 
1 )  ->  (
( F `  k
) : RR --> ( 0 [,]  +oo )  <->  ( F `  ( n  +  1 ) ) : RR --> ( 0 [,]  +oo ) ) )
374373rspccva 2883 . . . . . . . . 9  |-  ( ( A. k  e.  NN  ( F `  k ) : RR --> ( 0 [,]  +oo )  /\  (
n  +  1 )  e.  NN )  -> 
( F `  (
n  +  1 ) ) : RR --> ( 0 [,]  +oo ) )
375370, 371, 374syl2an 463 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 ( n  + 
1 ) ) : RR --> ( 0 [,] 
+oo ) )
376 itg2le 19094 . . . . . . . 8  |-  ( ( ( F `  n
) : RR --> ( 0 [,]  +oo )  /\  ( F `  ( n  +  1 ) ) : RR --> ( 0 [,]  +oo )  /\  ( F `  n )  o R  <_  ( F `
 ( n  + 
1 ) ) )  ->  ( S.2 `  ( F `  n )
)  <_  ( S.2 `  ( F `  (
n  +  1 ) ) ) )
377344, 375, 105, 376syl3anc 1182 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  <_  ( S.2 `  ( F `  ( n  +  1
) ) ) )
378377ralrimiva 2626 . . . . . 6  |-  ( ph  ->  A. n  e.  NN  ( S.2 `  ( F `
 n ) )  <_  ( S.2 `  ( F `  ( n  +  1 ) ) ) )
379367fveq2d 5529 . . . . . . . . . 10  |-  ( n  =  k  ->  ( S.2 `  ( F `  n ) )  =  ( S.2 `  ( F `  k )
) )
380 fvex 5539 . . . . . . . . . 10  |-  ( S.2 `  ( F `  k
) )  e.  _V
381379, 349, 380fvmpt 5602 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  =  ( S.2 `  ( F `  k )
) )
382 peano2nn 9758 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
383 fveq2 5525 . . . . . . . . . . . 12  |-  ( n  =  ( k  +  1 )  ->  ( F `  n )  =  ( F `  ( k  +  1 ) ) )
384383fveq2d 5529 . . . . . . . . . . 11  |-  ( n  =  ( k  +  1 )  ->  ( S.2 `  ( F `  n ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
385 fvex 5539 . . . . . . . . . . 11  |-  ( S.2 `  ( F `  (
k  +  1 ) ) )  e.  _V
386384, 349, 385fvmpt 5602 . . . . . . . . . 10  |-  ( ( k  +  1 )  e.  NN  ->  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
387382, 386syl 15 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
388381, 387breq12d 4036 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) `  k
)  <_  ( (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) )  <-> 
( S.2 `  ( F `
 k ) )  <_  ( S.2 `  ( F `  ( k  +  1 ) ) ) ) )
389388ralbiia 2575 . . . . . . 7  |-  ( A. k  e.  NN  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  <_  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n
) ) ) `  ( k  +  1 ) )  <->  A. k  e.  NN  ( S.2 `  ( F `  k )
)  <_  ( S.2 `  ( F `  (
k  +  1 ) ) ) )
390 oveq1 5865 . . . . . . . . . . 11  |-  ( n  =  k  ->  (
n  +  1 )  =  ( k  +  1 ) )
391390fveq2d 5529 . . . . . . . . . 10  |-  ( n  =  k  ->  ( F `  ( n  +  1 ) )  =  ( F `  ( k  +  1 ) ) )
392391fveq2d 5529 . . . . . . . . 9  |-  ( n  =  k  ->  ( S.2 `  ( F `  ( n  +  1
) ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
393379, 392breq12d 4036 . . . . . . . 8  |-  ( n  =  k  ->  (
( S.2 `  ( F `
 n ) )  <_  ( S.2 `  ( F `  ( n  +  1 ) ) )  <->  ( S.2 `  ( F `  k )
)  <_  ( S.2 `  ( F `  (
k  +  1 ) ) ) ) )
394393cbvralv 2764 . . . . . . 7  |-  ( A. n  e.  NN  ( S.2 `  ( F `  n ) )  <_ 
( S.2 `  ( F `
 ( n  + 
1 ) ) )  <->  A. k  e.  NN  ( S.2 `  ( F `
 k ) )  <_  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
395389, 394bitr4i 243 . . . . . 6  |-  ( A. k  e.  NN  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  <_  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n
) ) ) `  ( k  +  1 ) )  <->  A. n  e.  NN  ( S.2 `  ( F `  n )
)  <_  ( S.2 `  ( F `  (
n  +  1 ) ) ) )
396378, 395sylibr 203 . . . . 5  |-  ( ph  ->  A. k  e.  NN  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) `  k
)  <_  ( (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) ) )
397396r19.21bi 2641 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  <_  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n
) ) ) `  ( k  +  1 ) ) )
398362ralrimiva 2626 . . . . 5  |-  ( ph  ->  A. n  e.  NN  ( S.2 `  ( F `
 n ) )  <_  S )
399381breq1d 4033 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) `  k
)  <_  x  <->  ( S.2 `  ( F `  k
) )  <_  x
) )