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

Theorem itg2gt0 19063
Description: If the function  F is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
Hypotheses
Ref Expression
itg2gt0.1  |-  ( ph  ->  A  e.  dom  vol )
itg2gt0.2  |-  ( ph  ->  0  <  ( vol `  A ) )
itg2gt0.3  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
itg2gt0.4  |-  ( ph  ->  F  e. MblFn )
itg2gt0.5  |-  ( (
ph  /\  x  e.  A )  ->  0  <  ( F `  x
) )
Assertion
Ref Expression
itg2gt0  |-  ( ph  ->  0  <  ( S.2 `  F ) )
Distinct variable groups:    x, A    x, F    ph, x

Proof of Theorem itg2gt0
StepHypRef Expression
1 itg2gt0.2 . 2  |-  ( ph  ->  0  <  ( vol `  A ) )
2 itg2gt0.1 . . . . . . 7  |-  ( ph  ->  A  e.  dom  vol )
3 iccssxr 10684 . . . . . . . 8  |-  ( 0 [,]  +oo )  C_  RR*
4 volf 18836 . . . . . . . . 9  |-  vol : dom  vol --> ( 0 [,] 
+oo )
54ffvelrni 5584 . . . . . . . 8  |-  ( A  e.  dom  vol  ->  ( vol `  A )  e.  ( 0 [,] 
+oo ) )
63, 5sseldi 3139 . . . . . . 7  |-  ( A  e.  dom  vol  ->  ( vol `  A )  e.  RR* )
72, 6syl 17 . . . . . 6  |-  ( ph  ->  ( vol `  A
)  e.  RR* )
87adantr 453 . . . . 5  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol `  A )  e. 
RR* )
9 itg2gt0.3 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
10 reex 8782 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
11 fex 5669 . . . . . . . . . . . . . . . 16  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  RR  e.  _V )  ->  F  e.  _V )
129, 10, 11sylancl 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  _V )
13 cnvexg 5181 . . . . . . . . . . . . . . 15  |-  ( F  e.  _V  ->  `' F  e.  _V )
1412, 13syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  `' F  e.  _V )
15 imaexg 5000 . . . . . . . . . . . . . 14  |-  ( `' F  e.  _V  ->  ( `' F " ( ( 1  /  n ) (,)  +oo ) )  e. 
_V )
1614, 15syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' F "
( ( 1  /  n ) (,)  +oo ) )  e.  _V )
1716adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( `' F " ( ( 1  /  n ) (,)  +oo ) )  e. 
_V )
18 eqid 2256 . . . . . . . . . . . 12  |-  ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  =  ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )
1917, 18fmptd 5604 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) : NN --> _V )
20 ffn 5313 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) : NN --> _V  ->  ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  Fn  NN )
2119, 20syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  Fn  NN )
22 fniunfv 5693 . . . . . . . . . 10  |-  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  Fn  NN  ->  U_ k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  = 
U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )
2321, 22syl 17 . . . . . . . . 9  |-  ( ph  ->  U_ k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k )  =  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )
24 itg2gt0.4 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e. MblFn )
25 0re 8792 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
26 pnfxr 10408 . . . . . . . . . . . . . . . . 17  |-  +oo  e.  RR*
27 icossre 10682 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
2825, 26, 27mp2an 656 . . . . . . . . . . . . . . . 16  |-  ( 0 [,)  +oo )  C_  RR
29 fss 5321 . . . . . . . . . . . . . . . 16  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
309, 28, 29sylancl 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : RR --> RR )
31 mbfima 18935 . . . . . . . . . . . . . . 15  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " ( ( 1  /  n ) (,)  +oo ) )  e. 
dom  vol )
3224, 30, 31syl2anc 645 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' F "
( ( 1  /  n ) (,)  +oo ) )  e.  dom  vol )
3332adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( `' F " ( ( 1  /  n ) (,)  +oo ) )  e. 
dom  vol )
3433, 18fmptd 5604 . . . . . . . . . . . 12  |-  ( ph  ->  ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) : NN --> dom  vol )
35 ffvelrn 5583 . . . . . . . . . . . 12  |-  ( ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) : NN --> dom  vol  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  e. 
dom  vol )
3634, 35sylan 459 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  e. 
dom  vol )
3736ralrimiva 2599 . . . . . . . . . 10  |-  ( ph  ->  A. k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k )  e.  dom  vol )
38 iunmbl 18858 . . . . . . . . . 10  |-  ( A. k  e.  NN  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  e. 
dom  vol  ->  U_ k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  e. 
dom  vol )
3937, 38syl 17 . . . . . . . . 9  |-  ( ph  ->  U_ k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k )  e.  dom  vol )
4023, 39eqeltrrd 2331 . . . . . . . 8  |-  ( ph  ->  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  e.  dom  vol )
41 mblss 18838 . . . . . . . 8  |-  ( U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  e. 
dom  vol  ->  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) 
C_  RR )
4240, 41syl 17 . . . . . . 7  |-  ( ph  ->  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) 
C_  RR )
43 ovolcl 18785 . . . . . . 7  |-  ( U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  C_  RR  ->  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  e.  RR* )
4442, 43syl 17 . . . . . 6  |-  ( ph  ->  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  e.  RR* )
4544adantr 453 . . . . 5  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  e.  RR* )
46 0xr 8832 . . . . . 6  |-  0  e.  RR*
4746a1i 12 . . . . 5  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  0  e.  RR* )
48 mblvol 18837 . . . . . . . 8  |-  ( A  e.  dom  vol  ->  ( vol `  A )  =  ( vol * `  A ) )
492, 48syl 17 . . . . . . 7  |-  ( ph  ->  ( vol `  A
)  =  ( vol
* `  A )
)
50 mblss 18838 . . . . . . . . . . . . . . . 16  |-  ( A  e.  dom  vol  ->  A 
C_  RR )
512, 50syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  RR )
5251sselda 3141 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  RR )
53 ffvelrn 5583 . . . . . . . . . . . . . . . . 17  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo ) )
549, 53sylan 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  ( 0 [,)  +oo ) )
55 elrege0 10698 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
5654, 55sylib 190 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( F `  x )  e.  RR  /\  0  <_  ( F `  x
) ) )
5756simpld 447 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  RR )
5852, 57syldan 458 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  e.  RR )
59 itg2gt0.5 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  0  <  ( F `  x
) )
60 nnrecl 9916 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  e.  RR  /\  0  <  ( F `  x ) )  ->  E. k  e.  NN  ( 1  /  k
)  <  ( F `  x ) )
6158, 59, 60syl2anc 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  E. k  e.  NN  ( 1  / 
k )  <  ( F `  x )
)
62 ffn 5313 . . . . . . . . . . . . . . . . . 18  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
639, 62syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  Fn  RR )
6463ad2antrr 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  F  Fn  RR )
65 elpreima 5565 . . . . . . . . . . . . . . . 16  |-  ( F  Fn  RR  ->  (
x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( ( 1  / 
k ) (,)  +oo ) ) ) )
6664, 65syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( ( 1  / 
k ) (,)  +oo ) ) ) )
6752adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  x  e.  RR )
6867biantrurd 496 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
( F `  x
)  e.  ( ( 1  /  k ) (,)  +oo )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( ( 1  / 
k ) (,)  +oo ) ) ) )
69 nnrecre 9736 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR )
7069adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  k )  e.  RR )
7170rexrd 8835 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  k )  e. 
RR* )
7271adantlr 698 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
1  /  k )  e.  RR* )
73 elioopnf 10689 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  k )  e.  RR*  ->  ( ( F `  x )  e.  ( ( 1  /  k ) (,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  ( 1  /  k )  < 
( F `  x
) ) ) )
7472, 73syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
( F `  x
)  e.  ( ( 1  /  k ) (,)  +oo )  <->  ( ( F `  x )  e.  RR  /\  ( 1  /  k )  < 
( F `  x
) ) ) )
7566, 68, 743bitr2d 274 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  <->  ( ( F `  x )  e.  RR  /\  ( 1  /  k )  < 
( F `  x
) ) ) )
76 id 21 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  NN )
77 imaexg 5000 . . . . . . . . . . . . . . . . . 18  |-  ( `' F  e.  _V  ->  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
_V )
7814, 77syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' F "
( ( 1  / 
k ) (,)  +oo ) )  e.  _V )
7978adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
_V )
80 oveq2 5786 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
1  /  n )  =  ( 1  / 
k ) )
8180oveq1d 5793 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( 1  /  n
) (,)  +oo )  =  ( ( 1  / 
k ) (,)  +oo ) )
8281imaeq2d 4986 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  ( `' F " ( ( 1  /  n ) (,)  +oo ) )  =  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )
8382, 18fvmptg 5520 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
_V )  ->  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  =  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )
8476, 79, 83syl2anr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  =  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )
8584eleq2d 2323 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  <->  x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) )
8658adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  ( F `  x )  e.  RR )
8786biantrurd 496 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
( 1  /  k
)  <  ( F `  x )  <->  ( ( F `  x )  e.  RR  /\  ( 1  /  k )  < 
( F `  x
) ) ) )
8875, 85, 873bitr4rd 279 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  NN )  ->  (
( 1  /  k
)  <  ( F `  x )  <->  x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k ) ) )
8988rexbidva 2533 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( E. k  e.  NN  ( 1  /  k
)  <  ( F `  x )  <->  E. k  e.  NN  x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) ) )
9061, 89mpbid 203 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  E. k  e.  NN  x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )
9190ex 425 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  A  ->  E. k  e.  NN  x  e.  ( (
n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) ) )
92 eluni2 3791 . . . . . . . . . . 11  |-  ( x  e.  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  <->  E. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) x  e.  z )
93 eleq2 2317 . . . . . . . . . . . . 13  |-  ( z  =  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  -> 
( x  e.  z  <-> 
x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) ) )
9493rexrn 5587 . . . . . . . . . . . 12  |-  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  Fn  NN  ->  ( E. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) x  e.  z  <->  E. k  e.  NN  x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) ) )
9521, 94syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( E. z  e. 
ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) x  e.  z  <->  E. k  e.  NN  x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) ) )
9692, 95syl5bb 250 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  <->  E. k  e.  NN  x  e.  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) ) )
9791, 96sylibrd 227 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  A  ->  x  e.  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
9897ssrdv 3146 . . . . . . . 8  |-  ( ph  ->  A  C_  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )
99 ovolss 18792 . . . . . . . 8  |-  ( ( A  C_  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  /\  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) 
C_  RR )  -> 
( vol * `  A )  <_  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
10098, 42, 99syl2anc 645 . . . . . . 7  |-  ( ph  ->  ( vol * `  A )  <_  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
10149, 100eqbrtrd 4003 . . . . . 6  |-  ( ph  ->  ( vol `  A
)  <_  ( vol * `
 U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
102101adantr 453 . . . . 5  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol `  A )  <_ 
( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
103 mblvol 18837 . . . . . . . . 9  |-  ( U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  e. 
dom  vol  ->  ( vol ` 
U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  =  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
10440, 103syl 17 . . . . . . . 8  |-  ( ph  ->  ( vol `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  =  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) )
105 peano2nn 9712 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
106105adantl 454 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  NN )
107 nnrecre 9736 . . . . . . . . . . . . . . 15  |-  ( ( k  +  1 )  e.  NN  ->  (
1  /  ( k  +  1 ) )  e.  RR )
108106, 107syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  ( k  +  1 ) )  e.  RR )
109108rexrd 8835 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  ( k  +  1 ) )  e. 
RR* )
110 nnre 9707 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR )
111110adantl 454 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR )
112111lep1d 9642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  <_ 
( k  +  1 ) )
113 nngt0 9729 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  0  <  k )
114113adantl 454 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  0  < 
k )
115106nnred 9715 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  RR )
116106nngt0d 9743 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  0  < 
( k  +  1 ) )
117 lerec 9592 . . . . . . . . . . . . . . 15  |-  ( ( ( k  e.  RR  /\  0  <  k )  /\  ( ( k  +  1 )  e.  RR  /\  0  < 
( k  +  1 ) ) )  -> 
( k  <_  (
k  +  1 )  <-> 
( 1  /  (
k  +  1 ) )  <_  ( 1  /  k ) ) )
118111, 114, 115, 116, 117syl22anc 1188 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  <_  ( k  +  1 )  <->  ( 1  /  ( k  +  1 ) )  <_ 
( 1  /  k
) ) )
119112, 118mpbid 203 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  ( k  +  1 ) )  <_ 
( 1  /  k
) )
120 iooss1 10643 . . . . . . . . . . . . 13  |-  ( ( ( 1  /  (
k  +  1 ) )  e.  RR*  /\  (
1  /  ( k  +  1 ) )  <_  ( 1  / 
k ) )  -> 
( ( 1  / 
k ) (,)  +oo )  C_  ( ( 1  /  ( k  +  1 ) ) (,) 
+oo ) )
121109, 119, 120syl2anc 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1  /  k ) (,)  +oo )  C_  (
( 1  /  (
k  +  1 ) ) (,)  +oo )
)
122 imass2 5023 . . . . . . . . . . . 12  |-  ( ( ( 1  /  k
) (,)  +oo )  C_  ( ( 1  / 
( k  +  1 ) ) (,)  +oo )  ->  ( `' F " ( ( 1  / 
k ) (,)  +oo ) )  C_  ( `' F " ( ( 1  /  ( k  +  1 ) ) (,)  +oo ) ) )
123121, 122syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  C_  ( `' F " ( ( 1  /  ( k  +  1 ) ) (,)  +oo ) ) )
12476, 78, 83syl2anr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  =  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )
125 imaexg 5000 . . . . . . . . . . . . 13  |-  ( `' F  e.  _V  ->  ( `' F " ( ( 1  /  ( k  +  1 ) ) (,)  +oo ) )  e. 
_V )
12614, 125syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( ( 1  / 
( k  +  1 ) ) (,)  +oo ) )  e.  _V )
127 oveq2 5786 . . . . . . . . . . . . . . 15  |-  ( n  =  ( k  +  1 )  ->  (
1  /  n )  =  ( 1  / 
( k  +  1 ) ) )
128127oveq1d 5793 . . . . . . . . . . . . . 14  |-  ( n  =  ( k  +  1 )  ->  (
( 1  /  n
) (,)  +oo )  =  ( ( 1  / 
( k  +  1 ) ) (,)  +oo ) )
129128imaeq2d 4986 . . . . . . . . . . . . 13  |-  ( n  =  ( k  +  1 )  ->  ( `' F " ( ( 1  /  n ) (,)  +oo ) )  =  ( `' F "
( ( 1  / 
( k  +  1 ) ) (,)  +oo ) ) )
130129, 18fvmptg 5520 . . . . . . . . . . . 12  |-  ( ( ( k  +  1 )  e.  NN  /\  ( `' F " ( ( 1  /  ( k  +  1 ) ) (,)  +oo ) )  e. 
_V )  ->  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 ( k  +  1 ) )  =  ( `' F "
( ( 1  / 
( k  +  1 ) ) (,)  +oo ) ) )
131105, 126, 130syl2anr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 ( k  +  1 ) )  =  ( `' F "
( ( 1  / 
( k  +  1 ) ) (,)  +oo ) ) )
132123, 124, 1313sstr4d 3182 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  C_  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  ( k  +  1 ) ) )
133132ralrimiva 2599 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k )  C_  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 ( k  +  1 ) ) )
134 volsup 18861 . . . . . . . . 9  |-  ( ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) : NN --> dom  vol  /\ 
A. k  e.  NN  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k )  C_  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 ( k  +  1 ) ) )  ->  ( vol `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  =  sup ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  ) )
13534, 133, 134syl2anc 645 . . . . . . . 8  |-  ( ph  ->  ( vol `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  =  sup ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  ) )
136104, 135eqtr3d 2290 . . . . . . 7  |-  ( ph  ->  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  =  sup ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  ) )
137136adantr 453 . . . . . 6  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  =  sup (
( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  ) )
13878adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
_V )
13976, 138, 83syl2anr 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  0  <  ( S.2 `  F
) )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  =  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )
140139fveq2d 5448 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  0  <  ( S.2 `  F
) )  /\  k  e.  NN )  ->  ( vol `  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )  =  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) )
14146a1i 12 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  0  e.  RR* )
142 nnrecgt0 9737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  NN  ->  0  <  ( 1  /  k
) )
143142adantl 454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  NN )  ->  0  < 
( 1  /  k
) )
144 ltle 8864 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 0  e.  RR  /\  ( 1  /  k
)  e.  RR )  ->  ( 0  < 
( 1  /  k
)  ->  0  <_  ( 1  /  k ) ) )
14525, 70, 144sylancr 647 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  NN )  ->  ( 0  <  ( 1  / 
k )  ->  0  <_  ( 1  /  k
) ) )
146143, 145mpd 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  NN )  ->  0  <_ 
( 1  /  k
) )
147 elxrge0 10699 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  /  k )  e.  ( 0 [,] 
+oo )  <->  ( (
1  /  k )  e.  RR*  /\  0  <_  ( 1  /  k
) ) )
14871, 146, 147sylanbrc 648 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  k )  e.  ( 0 [,]  +oo ) )
149 0le0 9781 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <_  0
150 elxrge0 10699 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
15146, 149, 150mpbir2an 891 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  ( 0 [,]  +oo )
152 ifcl 3561 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1  /  k
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  e.  ( 0 [,] 
+oo ) )
153148, 151, 152sylancl 646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  e.  ( 0 [,] 
+oo ) )
154153adantr 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  e.  ( 0 [,] 
+oo ) )
155 eqid 2256 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) )
156154, 155fmptd 5604 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN )  ->  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
157156adantrr 700 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
158 itg2cl 19035 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) ) )  e.  RR* )
159157, 158syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) ) )  e.  RR* )
160 rexr 8831 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  x  e.  RR* )
161160anim1i 554 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
162 elrege0 10698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
163 elxrge0 10699 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
164161, 162, 1633imtr4i 259 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
165164ssriv 3145 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
166 fss 5321 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  F : RR --> ( 0 [,] 
+oo ) )
1679, 165, 166sylancl 646 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : RR --> ( 0 [,]  +oo ) )
168 itg2cl 19035 . . . . . . . . . . . . . . . . . . 19  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  F )  e. 
RR* )
169167, 168syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S.2 `  F
)  e.  RR* )
170169adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  ( S.2 `  F )  e. 
RR* )
171 0nrp 10337 . . . . . . . . . . . . . . . . . . 19  |-  -.  0  e.  RR+
172 simpr 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
0  =  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )
173124, 36eqeltrrd 2331 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  NN )  ->  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
dom  vol )
174173adantrr 700 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
dom  vol )
175174adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( `' F "
( ( 1  / 
k ) (,)  +oo ) )  e.  dom  vol )
176172, 25syl6eqelr 2345 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  e.  RR )
17770, 143elrpd 10341 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  k )  e.  RR+ )
178177adantrr 700 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
1  /  k )  e.  RR+ )
179178adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( 1  /  k
)  e.  RR+ )
180 itg2const2 19044 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' F "
( ( 1  / 
k ) (,)  +oo ) )  e.  dom  vol 
/\  ( 1  / 
k )  e.  RR+ )  ->  ( ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  e.  RR  <->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  e.  RR ) )
181175, 179, 180syl2anc 645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  e.  RR  <->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  e.  RR ) )
182176, 181mpbird 225 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  e.  RR )
183 elrege0 10698 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  /  k )  e.  ( 0 [,) 
+oo )  <->  ( (
1  /  k )  e.  RR  /\  0  <_  ( 1  /  k
) ) )
18470, 146, 183sylanbrc 648 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  /  k )  e.  ( 0 [,)  +oo ) )
185184adantrr 700 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
1  /  k )  e.  ( 0 [,) 
+oo ) )
186185adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( 1  /  k
)  e.  ( 0 [,)  +oo ) )
187 itg2const 19043 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( `' F "
( ( 1  / 
k ) (,)  +oo ) )  e.  dom  vol 
/\  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  e.  RR  /\  (
1  /  k )  e.  ( 0 [,) 
+oo ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  =  ( ( 1  /  k
)  x.  ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) ) ) )
188175, 182, 186, 187syl3anc 1187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  =  ( ( 1  /  k
)  x.  ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) ) ) )
189172, 188eqtrd 2288 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
0  =  ( ( 1  /  k )  x.  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )
190 simplrr 740 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
0  <  ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) ) )
191182, 190elrpd 10341 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  e.  RR+ )
192179, 191rpmulcld 10359 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
( ( 1  / 
k )  x.  ( vol `  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ) )  e.  RR+ )
193189, 192eqeltrd 2330 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
k  e.  NN  /\  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  /\  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )  -> 
0  e.  RR+ )
194193ex 425 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
0  =  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  ->  0  e.  RR+ ) )
195171, 194mtoi 171 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  -.  0  =  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )
196 itg2ge0 19038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  ->  0  <_  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )
197157, 196syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  0  <_  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )
198 xrleloe 10431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  e.  RR*  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) ) )  e.  RR* )  ->  ( 0  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) ) )  <->  ( 0  < 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  \/  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) ) ) )
19946, 159, 198sylancr 647 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
0  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  <->  ( 0  <  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  \/  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) ) ) )
200197, 199mpbid 203 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
0  <  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  \/  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) ) )
201200ord 368 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  ( -.  0  <  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )  ->  0  =  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) ) )
202195, 201mt3d 119 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  0  <  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) ) )
203167adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  F : RR --> ( 0 [,] 
+oo ) )
20470adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( 1  /  k
)  e.  RR )
20563adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  e.  NN )  ->  F  Fn  RR )
206205, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  NN )  ->  ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( ( 1  / 
k ) (,)  +oo ) ) ) )
207206biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( x  e.  RR  /\  ( F `  x
)  e.  ( ( 1  /  k ) (,)  +oo ) ) )
208207simpld 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  ->  x  e.  RR )
20957adantlr 698 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
210208, 209syldan 458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( F `  x
)  e.  RR )
21171adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( 1  /  k
)  e.  RR* )
212207simprd 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( F `  x
)  e.  ( ( 1  /  k ) (,)  +oo ) )
213 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( F `  x
)  e.  RR  /\  ( 1  /  k
)  <  ( F `  x ) )  -> 
( 1  /  k
)  <  ( F `  x ) )
21473, 213syl6bi 221 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  /  k )  e.  RR*  ->  ( ( F `  x )  e.  ( ( 1  /  k ) (,) 
+oo )  ->  (
1  /  k )  <  ( F `  x ) ) )
215211, 212, 214sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( 1  /  k
)  <  ( F `  x ) )
216204, 210, 215ltled 8921 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
( 1  /  k
)  <_  ( F `  x ) )
21756simprd 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  0  <_ 
( F `  x
) )
218217adantlr 698 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  ->  0  <_  ( F `  x
) )
219208, 218syldan 458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
0  <_  ( F `  x ) )
220 breq1 3986 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  /  k )  =  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 )  -> 
( ( 1  / 
k )  <_  ( F `  x )  <->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) ) )
221 breq1 3986 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  =  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 )  -> 
( 0  <_  ( F `  x )  <->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) ) )
222220, 221ifboth 3556 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 1  /  k
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) )
223216, 219, 222syl2anc 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) )
224223adantlr 698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  /\  x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  ->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 )  <_ 
( F `  x
) )
225 iffalse 3532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  =  0 )
226225adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  /\  -.  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  =  0 )
227218adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  /\  -.  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  -> 
0  <_  ( F `  x ) )
228226, 227eqbrtrd 4003 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  /\  -.  x  e.  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) )
229224, 228pm2.61dan 769 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  NN )  /\  x  e.  RR )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) )
230229ralrimiva 2599 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  A. x  e.  RR  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 )  <_ 
( F `  x
) )
231230adantrr 700 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  A. x  e.  RR  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 )  <_ 
( F `  x
) )
23210a1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  RR  e.  _V )
233 ovex 5803 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  /  k )  e. 
_V
234 c0ex 8786 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  _V
235233, 234ifex 3583 . . . . . . . . . . . . . . . . . . . . . 22  |-  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  e.  _V
236235a1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  e.  _V )
237 fvex 5458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F `
 x )  e. 
_V
238237a1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e. 
_V )
239 eqidd 2257 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) )
2409feqmptd 5495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
241232, 236, 238, 239, 240ofrfval2 6016 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) )  o R  <_  F  <->  A. x  e.  RR  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 )  <_  ( F `  x ) ) )
242241biimpar 473 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  A. x  e.  RR  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 )  <_ 
( F `  x
) )  ->  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) )  o R  <_  F )
243231, 242syldan 458 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) )  o R  <_  F )
244 itg2le 19042 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  F : RR --> ( 0 [,] 
+oo )  /\  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ,  ( 1  /  k
) ,  0 ) )  o R  <_  F )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) ) )  <_  ( S.2 `  F ) )
245157, 203, 243, 244syl3anc 1187 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) ,  ( 1  /  k ) ,  0 ) ) )  <_  ( S.2 `  F ) )
246141, 159, 170, 202, 245xrltletrd 10445 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  NN  /\  0  < 
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )  ->  0  <  ( S.2 `  F
) )
247246expr 601 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( 0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  ->  0  <  ( S.2 `  F ) ) )
248247con3d 127 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( -.  0  <  ( S.2 `  F )  ->  -.  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )
2494ffvelrni 5584 . . . . . . . . . . . . . . . . 17  |-  ( ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
dom  vol  ->  ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  e.  ( 0 [,]  +oo ) )
2503, 249sseldi 3139 . . . . . . . . . . . . . . . 16  |-  ( ( `' F " ( ( 1  /  k ) (,)  +oo ) )  e. 
dom  vol  ->  ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  e. 
RR* )
251173, 250syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol `  ( `' F "
( ( 1  / 
k ) (,)  +oo ) ) )  e. 
RR* )
252 xrlenlt 8844 . . . . . . . . . . . . . . 15  |-  ( ( ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  e.  RR*  /\  0  e.  RR* )  ->  (
( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  <_  0  <->  -.  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )
253251, 46, 252sylancl 646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) )  <_  0  <->  -.  0  <  ( vol `  ( `' F " ( ( 1  /  k ) (,)  +oo ) ) ) ) )
254248, 253sylibrd 227 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( -.  0  <  ( S.2 `  F )  ->  ( vol `  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) )  <_ 
0 ) )
255254imp 420 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN )  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol `  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) )  <_ 
0 )
256255an32s 782 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  0  <  ( S.2 `  F
) )  /\  k  e.  NN )  ->  ( vol `  ( `' F " ( ( 1  / 
k ) (,)  +oo ) ) )  <_ 
0 )
257140, 256eqbrtrd 4003 . . . . . . . . . 10  |-  ( ( ( ph  /\  -.  0  <  ( S.2 `  F
) )  /\  k  e.  NN )  ->  ( vol `  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )  <_  0 )
258257ralrimiva 2599 . . . . . . . . 9  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  A. k  e.  NN  ( vol `  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )  <_  0 )
259 fveq2 5444 . . . . . . . . . . . . 13  |-  ( z  =  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  -> 
( vol `  z
)  =  ( vol `  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k ) ) )
260259breq1d 3993 . . . . . . . . . . . 12  |-  ( z  =  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k )  -> 
( ( vol `  z
)  <_  0  <->  ( vol `  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `  k ) )  <_ 
0 ) )
261260ralrn 5588 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  Fn  NN  ->  ( A. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ( vol `  z
)  <_  0  <->  A. k  e.  NN  ( vol `  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )  <_  0 ) )
26219, 20, 2613syl 20 . . . . . . . . . 10  |-  ( ph  ->  ( A. z  e. 
ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ( vol `  z )  <_  0  <->  A. k  e.  NN  ( vol `  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )  <_  0 ) )
263262adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( A. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ( vol `  z
)  <_  0  <->  A. k  e.  NN  ( vol `  (
( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) `
 k ) )  <_  0 ) )
