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

Theorem itg2monolem1 19634
Description: Lemma for itg2mono 19637. 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 19637. 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 19598. 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 10513 . 2  |-  NN  =  ( ZZ>= `  1 )
2 1z 10303 . . 3  |-  1  e.  ZZ
32a1i 11 . 2  |-  ( ph  ->  1  e.  ZZ )
4 readdcl 9065 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  +  y )  e.  RR )
54adantl 453 . . . . . . . . . . . . . . 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 9083 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
8 pnfxr 10705 . . . . . . . . . . . . . . . . 17  |-  +oo  e.  RR*
9 icossre 10983 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
107, 8, 9mp2an 654 . . . . . . . . . . . . . . . 16  |-  ( 0 [,)  +oo )  C_  RR
11 fss 5591 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  n
) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F `
 n ) : RR --> RR )
126, 10, 11sylancl 644 . . . . . . . . . . . . . . 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 9123 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR*
16 1re 9082 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR
1716rexri 9129 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR*
18 elioo2 10949 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  RR*  /\  1  e.  RR* )  ->  ( T  e.  ( 0 (,) 1 )  <->  ( T  e.  RR  /\  0  < 
T  /\  T  <  1 ) ) )
1915, 17, 18mp2an 654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T  e.  ( 0 (,) 1 )  <->  ( T  e.  RR  /\  0  < 
T  /\  T  <  1 ) )
2014, 19sylib 189 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( T  e.  RR  /\  0  <  T  /\  T  <  1 ) )
2120simp1d 969 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  e.  RR )
2221renegcld 9456 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
-u T  e.  RR )
2313, 22i1fmulc 19587 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( RR  X.  { -u T } )  o F  x.  H
)  e.  dom  S.1 )
2423adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  e. 
dom  S.1 )
25 i1ff 19560 . . . . . . . . . . . . . . . 16  |-  ( ( ( RR  X.  { -u T } )  o F  x.  H )  e.  dom  S.1  ->  ( ( RR  X.  { -u T } )  o F  x.  H ) : RR --> RR )
2624, 25syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H ) : RR --> RR )
27 reex 9073 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
2827a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  RR  e.  _V )
29 inidm 3542 . . . . . . . . . . . . . . 15  |-  ( RR 
i^i  RR )  =  RR
305, 12, 26, 28, 28, 29off 6312 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) ) : RR --> RR )
3130adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) : RR --> RR )
32 ffn 5583 . . . . . . . . . . . . 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 )
3331, 32syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) )  Fn  RR )
34 elpreima 5842 . . . . . . . . . . . 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 ) ) ) )
3533, 34syl 16 . . . . . . . . . . 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 ) ) ) )
36 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  x  e.  RR )
3736biantrurd 495 . . . . . . . . . . 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 ) ) ) )
3835, 37bitr4d 248 . . . . . . . . . 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 ) ) )
3930ffvelrnda 5862 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) ) `
 x )  e.  RR )
4039biantrurd 495 . . . . . . . . . . 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 ) ) )
41 elioomnf 10991 . . . . . . . . . . . 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 ) ) )
4215, 41ax-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 ) )
4340, 42syl6rbbr 256 . . . . . . . . . 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 ) )
44 ffn 5583 . . . . . . . . . . . . . . 15  |-  ( ( F `  n ) : RR --> RR  ->  ( F `  n )  Fn  RR )
4512, 44syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  Fn  RR )
46 ffn 5583 . . . . . . . . . . . . . . 15  |-  ( ( ( RR  X.  { -u T } )  o F  x.  H ) : RR --> RR  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  Fn  RR )
4726, 46syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  Fn  RR )
48 eqidd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
) `  x )  =  ( ( F `
 n ) `  x ) )
4922adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  -u T  e.  RR )
50 i1ff 19560 . . . . . . . . . . . . . . . . . . 19  |-  ( H  e.  dom  S.1  ->  H : RR --> RR )
5113, 50syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H : RR --> RR )
52 ffn 5583 . . . . . . . . . . . . . . . . . 18  |-  ( H : RR --> RR  ->  H  Fn  RR )
5351, 52syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  H  Fn  RR )
5453adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  H  Fn  RR )
55 eqidd 2436 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  =  ( H `  x ) )
5628, 49, 54, 55ofc1 6319 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( RR  X.  { -u T } )  o F  x.  H
) `  x )  =  ( -u T  x.  ( H `  x
) ) )
5721recnd 9106 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  CC )
5857ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  T  e.  CC )
5951ffvelrnda 5862 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( H `
 x )  e.  RR )
6059adantlr 696 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  e.  RR )
6160recnd 9106 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  e.  CC )
6258, 61mulneg1d 9478 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( -u T  x.  ( H `
 x ) )  =  -u ( T  x.  ( H `  x ) ) )
6356, 62eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( RR  X.  { -u T } )  o F  x.  H
) `  x )  =  -u ( T  x.  ( H `  x ) ) )
6445, 47, 28, 28, 29, 48, 63ofval 6306 . . . . . . . . . . . . 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 )
) ) )
6512ffvelrnda 5862 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
) `  x )  e.  RR )
6665recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  n
) `  x )  e.  CC )
6721adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
6867, 59remulcld 9108 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  RR )
6968adantlr 696 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  RR )
7069recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  CC )
7166, 70negsubd 9409 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n ) `  x
)  +  -u ( T  x.  ( H `  x ) ) )  =  ( ( ( F `  n ) `
 x )  -  ( T  x.  ( H `  x )
) ) )
7264, 71eqtrd 2467 . . . . . . . . . . . 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 ) ) ) )
7372breq1d 4214 . . . . . . . . . . 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
) )
747a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  0  e.  RR )
7565, 69, 74ltsubaddd 9614 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( ( F `
 n ) `  x )  -  ( T  x.  ( H `  x ) ) )  <  0  <->  ( ( F `  n ) `  x )  <  (
0  +  ( T  x.  ( H `  x ) ) ) ) )
7670addid2d 9259 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
0  +  ( T  x.  ( H `  x ) ) )  =  ( T  x.  ( H `  x ) ) )
7776breq2d 4216 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( ( F `  n ) `  x
)  <  ( 0  +  ( T  x.  ( H `  x ) ) )  <->  ( ( F `  n ) `  x )  <  ( T  x.  ( H `  x ) ) ) )
7873, 75, 773bitrd 271 . . . . . . . . . 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 ) ) ) )
7938, 43, 783bitrd 271 . . . . . . . . 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 ) ) ) )
8079notbid 286 . . . . . . . 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 )
) ) )
81 eldif 3322 . . . . . . . . . 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 ) ) ) )
8281baib 872 . . . . . . . . 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 ) ) ) )
8382adantl 453 . . . . . . . 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 ) ) ) )
8469, 65lenltd 9211 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  n ) `  x )  <->  -.  (
( F `  n
) `  x )  <  ( T  x.  ( H `  x )
) ) )
8580, 83, 843bitr4d 277 . . . . . . 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 ) ) )
8685rabbi2dva 3541 . . . . . 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
) } )
87 rembl 19427 . . . . . . 7  |-  RR  e.  dom  vol
88 itg2mono.2 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e. MblFn
)
89 i1fmbf 19559 . . . . . . . . . . 11  |-  ( ( ( RR  X.  { -u T } )  o F  x.  H )  e.  dom  S.1  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  e. MblFn )
9024, 89syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( RR  X.  { -u T } )  o F  x.  H )  e. MblFn
)
9188, 90mbfadd 19545 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( F `  n )  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H ) )  e. MblFn )
92 mbfima 19516 . . . . . . . . 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 )
9391, 30, 92syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( `' ( ( F `  n )  o F  +  ( ( RR 
X.  { -u T } )  o F  x.  H ) )
" (  -oo (,) 0 ) )  e. 
dom  vol )
94 cmmbl 19421 . . . . . . . 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 )
9593, 94syl 16 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( RR 
\  ( `' ( ( F `  n
)  o F  +  ( ( RR  X.  { -u T } )  o F  x.  H
) ) " (  -oo (,) 0 ) ) )  e.  dom  vol )
96 inmbl 19428 . . . . . . 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 )
9787, 95, 96sylancr 645 . . . . . 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 )
9886, 97eqeltrrd 2510 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  n ) `  x
) }  e.  dom  vol )
99 itg2mono.11 . . . . 5  |-  A  =  ( n  e.  NN  |->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  n ) `  x ) } )
10098, 99fmptd 5885 . . . 4  |-  ( ph  ->  A : NN --> dom  vol )
101 itg2mono.4 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  o R  <_  ( F `  ( n  +  1 ) ) )
102101ralrimiva 2781 . . . . . . . . . . 11  |-  ( ph  ->  A. n  e.  NN  ( F `  n )  o R  <_  ( F `  ( n  +  1 ) ) )
103 fveq2 5720 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  ( F `  n )  =  ( F `  j ) )
104 oveq1 6080 . . . . . . . . . . . . . 14  |-  ( n  =  j  ->  (
n  +  1 )  =  ( j  +  1 ) )
105104fveq2d 5724 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  ( F `  ( n  +  1 ) )  =  ( F `  ( j  +  1 ) ) )
106103, 105breq12d 4217 . . . . . . . . . . . 12  |-  ( n  =  j  ->  (
( F `  n
)  o R  <_ 
( F `  (
n  +  1 ) )  <->  ( F `  j )  o R  <_  ( F `  ( j  +  1 ) ) ) )
107106cbvralv 2924 . . . . . . . . . . 11  |-  ( A. n  e.  NN  ( F `  n )  o R  <_  ( F `
 ( n  + 
1 ) )  <->  A. j  e.  NN  ( F `  j )  o R  <_  ( F `  ( j  +  1 ) ) )
108102, 107sylib 189 . . . . . . . . . 10  |-  ( ph  ->  A. j  e.  NN  ( F `  j )  o R  <_  ( F `  ( j  +  1 ) ) )
109108r19.21bi 2796 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j )  o R  <_  ( F `  ( j  +  1 ) ) )
1106ralrimiva 2781 . . . . . . . . . . . . 13  |-  ( ph  ->  A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,)  +oo ) )
111103feq1d 5572 . . . . . . . . . . . . . 14  |-  ( n  =  j  ->  (
( F `  n
) : RR --> ( 0 [,)  +oo )  <->  ( F `  j ) : RR --> ( 0 [,)  +oo ) ) )
112111cbvralv 2924 . . . . . . . . . . . . 13  |-  ( A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,) 
+oo )  <->  A. j  e.  NN  ( F `  j ) : RR --> ( 0 [,)  +oo ) )
113110, 112sylib 189 . . . . . . . . . . . 12  |-  ( ph  ->  A. j  e.  NN  ( F `  j ) : RR --> ( 0 [,)  +oo ) )
114113r19.21bi 2796 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j ) : RR --> ( 0 [,) 
+oo ) )
115 ffn 5583 . . . . . . . . . . 11  |-  ( ( F `  j ) : RR --> ( 0 [,)  +oo )  ->  ( F `  j )  Fn  RR )
116114, 115syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j )  Fn  RR )
117 peano2nn 10004 . . . . . . . . . . . 12  |-  ( j  e.  NN  ->  (
j  +  1 )  e.  NN )
118 fveq2 5720 . . . . . . . . . . . . . 14  |-  ( n  =  ( j  +  1 )  ->  ( F `  n )  =  ( F `  ( j  +  1 ) ) )
119118feq1d 5572 . . . . . . . . . . . . 13  |-  ( n  =  ( j  +  1 )  ->  (
( F `  n
) : RR --> ( 0 [,)  +oo )  <->  ( F `  ( j  +  1 ) ) : RR --> ( 0 [,)  +oo ) ) )
120119rspccva 3043 . . . . . . . . . . . 12  |-  ( ( A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,)  +oo )  /\  (
j  +  1 )  e.  NN )  -> 
( F `  (
j  +  1 ) ) : RR --> ( 0 [,)  +oo ) )
121110, 117, 120syl2an 464 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 ( j  +  1 ) ) : RR --> ( 0 [,) 
+oo ) )
122 ffn 5583 . . . . . . . . . . 11  |-  ( ( F `  ( j  +  1 ) ) : RR --> ( 0 [,)  +oo )  ->  ( F `  ( j  +  1 ) )  Fn  RR )
123121, 122syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 ( j  +  1 ) )  Fn  RR )
12427a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  RR  e.  _V )
125 eqidd 2436 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  =  ( ( F `
 j ) `  x ) )
126 eqidd 2436 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  (
j  +  1 ) ) `  x )  =  ( ( F `
 ( j  +  1 ) ) `  x ) )