264258, 263mpbird 225 . . . . . . . 8  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  A. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ( vol `  z )  <_  0 )
265 ffn 5313 . . . . . . . . . 10  |-  ( vol
: dom  vol --> ( 0 [,]  +oo )  ->  vol  Fn 
dom  vol )
2664, 265ax-mp 10 . . . . . . . . 9  |-  vol  Fn  dom  vol
267 frn 5319 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) : NN --> dom  vol  ->  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  C_  dom  vol )
26834, 267syl 17 . . . . . . . . . 10  |-  ( ph  ->  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  C_  dom  vol )
269268adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) 
C_  dom  vol )
270 breq1 3986 . . . . . . . . . 10  |-  ( x  =  ( vol `  z
)  ->  ( x  <_  0  <->  ( vol `  z
)  <_  0 ) )
271270ralima 5678 . . . . . . . . 9  |-  ( ( vol  Fn  dom  vol  /\ 
ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) )  C_  dom  vol )  ->  ( A. x  e.  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) x  <_  0  <->  A. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ( vol `  z
)  <_  0 ) )
272266, 269, 271sylancr 647 . . . . . . . 8  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( A. x  e.  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) x  <_  0  <->  A. z  e.  ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ( vol `  z
)  <_  0 ) )
273264, 272mpbird 225 . . . . . . 7  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  A. x  e.  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) x  <_  0
)
274 imassrn 4999 . . . . . . . . 9  |-  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) 
C_  ran  vol
275 frn 5319 . . . . . . . . . . 11  |-  ( vol
: dom  vol --> ( 0 [,]  +oo )  ->  ran  vol  C_  ( 0 [,]  +oo ) )
2764, 275ax-mp 10 . . . . . . . . . 10  |-  ran  vol  C_  ( 0 [,]  +oo )
277276, 3sstri 3149 . . . . . . . . 9  |-  ran  vol  C_ 
RR*
278274, 277sstri 3149 . . . . . . . 8  |-  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) 
C_  RR*
279 supxrleub 10597 . . . . . . . 8  |-  ( ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  C_  RR*  /\  0  e.  RR* )  ->  ( sup ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  )  <_  0  <->  A. x  e.  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) x  <_  0
) )
280278, 46, 279mp2an 656 . . . . . . 7  |-  ( sup ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  )  <_  0  <->  A. x  e.  ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) x  <_  0
)
281273, 280sylibr 205 . . . . . 6  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  sup ( ( vol " ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) ) ,  RR* ,  <  )  <_  0 )
282137, 281eqbrtrd 4003 . . . . 5  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol * `  U. ran  (  n  e.  NN  |->  ( `' F " ( ( 1  /  n ) (,)  +oo ) ) ) )  <_  0 )
2838, 45, 47, 102, 282xrletrd 10446 . . . 4  |-  ( (
ph  /\  -.  0  <  ( S.2 `  F
) )  ->  ( vol `  A )  <_ 
0 )
284283ex 425 . . 3  |-  ( ph  ->  ( -.  0  < 
( S.2 `  F )  ->  ( vol `  A
)  <_  0 ) )
285 xrlenlt 8844 . . . 4  |-  ( ( ( vol `  A
)  e.  RR*  /\  0  e.  RR* )  ->  (
( vol `  A
)  <_  0  <->  -.  0  <  ( vol `  A
) ) )
2867, 46, 285sylancl 646 . . 3  |-  ( ph  ->  ( ( vol `  A
)  <_  0  <->  -.  0  <  ( vol `  A
) ) )
287284, 286sylibd 207 . 2  |-  ( ph  ->  ( -.  0  < 
( S.2 `  F )  ->  -.  0  <  ( vol `  A ) ) )
2881, 287mt4d 132 1  |-  ( ph  ->  0  <  ( S.2 `  F ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359    /\ wa 360    = wceq 1619    e. wcel 1621   A.wral 2516   E.wrex 2517   _Vcvv 2757    C_ wss 3113   ifcif 3525   U.cuni 3787   U_ciun 3865   class class class wbr 3983    e. cmpt 4037   `'ccnv 4646   dom cdm 4647   ran crn 4648   "cima 4650    Fn wfn 4654   -->wf 4655   ` cfv 4659  (class class class)co 5778    o Rcofr 5997   supcsup 7147   RRcr 8690   0cc0 8691   1c1 8692    + caddc 8694    x. cmul 8696    +oocpnf 8818   RR*cxr 8820    < clt 8821    <_ cle 8822    / cdiv 9377   NNcn 9700   RR+crp 10307   (,)cioo 10608   [,)cico 10610   [,]cicc 10611   vol *covol 18770   volcvol 18771  MblFncmbf 18917   S.2citg2 18919
This theorem is referenced by:  itggt0  19144
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470  ax-inf2 7296  ax-cc 8015  ax-cnex 8747  ax-resscn 8748  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-mulcom 8755  ax-addass 8756  ax-mulass 8757  ax-distr 8758  ax-i2m1 8759  ax-1ne0 8760  ax-1rid 8761  ax-rnegex 8762  ax-rrecex 8763  ax-cnre 8764  ax-pre-lttri 8765  ax-pre-lttrn 8766  ax-pre-ltadd 8767  ax-pre-mulgt0 8768  ax-pre-sup 8769  ax-addf 8770
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2521  df-rex 2522  df-reu 2523  df-rmo 2524  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-int 3823  df-iun 3867  df-disj 3954  df-br 3984  df-opab 4038  df-mpt 4039  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-se 4311  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-isom 4676  df-ov 5781  df-oprab 5782  df-mpt2 5783  df-of 5998  df-ofr 5999  df-1st 6042  df-2nd 6043  df-iota 6211  df-riota 6258  df-recs 6342  df-rdg 6377  df-1o 6433  df-2o 6434  df-oadd 6437  df-er 6614  df-map 6728  df-pm 6729  df-en 6818  df-dom 6819  df-sdom 6820  df-fin 6821  df-fi 7119  df-sup 7148  df-oi 7179  df-card 7526  df-cda 7748  df-pnf 8823  df-mnf 8824  df-xr 8825  df-ltxr 8826  df-le 8827  df-sub 8993  df-neg 8994  df-div 9378  df-n 9701  df-2 9758  df-3 9759  df-n0 9919  df-z 9978  df-uz 10184  df-q 10270  df-rp 10308  df-xneg 10405  df-xadd 10406  df-xmul 10407  df-ioo 10612  df-ico 10614  df-icc 10615  df-fz 10735  df-fzo 10823  df-fl 10877  df-seq 10999  df-exp 11057  df-hash 11290  df-cj 11535  df-re 11536  df-im 11537  df-sqr 11671  df-abs 11672  df-clim 11913  df-rlim 11914  df-sum 12110  df-rest 13275  df-topgen 13292  df-xmet 16321  df-met 16322  df-bl 16323  df-mopn 16324  df-top 16584  df-bases 16586  df-topon 16587  df-cmp 17062  df-cncf 18330  df-ovol 18772  df-vol 18773  df-mbf 18923  df-itg1 18924  df-itg2 18925  df-0p 18973
  Copyright terms: Public domain W3C validator