127116, 123, 124, 124, 29, 125, 126ofrfval 6305 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( F `  j )  o R  <_  ( F `  ( j  +  1 ) )  <->  A. x  e.  RR  ( ( F `  j ) `  x
)  <_  ( ( F `  ( j  +  1 ) ) `
 x ) ) )
128109, 127mpbid 202 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  A. x  e.  RR  ( ( F `
 j ) `  x )  <_  (
( F `  (
j  +  1 ) ) `  x ) )
129128r19.21bi 2796 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  <_  ( ( F `  ( j  +  1 ) ) `  x
) )
13021ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  T  e.  RR )
13151adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  H : RR
--> RR )
132131ffvelrnda 5862 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  ( H `  x )  e.  RR )
133130, 132remulcld 9108 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  ( T  x.  ( H `  x ) )  e.  RR )
134 fss 5591 . . . . . . . . . 10  |-  ( ( ( F `  j
) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F `
 j ) : RR --> RR )
135114, 10, 134sylancl 644 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 j ) : RR --> RR )
136135ffvelrnda 5862 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  j
) `  x )  e.  RR )
137 fss 5591 . . . . . . . . . 10  |-  ( ( ( F `  (
j  +  1 ) ) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F `
 ( j  +  1 ) ) : RR --> RR )
138121, 10, 137sylancl 644 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( F `
 ( j  +  1 ) ) : RR --> RR )
139138ffvelrnda 5862 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( F `  (
j  +  1 ) ) `  x )  e.  RR )
140 letr 9159 . . . . . . . 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
) ) )
141133, 136, 139, 140syl3anc 1184 . . . . . . 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
) ) )
142129, 141mpan2d 656 . . . . . 6  |-  ( ( ( ph  /\  j  e.  NN )  /\  x  e.  RR )  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x )  ->  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) ) )
143142ss2rabdv 3416 . . . . 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
) } )
144103fveq1d 5722 . . . . . . . . 9  |-  ( n  =  j  ->  (
( F `  n
) `  x )  =  ( ( F `
 j ) `  x ) )
145144breq2d 4216 . . . . . . . 8  |-  ( n  =  j  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  n ) `  x )  <->  ( T  x.  ( H `  x
) )  <_  (
( F `  j
) `  x )
) )
146145rabbidv 2940 . . . . . . 7  |-  ( n  =  j  ->  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  n ) `  x
) }  =  {
x  e.  RR  | 
( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) } )
14727rabex 4346 . . . . . . 7  |-  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) }  e.  _V
148146, 99, 147fvmpt 5798 . . . . . 6  |-  ( j  e.  NN  ->  ( A `  j )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) } )
149148adantl 453 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 j )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) } )
150117adantl 453 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( j  +  1 )  e.  NN )
151118fveq1d 5722 . . . . . . . . 9  |-  ( n  =  ( j  +  1 )  ->  (
( F `  n
) `  x )  =  ( ( F `
 ( j  +  1 ) ) `  x ) )
152151breq2d 4216 . . . . . . . 8  |-  ( n  =  ( j  +  1 )  ->  (
( T  x.  ( H `  x )
)  <_  ( ( F `  n ) `  x )  <->  ( T  x.  ( H `  x
) )  <_  (
( F `  (
j  +  1 ) ) `  x ) ) )
153152rabbidv 2940 . . . . . . 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 ) } )
15427rabex 4346 . . . . . . 7  |-  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) }  e.  _V
155153, 99, 154fvmpt 5798 . . . . . 6  |-  ( ( j  +  1 )  e.  NN  ->  ( A `  ( j  +  1 ) )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  ( j  +  1 ) ) `  x
) } )
156150, 155syl 16 . . . . 5  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 ( j  +  1 ) )  =  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_  ( ( F `  ( j  +  1 ) ) `
 x ) } )
157143, 149, 1563sstr4d 3383 . . . 4  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 j )  C_  ( A `  ( j  +  1 ) ) )
15868adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  e.  RR )
15959adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( H `  x
)  e.  RR )
16065an32s 780 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  (
( F `  n
) `  x )  e.  RR )
161 eqid 2435 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) )
162160, 161fmptd 5885 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) : NN --> RR )
163 frn 5589 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) : NN --> RR  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  C_  RR )
164162, 163syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  C_  RR )
165 1nn 10003 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  NN
166 fdm 5587 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) : NN --> RR  ->  dom  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  NN )
167162, 166syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  dom  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =  NN )
168165, 167syl5eleqr 2522 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  1  e. 
dom  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) )
169 ne0i 3626 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  dom  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  ->  dom  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) )  =/=  (/) )
170168, 169syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  dom  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =/=  (/) )
171 dm0rn0 5078 . . . . . . . . . . . . . . . . . 18  |-  ( dom  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  (/)  <->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  (/) )
172171necon3bii 2630 . . . . . . . . . . . . . . . . 17  |-  ( dom  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =/=  (/)  <->  ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  =/=  (/) )
173170, 172sylib 189 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =/=  (/) )
174 itg2mono.5 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  E. y  e.  RR  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
)
175 ffn 5583 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  |->  ( ( F `  n
) `  x )
) : NN --> RR  ->  ( n  e.  NN  |->  ( ( F `  n
) `  x )
)  Fn  NN )
176162, 175syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) )  Fn  NN )
177 breq1 4207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  ( ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) `
 m )  -> 
( z  <_  y  <->  ( ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  <_  y )
)
178177ralrn 5865 . . . . . . . . . . . . . . . . . . . 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
) )
179176, 178syl 16 . . . . . . . . . . . . . . . . . . 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 ) )
180 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( F `  n )  =  ( F `  m ) )
181180fveq1d 5722 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( F `  n
) `  x )  =  ( ( F `
 m ) `  x ) )
182 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  m ) `
 x )  e. 
_V
183181, 161, 182fvmpt 5798 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN  ->  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  =  ( ( F `  m ) `
 x ) )
184183breq1d 4214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN  ->  (
( ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) `  m )  <_  y  <->  ( ( F `  m
) `  x )  <_  y ) )
185184ralbiia 2729 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. m  e.  NN  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  <_  y  <->  A. m  e.  NN  ( ( F `
 m ) `  x )  <_  y
)
186181breq1d 4214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
( ( F `  n ) `  x
)  <_  y  <->  ( ( F `  m ) `  x )  <_  y
) )
187186cbvralv 2924 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. n  e.  NN  (
( F `  n
) `  x )  <_  y  <->  A. m  e.  NN  ( ( F `  m ) `  x
)  <_  y )
188185, 187bitr4i 244 . . . . . . . . . . . . . . . . . . 19  |-  ( A. m  e.  NN  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  m
)  <_  y  <->  A. n  e.  NN  ( ( F `
 n ) `  x )  <_  y
)
189179, 188syl6bb 253 . . . . . . . . . . . . . . . . . 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
) )
190189rexbidv 2718 . . . . . . . . . . . . . . . . 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
) )
191174, 190mpbird 224 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  E. y  e.  RR  A. z  e. 
ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) z  <_  y )
192 suprcl 9960 . . . . . . . . . . . . . . . 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 )
193164, 173, 191, 192syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  )  e.  RR )
194193adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  )  e.  RR )
19520simp3d 971 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  <  1 )
196195adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  T  <  1 )
19721adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  T  e.  RR )
19816a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
1  e.  RR )
199 simprr 734 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
0  <  ( H `  x ) )
200 ltmul1 9852 . . . . . . . . . . . . . . . . 17  |-  ( ( T  e.  RR  /\  1  e.  RR  /\  (
( H `  x
)  e.  RR  /\  0  <  ( H `  x ) ) )  ->  ( T  <  1  <->  ( T  x.  ( H `  x ) )  <  ( 1  x.  ( H `  x ) ) ) )
201197, 198, 159, 199, 200syl112anc 1188 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  <  1  <->  ( T  x.  ( H `
 x ) )  <  ( 1  x.  ( H `  x
) ) ) )
202196, 201mpbid 202 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  <  ( 1  x.  ( H `  x ) ) )
203159recnd 9106 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( H `  x
)  e.  CC )
204203mulid2d 9098 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( 1  x.  ( H `  x )
)  =  ( H `
 x ) )
205202, 204breqtrd 4228 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  <  ( H `  x ) )
206 itg2mono.9 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  o R  <_  G )
207 itg2mono.1 . . . . . . . . . . . . . . . . . . . . 21  |-  G  =  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  ) )
208193, 207fmptd 5885 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  G : RR --> RR )
209 ffn 5583 . . . . . . . . . . . . . . . . . . . 20  |-  ( G : RR --> RR  ->  G  Fn  RR )
210208, 209syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  G  Fn  RR )
21127a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  e.  _V )
212 eqidd 2436 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  RR )  ->  ( H `
 y )  =  ( H `  y
) )
213 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
( F `  n
) `  x )  =  ( ( F `
 n ) `  y ) )
214213mpteq2dv 4288 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
n  e.  NN  |->  ( ( F `  n
) `  x )
)  =  ( n  e.  NN  |->  ( ( F `  n ) `
 y ) ) )
215214rneqd 5089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =  ran  ( n  e.  NN  |->  ( ( F `  n ) `  y
) ) )
216215supeq1d 7443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  sup ( ran  ( n  e.  NN  |->  ( ( F `
 n ) `  x ) ) ,  RR ,  <  )  =  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
217 ltso 9148 . . . . . . . . . . . . . . . . . . . . . 22  |-  <  Or  RR
218217supex 7460 . . . . . . . . . . . . . . . . . . . . 21  |-  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  y
) ) ,  RR ,  <  )  e.  _V
219216, 207, 218fvmpt 5798 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR  ->  ( G `  y )  =  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
220219adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  RR )  ->  ( G `
 y )  =  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
22153, 210, 211, 211, 29, 212, 220ofrfval 6305 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( H  o R  <_  G  <->  A. y  e.  RR  ( H `  y )  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `
 n ) `  y ) ) ,  RR ,  <  )
) )
222206, 221mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. y  e.  RR  ( H `  y )  <_  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  y )
) ,  RR ,  <  ) )
223 fveq2 5720 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
224223, 216breq12d 4217 . . . . . . . . . . . . . . . . . 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 ,  <  )
) )
225224cbvralv 2924 . . . . . . . . . . . . . . . . 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 ,  <  ) )
226222, 225sylibr 204 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. x  e.  RR  ( H `  x )  <_  sup ( ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
) ,  RR ,  <  ) )
227226r19.21bi 2796 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( H `
 x )  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `
 x ) ) ,  RR ,  <  ) )
228227adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( H `  x
)  <_  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  ) )
229158, 159, 194, 205, 228ltletrd 9222 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  <  sup ( ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ,  RR ,  <  ) )
230164adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  C_  RR )
231173adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) )  =/=  (/) )
232191adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. y  e.  RR  A. z  e.  ran  (
n  e.  NN  |->  ( ( F `  n
) `  x )
) z  <_  y
)
233 suprlub 9962 . . . . . . . . . . . . . 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 ) )
234230, 231, 232, 158, 233syl31anc 1187 . . . . . . . . . . . . 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 ) )
235229, 234mpbid 202 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. w  e.  ran  ( n  e.  NN  |->  ( ( F `  n ) `  x
) ) ( T  x.  ( H `  x ) )  < 
w )
236176adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( n  e.  NN  |->  ( ( F `  n ) `  x
) )  Fn  NN )
237 breq2 4208 . . . . . . . . . . . . . . 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
) ) )
238237rexrn 5864 . . . . . . . . . . . . . 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 )
) )
239236, 238syl 16 . . . . . . . . . . . . 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 )
) )
240 fvex 5734 . . . . . . . . . . . . . . . 16  |-  ( ( F `  j ) `
 x )  e. 
_V
241144, 161, 240fvmpt 5798 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( ( F `  n ) `  x
) ) `  j
)  =  ( ( F `  j ) `
 x ) )
242241breq2d 4216 . . . . . . . . . . . . . 14  |-  ( j  e.  NN  ->  (
( T  x.  ( H `  x )
)  <  ( (
n  e.  NN  |->  ( ( F `  n
) `  x )
) `  j )  <->  ( T  x.  ( H `
 x ) )  <  ( ( F `
 j ) `  x ) ) )
243242rexbiia 2730 . . . . . . . . . . . . 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 ) )
244239, 243syl6bb 253 . . . . . . . . . . . 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 ) ) )
245235, 244mpbid 202 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <  ( ( F `  j ) `  x ) )
246197, 159remulcld 9108 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  -> 
( T  x.  ( H `  x )
)  e.  RR )
247246adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  0  <  ( H `  x ) ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  e.  RR )
248114adantlr 696 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  ( F `  j ) : RR --> ( 0 [,) 
+oo ) )
249 simplr 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  x  e.  RR )
250248, 249ffvelrnd 5863 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( F `  j
) `  x )  e.  ( 0 [,)  +oo ) )
251 elrege0 10999 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  j
) `  x )  e.  ( 0 [,)  +oo ) 
<->  ( ( ( F `
 j ) `  x )  e.  RR  /\  0  <_  ( ( F `  j ) `  x ) ) )
252250, 251sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( ( F `  j ) `  x
)  e.  RR  /\  0  <_  ( ( F `
 j ) `  x ) ) )
253252simpld 446 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( F `  j
) `  x )  e.  RR )
254253adantlrr 702 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  0  <  ( H `  x ) ) )  /\  j  e.  NN )  ->  ( ( F `
 j ) `  x )  e.  RR )
255 ltle 9155 . . . . . . . . . . . . 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 )
) )
256247, 254, 255syl2anc 643 . . . . . . . . . . . 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 )
) )
257256reximdva 2810 . . . . . . . . . . 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 ) ) )
258245, 257mpd 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR  /\  0  < 
( H `  x
) ) )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) )
259258anassrs 630 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  0  <  ( H `  x
) )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
260 ne0i 3626 . . . . . . . . . . . 12  |-  ( 1  e.  NN  ->  NN  =/=  (/) )
261165, 260ax-mp 8 . . . . . . . . . . 11  |-  NN  =/=  (/)
26268adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  -> 
( T  x.  ( H `  x )
)  e.  RR )
263262adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  e.  RR )
2647a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  0  e.  RR )
265252adantlrr 702 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( ( ( F `  j ) `
 x )  e.  RR  /\  0  <_ 
( ( F `  j ) `  x
) ) )
266265simpld 446 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( ( F `
 j ) `  x )  e.  RR )
267 simplrr 738 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( H `  x )  <_  0
)
26859adantrr 698 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  -> 
( H `  x
)  e.  RR )
269268adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( H `  x )  e.  RR )
27021ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  T  e.  RR )
27120simp2d 970 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <  T )
272271ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  0  <  T
)
273 lemul2 9855 . . . . . . . . . . . . . . . 16  |-  ( ( ( H `  x
)  e.  RR  /\  0  e.  RR  /\  ( T  e.  RR  /\  0  <  T ) )  -> 
( ( H `  x )  <_  0  <->  ( T  x.  ( H `
 x ) )  <_  ( T  x.  0 ) ) )
274269, 264, 270, 272, 273syl112anc 1188 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( ( H `
 x )  <_ 
0  <->  ( T  x.  ( H `  x ) )  <_  ( T  x.  0 ) ) )
275267, 274mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  <_  ( T  x.  0 ) )
276270recnd 9106 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  T  e.  CC )
277276mul01d 9257 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  0 )  =  0 )
278275, 277breqtrd 4228 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  <_  0 )
279265simprd 450 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  0  <_  (
( F `  j
) `  x )
)
280263, 264, 266, 278, 279letrd 9219 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR  /\  ( H `  x )  <_  0 ) )  /\  j  e.  NN )  ->  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
281280ralrimiva 2781 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  ->  A. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) )
282 r19.2z 3709 . . . . . . . . . . 11  |-  ( ( NN  =/=  (/)  /\  A. j  e.  NN  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
283261, 281, 282sylancr 645 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR  /\  ( H `
 x )  <_ 
0 ) )  ->  E. j  e.  NN  ( T  x.  ( H `  x )
)  <_  ( ( F `  j ) `  x ) )
284283anassrs 630 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( H `  x )  <_  0 )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
2857a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  0  e.  RR )
286259, 284, 285, 59ltlecasei 9173 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) )
287286ralrimiva 2781 . . . . . . 7  |-  ( ph  ->  A. x  e.  RR  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) )
288 rabid2 2877 . . . . . . 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 ) )
289287, 288sylibr 204 . . . . . 6  |-  ( ph  ->  RR  =  { x  e.  RR  |  E. j  e.  NN  ( T  x.  ( H `  x ) )  <_  ( ( F `  j ) `  x ) } )
290 iunrab 4130 . . . . . 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 ) }
291289, 290syl6eqr 2485 . . . . 5  |-  ( ph  ->  RR  =  U_ j  e.  NN  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) } )
292149iuneq2dv 4106 . . . . 5  |-  ( ph  ->  U_ j  e.  NN  ( A `  j )  =  U_ j  e.  NN  { x  e.  RR  |  ( T  x.  ( H `  x ) )  <_ 
( ( F `  j ) `  x
) } )
293 ffn 5583 . . . . . . 7  |-  ( A : NN --> dom  vol  ->  A  Fn  NN )
294100, 293syl 16 . . . . . 6  |-  ( ph  ->  A  Fn  NN )
295 fniunfv 5986 . . . . . 6  |-  ( A  Fn  NN  ->  U_ j  e.  NN  ( A `  j )  =  U. ran  A )
296294, 295syl 16 . . . . 5  |-  ( ph  ->  U_ j  e.  NN  ( A `  j )  =  U. ran  A
)
297291, 292, 2963eqtr2rd 2474 . . . 4  |-  ( ph  ->  U. ran  A  =  RR )
298 eqid 2435 . . . 4  |-  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) )
299100, 157, 297, 13, 298itg1climres 19598 . . 3  |-  ( ph  ->  ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) )  ~~>  ( S.1 `  H ) )
300 nnex 9998 . . . . 5  |-  NN  e.  _V
301300mptex 5958 . . . 4  |-  ( j  e.  NN  |->  ( T  x.  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )  e.  _V
302301a1i 11 . . 3  |-  ( ph  ->  ( j  e.  NN  |->  ( T  x.  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 ) ) ) ) )  e. 
_V )
303 fveq2 5720 . . . . . . . . . . 11  |-  ( j  =  k  ->  ( A `  j )  =  ( A `  k ) )
304303eleq2d 2502 . . . . . . . . . 10  |-  ( j  =  k  ->  (
x  e.  ( A `
 j )  <->  x  e.  ( A `  k ) ) )
305304ifbid 3749 . . . . . . . . 9  |-  ( j  =  k  ->  if ( x  e.  ( A `  j ) ,  ( H `  x ) ,  0 )  =  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )
306305mpteq2dv 4288 . . . . . . . 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 ) ) )
307306fveq2d 5724 . . . . . . 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 ) ) ) )
308 eqid 2435 . . . . . . 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 ) ) ) )
309 fvex 5734 . . . . . . 7  |-  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) )  e. 
_V
310307, 308, 309fvmpt 5798 . . . . . 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 ) ) ) )
311310adantl 453 . . . . 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 ) ) ) )
31213adantr 452 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  H  e. 
dom  S.1 )
313100ffvelrnda 5862 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( A `
 k )  e. 
dom  vol )
314 eqid 2435 . . . . . . . 8  |-  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )
315314i1fres 19589 . . . . . . 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 )
316312, 313, 315syl2anc 643 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( x  e.  RR  |->  if ( x  e.  ( A `
 k ) ,  ( H `  x
) ,  0 ) )  e.  dom  S.1 )
317 itg1cl 19569 . . . . . 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 )
318316, 317syl 16 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) )  e.  RR )
319311, 318eqeltrd 2509 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k )  e.  RR )
320319recnd 9106 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( S.1 `  ( x  e.  RR  |->  if ( x  e.  ( A `
 j ) ,  ( H `  x
) ,  0 ) ) ) ) `  k )  e.  CC )
321307oveq2d 6089 . . . . . 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 ) ) ) ) )
322 eqid 2435 . . . . . 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 ) ) ) ) )
323 ovex 6098 . . . . . 6  |-  ( T  x.  ( S.1 `  (
x  e.  RR  |->  if ( x  e.  ( A `  k ) ,  ( H `  x ) ,  0 ) ) ) )  e.  _V
324321, 322, 323fvmpt 5798 . . . . 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 ) ) ) ) )
325310oveq2d 6089 . . . . 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 ) ) ) ) )
326324, 325eqtr4d 2470 . . . 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 ) ) )
327326adantl 453 . . 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 ) ) )
3281, 3, 299, 57, 302, 320, 327climmulc2 12422 . 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
) ) )
329 rexr 9122 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  RR* )
330329anim1i 552 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
331 elrege0 10999 . . . . . . . . 9  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
332 elxrge0 11000 . . . . . . . . 9  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
333330, 331, 3323imtr4i 258 . . . . . . . 8  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
334333ssriv 3344 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
335 fss 5591 . . . . . . 7  |-  ( ( ( F `  n
) : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  ( F `  n ) : RR --> ( 0 [,] 
+oo ) )
3366, 334, 335sylancl 644 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n ) : RR --> ( 0 [,] 
+oo ) )
337 itg2mono.10 . . . . . . 7  |-  ( ph  ->  S  e.  RR )
338337adantr 452 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  S  e.  RR )
339 itg2cl 19616 . . . . . . . . . . . 12  |-  ( ( F `  n ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( F `  n ) )  e. 
RR* )
340336, 339syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  RR* )
341 eqid 2435 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  ( S.2 `  ( F `  n
) ) )  =  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )
342340, 341fmptd 5885 . . . . . . . . . 10  |-  ( ph  ->  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) : NN --> RR* )
343 frn 5589 . . . . . . . . . 10  |-  ( ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) : NN --> RR*  ->  ran  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )  C_  RR* )
344342, 343syl 16 . . . . . . . . 9  |-  ( ph  ->  ran  ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) )  C_  RR* )
345344adantr 452 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )  C_  RR* )
346 fvex 5734 . . . . . . . . . . 11  |-  ( S.2 `  ( F `  n
) )  e.  _V
347346elabrex 5977 . . . . . . . . . 10  |-  ( n  e.  NN  ->  ( S.2 `  ( F `  n ) )  e. 
{ x  |  E. n  e.  NN  x  =  ( S.2 `  ( F `  n )
) } )
348347adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  {
x  |  E. n  e.  NN  x  =  ( S.2 `  ( F `
 n ) ) } )
349341rnmpt 5108 . . . . . . . . 9  |-  ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) )  =  { x  |  E. n  e.  NN  x  =  ( S.2 `  ( F `  n
) ) }
350348, 349syl6eleqr 2526 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  ran  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) )
351 supxrub 10895 . . . . . . . 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* ,  <  ) )
352345, 350, 351syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  <_  sup ( ran  ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) ,  RR* ,  <  ) )
353 itg2mono.6 . . . . . . 7  |-  S  =  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) ,  RR* ,  <  )
354352, 353syl6breqr 4244 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  <_  S
)
355 itg2lecl 19622 . . . . . 6  |-  ( ( ( F `  n
) : RR --> ( 0 [,]  +oo )  /\  S  e.  RR  /\  ( S.2 `  ( F `  n
) )  <_  S
)  ->  ( S.2 `  ( F `  n
) )  e.  RR )
356336, 338, 354, 355syl3anc 1184 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  e.  RR )
357356, 341fmptd 5885 . . . 4  |-  ( ph  ->  ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) : NN --> RR )
358336ralrimiva 2781 . . . . . . . . . 10  |-  ( ph  ->  A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,]  +oo ) )
359 fveq2 5720 . . . . . . . . . . . 12  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
360359feq1d 5572 . . . . . . . . . . 11  |-  ( n  =  k  ->  (
( F `  n
) : RR --> ( 0 [,]  +oo )  <->  ( F `  k ) : RR --> ( 0 [,]  +oo ) ) )
361360cbvralv 2924 . . . . . . . . . 10  |-  ( A. n  e.  NN  ( F `  n ) : RR --> ( 0 [,] 
+oo )  <->  A. k  e.  NN  ( F `  k ) : RR --> ( 0 [,]  +oo ) )
362358, 361sylib 189 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  NN  ( F `  k ) : RR --> ( 0 [,]  +oo ) )
363 peano2nn 10004 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
n  +  1 )  e.  NN )
364 fveq2 5720 . . . . . . . . . . 11  |-  ( k  =  ( n  + 
1 )  ->  ( F `  k )  =  ( F `  ( n  +  1
) ) )
365364feq1d 5572 . . . . . . . . . 10  |-  ( k  =  ( n  + 
1 )  ->  (
( F `  k
) : RR --> ( 0 [,]  +oo )  <->  ( F `  ( n  +  1 ) ) : RR --> ( 0 [,]  +oo ) ) )
366365rspccva 3043 . . . . . . . . 9  |-  ( ( A. k  e.  NN  ( F `  k ) : RR --> ( 0 [,]  +oo )  /\  (
n  +  1 )  e.  NN )  -> 
( F `  (
n  +  1 ) ) : RR --> ( 0 [,]  +oo ) )
367362, 363, 366syl2an 464 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 ( n  + 
1 ) ) : RR --> ( 0 [,] 
+oo ) )
368 itg2le 19623 . . . . . . . 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 ) ) ) )
369336, 367, 101, 368syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.2 `  ( F `  n
) )  <_  ( S.2 `  ( F `  ( n  +  1
) ) ) )
370369ralrimiva 2781 . . . . . 6  |-  ( ph  ->  A. n  e.  NN  ( S.2 `  ( F `
 n ) )  <_  ( S.2 `  ( F `  ( n  +  1 ) ) ) )
371359fveq2d 5724 . . . . . . . . . 10  |-  ( n  =  k  ->  ( S.2 `  ( F `  n ) )  =  ( S.2 `  ( F `  k )
) )
372 fvex 5734 . . . . . . . . . 10  |-  ( S.2 `  ( F `  k
) )  e.  _V
373371, 341, 372fvmpt 5798 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  =  ( S.2 `  ( F `  k )
) )
374 peano2nn 10004 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
375 fveq2 5720 . . . . . . . . . . . 12  |-  ( n  =  ( k  +  1 )  ->  ( F `  n )  =  ( F `  ( k  +  1 ) ) )
376375fveq2d 5724 . . . . . . . . . . 11  |-  ( n  =  ( k  +  1 )  ->  ( S.2 `  ( F `  n ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
377 fvex 5734 . . . . . . . . . . 11  |-  ( S.2 `  ( F `  (
k  +  1 ) ) )  e.  _V
378376, 341, 377fvmpt 5798 . . . . . . . . . 10  |-  ( ( k  +  1 )  e.  NN  ->  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
379374, 378syl 16 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
380373, 379breq12d 4217 . . . . . . . 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 ) ) ) ) )
381380ralbiia 2729 . . . . . . 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 ) ) ) )
382 oveq1 6080 . . . . . . . . . . 11  |-  ( n  =  k  ->  (
n  +  1 )  =  ( k  +  1 ) )
383382fveq2d 5724 . . . . . . . . . 10  |-  ( n  =  k  ->  ( F `  ( n  +  1 ) )  =  ( F `  ( k  +  1 ) ) )
384383fveq2d 5724 . . . . . . . . 9  |-  ( n  =  k  ->  ( S.2 `  ( F `  ( n  +  1
) ) )  =  ( S.2 `  ( F `  ( k  +  1 ) ) ) )
385371, 384breq12d 4217 . . . . . . . 8  |-  ( n  =  k  ->  (
( S.2 `  ( F `
 n ) )  <_  ( S.2 `  ( F `  ( n  +  1 ) ) )  <->  ( S.2 `  ( F `  k )
)  <_  ( S.2 `  ( F `  (
k  +  1 ) ) ) ) )
386385cbvralv 2924 . . . . . . 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 ) ) ) )
387381, 386bitr4i 244 . . . . . 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 ) ) ) )
388370, 387sylibr 204 . . . . 5  |-  ( ph  ->  A. k  e.  NN  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) `  k
)  <_  ( (
n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  ( k  +  1 ) ) )
389388r19.21bi 2796 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  <_  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n
) ) ) `  ( k  +  1 ) ) )
390354ralrimiva 2781 . . . . 5  |-  ( ph  ->  A. n  e.  NN  ( S.2 `  ( F `
 n ) )  <_  S )
391373breq1d 4214 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) `  k
)  <_  x  <->  ( S.2 `  ( F `  k
) )  <_  x
) )
392391ralbiia 2729 . . . . . . . 8  |-  ( A. k  e.  NN  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  <_  x  <->  A. k  e.  NN  ( S.2 `  ( F `  k )
)  <_  x )
393371breq1d 4214 . . . . . . . . 9  |-  ( n  =  k  ->  (
( S.2 `  ( F `
 n ) )  <_  x  <->  ( S.2 `  ( F `  k
) )  <_  x
) )
394393cbvralv 2924 . . . . . . . 8  |-  ( A. n  e.  NN  ( S.2 `  ( F `  n ) )  <_  x 
<-> 
A. k  e.  NN  ( S.2 `  ( F `
 k ) )  <_  x )
395392, 394bitr4i 244 . . . . . . 7  |-  ( A. k  e.  NN  (
( n  e.  NN  |->  ( S.2 `  ( F `
 n ) ) ) `  k )  <_  x  <->  A. n  e.  NN  ( S.2 `  ( F `  n )
)  <_  x )
396 breq2 4208 . . . . . . . 8  |-  ( x  =  S  ->  (
( S.2 `  ( F `
 n ) )  <_  x  <->  ( S.2 `  ( F `  n
) )  <_  S
) )
397396ralbidv 2717 . . . . . . 7  |-  ( x  =  S  ->  ( A. n  e.  NN  ( S.2 `  ( F `
 n ) )  <_  x  <->  A. n  e.  NN  ( S.2 `  ( F `  n )
)  <_  S )
)
398395, 397syl5bb 249 . . . . . 6  |-  ( x  =  S  ->  ( A. k  e.  NN  ( ( n  e.  NN  |->  ( S.2 `  ( F `  n )
) ) `  k
)  <_  x  <->  A. n  e.  NN  ( S.2 `  ( F `  n )