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

Theorem itg1climres 21204
Description: Restricting the simple function  F to the increasing sequence  A ( n ) of measurable sets whose union is  RR yields a sequence of simple functions whose integrals approach the integral of  F. (Contributed by Mario Carneiro, 15-Aug-2014.)
Hypotheses
Ref Expression
itg1climres.1  |-  ( ph  ->  A : NN --> dom  vol )
itg1climres.2  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  ( A `  ( n  +  1 ) ) )
itg1climres.3  |-  ( ph  ->  U. ran  A  =  RR )
itg1climres.4  |-  ( ph  ->  F  e.  dom  S.1 )
itg1climres.5  |-  G  =  ( x  e.  RR  |->  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 ) )
Assertion
Ref Expression
itg1climres  |-  ( ph  ->  ( n  e.  NN  |->  ( S.1 `  G ) )  ~~>  ( S.1 `  F
) )
Distinct variable groups:    x, n, A    n, F, x    ph, n, x
Allowed substitution hints:    G( x, n)

Proof of Theorem itg1climres
Dummy variables  j 
y  z  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10908 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1zzd 10689 . . 3  |-  ( ph  ->  1  e.  ZZ )
3 itg1climres.4 . . . . 5  |-  ( ph  ->  F  e.  dom  S.1 )
4 i1frn 21167 . . . . 5  |-  ( F  e.  dom  S.1  ->  ran 
F  e.  Fin )
53, 4syl 16 . . . 4  |-  ( ph  ->  ran  F  e.  Fin )
6 difss 3495 . . . 4  |-  ( ran 
F  \  { 0 } )  C_  ran  F
7 ssfi 7545 . . . 4  |-  ( ( ran  F  e.  Fin  /\  ( ran  F  \  { 0 } ) 
C_  ran  F )  ->  ( ran  F  \  { 0 } )  e.  Fin )
85, 6, 7sylancl 662 . . 3  |-  ( ph  ->  ( ran  F  \  { 0 } )  e.  Fin )
9 1zzd 10689 . . . 4  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  1  e.  ZZ )
10 i1fima 21168 . . . . . . . . . . . 12  |-  ( F  e.  dom  S.1  ->  ( `' F " { k } )  e.  dom  vol )
113, 10syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F " { k } )  e.  dom  vol )
1211ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( `' F " { k } )  e.  dom  vol )
13 itg1climres.1 . . . . . . . . . . . 12  |-  ( ph  ->  A : NN --> dom  vol )
1413ffvelrnda 5855 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  e. 
dom  vol )
1514adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( A `  n )  e.  dom  vol )
16 inmbl 21035 . . . . . . . . . 10  |-  ( ( ( `' F " { k } )  e.  dom  vol  /\  ( A `  n )  e.  dom  vol )  ->  ( ( `' F " { k } )  i^i  ( A `  n ) )  e. 
dom  vol )
1712, 15, 16syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  (
( `' F " { k } )  i^i  ( A `  n ) )  e. 
dom  vol )
18 mblvol 21025 . . . . . . . . 9  |-  ( ( ( `' F " { k } )  i^i  ( A `  n ) )  e. 
dom  vol  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) )  =  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
1917, 18syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  =  ( vol* `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )
20 inss1 3582 . . . . . . . . . 10  |-  ( ( `' F " { k } )  i^i  ( A `  n )
)  C_  ( `' F " { k } )
2120a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  (
( `' F " { k } )  i^i  ( A `  n ) )  C_  ( `' F " { k } ) )
22 mblss 21026 . . . . . . . . . 10  |-  ( ( `' F " { k } )  e.  dom  vol 
->  ( `' F " { k } ) 
C_  RR )
2312, 22syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( `' F " { k } )  C_  RR )
24 mblvol 21025 . . . . . . . . . . 11  |-  ( ( `' F " { k } )  e.  dom  vol 
->  ( vol `  ( `' F " { k } ) )  =  ( vol* `  ( `' F " { k } ) ) )
2512, 24syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( `' F " { k } ) )  =  ( vol* `  ( `' F " { k } ) ) )
26 i1fima2sn 21170 . . . . . . . . . . . 12  |-  ( ( F  e.  dom  S.1  /\  k  e.  ( ran 
F  \  { 0 } ) )  -> 
( vol `  ( `' F " { k } ) )  e.  RR )
273, 26sylan 471 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( vol `  ( `' F " { k } ) )  e.  RR )
2827adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( `' F " { k } ) )  e.  RR )
2925, 28eqeltrrd 2518 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol* `  ( `' F " { k } ) )  e.  RR )
30 ovolsscl 20981 . . . . . . . . 9  |-  ( ( ( ( `' F " { k } )  i^i  ( A `  n ) )  C_  ( `' F " { k } )  /\  ( `' F " { k } )  C_  RR  /\  ( vol* `  ( `' F " { k } ) )  e.  RR )  ->  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  e.  RR )
3121, 23, 29, 30syl3anc 1218 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  e.  RR )
3219, 31eqeltrd 2517 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  e.  RR )
33 eqid 2443 . . . . . . 7  |-  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
3432, 33fmptd 5879 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) : NN --> RR )
35 itg1climres.2 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  ( A `  ( n  +  1 ) ) )
3635adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( A `  n )  C_  ( A `  (
n  +  1 ) ) )
37 sslin 3588 . . . . . . . . . . . 12  |-  ( ( A `  n ) 
C_  ( A `  ( n  +  1
) )  ->  (
( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) )
3836, 37syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  (
( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) )
3913adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A : NN --> dom  vol )
40 peano2nn 10346 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  (
n  +  1 )  e.  NN )
41 ffvelrn 5853 . . . . . . . . . . . . . 14  |-  ( ( A : NN --> dom  vol  /\  ( n  +  1 )  e.  NN )  ->  ( A `  ( n  +  1
) )  e.  dom  vol )
4239, 40, 41syl2an 477 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( A `  ( n  +  1 ) )  e.  dom  vol )
43 inmbl 21035 . . . . . . . . . . . . 13  |-  ( ( ( `' F " { k } )  e.  dom  vol  /\  ( A `  ( n  +  1 ) )  e.  dom  vol )  ->  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  e. 
dom  vol )
4412, 42, 43syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  (
( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  e. 
dom  vol )
45 mblss 21026 . . . . . . . . . . . 12  |-  ( ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  e. 
dom  vol  ->  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) )  C_  RR )
4644, 45syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  (
( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  C_  RR )
47 ovolss 20980 . . . . . . . . . . 11  |-  ( ( ( ( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  /\  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  C_  RR )  ->  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) ) )
4838, 46, 47syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) ) )
49 mblvol 21025 . . . . . . . . . . 11  |-  ( ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  e. 
dom  vol  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) )  =  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) ) )
5044, 49syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) )  =  ( vol* `  (
( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) ) )
5148, 19, 503brtr4d 4334 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) ) )
5251ralrimiva 2811 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A. n  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) ) )
53 fveq2 5703 . . . . . . . . . . . . . 14  |-  ( n  =  j  ->  ( A `  n )  =  ( A `  j ) )
5453ineq2d 3564 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  (
( `' F " { k } )  i^i  ( A `  n ) )  =  ( ( `' F " { k } )  i^i  ( A `  j ) ) )
5554fveq2d 5707 . . . . . . . . . . . 12  |-  ( n  =  j  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) )
56 fvex 5713 . . . . . . . . . . . 12  |-  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j ) ) )  e.  _V
5755, 33, 56fvmpt 5786 . . . . . . . . . . 11  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) )
58 peano2nn 10346 . . . . . . . . . . . 12  |-  ( j  e.  NN  ->  (
j  +  1 )  e.  NN )
59 fveq2 5703 . . . . . . . . . . . . . . 15  |-  ( n  =  ( j  +  1 )  ->  ( A `  n )  =  ( A `  ( j  +  1 ) ) )
6059ineq2d 3564 . . . . . . . . . . . . . 14  |-  ( n  =  ( j  +  1 )  ->  (
( `' F " { k } )  i^i  ( A `  n ) )  =  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )
6160fveq2d 5707 . . . . . . . . . . . . 13  |-  ( n  =  ( j  +  1 )  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
62 fvex 5713 . . . . . . . . . . . . 13  |-  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )  e.  _V
6361, 33, 62fvmpt 5786 . . . . . . . . . . . 12  |-  ( ( j  +  1 )  e.  NN  ->  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  ( j  +  1 ) )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
6458, 63syl 16 . . . . . . . . . . 11  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  ( j  +  1 ) )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
6557, 64breq12d 4317 . . . . . . . . . 10  |-  ( j  e.  NN  ->  (
( ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  ( j  +  1 ) )  <-> 
( vol `  (
( `' F " { k } )  i^i  ( A `  j ) ) )  <_  ( vol `  (
( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) ) )
6665ralbiia 2759 . . . . . . . . 9  |-  ( A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  ( j  +  1 ) )  <->  A. j  e.  NN  ( vol `  (
( `' F " { k } )  i^i  ( A `  j ) ) )  <_  ( vol `  (
( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
67 oveq1 6110 . . . . . . . . . . . . . 14  |-  ( n  =  j  ->  (
n  +  1 )  =  ( j  +  1 ) )
6867fveq2d 5707 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  ( A `  ( n  +  1 ) )  =  ( A `  ( j  +  1 ) ) )
6968ineq2d 3564 . . . . . . . . . . . 12  |-  ( n  =  j  ->  (
( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  =  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )
7069fveq2d 5707 . . . . . . . . . . 11  |-  ( n  =  j  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
7155, 70breq12d 4317 . . . . . . . . . 10  |-  ( n  =  j  ->  (
( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) )  <_  ( vol `  (
( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) )  <-> 
( vol `  (
( `' F " { k } )  i^i  ( A `  j ) ) )  <_  ( vol `  (
( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) ) )
7271cbvralv 2959 . . . . . . . . 9  |-  ( A. n  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1 ) ) ) )  <->  A. j  e.  NN  ( vol `  (
( `' F " { k } )  i^i  ( A `  j ) ) )  <_  ( vol `  (
( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
7366, 72bitr4i 252 . . . . . . . 8  |-  ( A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  ( j  +  1 ) )  <->  A. n  e.  NN  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) )  <_  ( vol `  (
( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) ) )
7452, 73sylibr 212 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A. j  e.  NN  ( ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  ( j  +  1 ) ) )
7574r19.21bi 2826 . . . . . 6  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  ( j  +  1 ) ) )
76 ovolss 20980 . . . . . . . . . . 11  |-  ( ( ( ( `' F " { k } )  i^i  ( A `  n ) )  C_  ( `' F " { k } )  /\  ( `' F " { k } )  C_  RR )  ->  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n ) ) )  <_  ( vol* `  ( `' F " { k } ) ) )
7720, 23, 76sylancr 663 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol* `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol* `  ( `' F " { k } ) ) )
7877, 19, 253brtr4d 4334 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( `' F " { k } ) ) )
7978ralrimiva 2811 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A. n  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( `' F " { k } ) ) )
8057breq1d 4314 . . . . . . . . . 10  |-  ( j  e.  NN  ->  (
( ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) )  <->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j ) ) )  <_  ( vol `  ( `' F " { k } ) ) ) )
8180ralbiia 2759 . . . . . . . . 9  |-  ( A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) )  <->  A. j  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) )  <_  ( vol `  ( `' F " { k } ) ) )
8255breq1d 4314 . . . . . . . . . 10  |-  ( n  =  j  ->  (
( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) )  <_  ( vol `  ( `' F " { k } ) )  <->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j ) ) )  <_  ( vol `  ( `' F " { k } ) ) ) )
8382cbvralv 2959 . . . . . . . . 9  |-  ( A. n  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( `' F " { k } ) )  <->  A. j  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) )  <_  ( vol `  ( `' F " { k } ) ) )
8481, 83bitr4i 252 . . . . . . . 8  |-  ( A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) )  <->  A. n  e.  NN  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) )  <_  ( vol `  ( `' F " { k } ) ) )
8579, 84sylibr 212 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A. j  e.  NN  ( ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) ) )
86 breq2 4308 . . . . . . . . 9  |-  ( x  =  ( vol `  ( `' F " { k } ) )  -> 
( ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  x  <->  ( (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) ) ) )
8786ralbidv 2747 . . . . . . . 8  |-  ( x  =  ( vol `  ( `' F " { k } ) )  -> 
( A. j  e.  NN  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  x  <->  A. j  e.  NN  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) ) ) )
8887rspcev 3085 . . . . . . 7  |-  ( ( ( vol `  ( `' F " { k } ) )  e.  RR  /\  A. j  e.  NN  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  ( vol `  ( `' F " { k } ) ) )  ->  E. x  e.  RR  A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  x
)
8927, 85, 88syl2anc 661 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  E. x  e.  RR  A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  x
)
901, 9, 34, 75, 89climsup 13159 . . . . 5  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  ~~>  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ,  RR ,  <  )
)
91 eqid 2443 . . . . . . . 8  |-  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) )  =  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) )
9217, 91fmptd 5879 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) : NN --> dom  vol )
9338ralrimiva 2811 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A. n  e.  NN  ( ( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) )
94 fvex 5713 . . . . . . . . . . . . 13  |-  ( A `
 j )  e. 
_V
9594inex2 4446 . . . . . . . . . . . 12  |-  ( ( `' F " { k } )  i^i  ( A `  j )
)  e.  _V
9654, 91, 95fvmpt 5786 . . . . . . . . . . 11  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 j )  =  ( ( `' F " { k } )  i^i  ( A `  j ) ) )
97 fvex 5713 . . . . . . . . . . . . . 14  |-  ( A `
 ( j  +  1 ) )  e. 
_V
9897inex2 4446 . . . . . . . . . . . . 13  |-  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) )  e.  _V
9960, 91, 98fvmpt 5786 . . . . . . . . . . . 12  |-  ( ( j  +  1 )  e.  NN  ->  (
( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 ( j  +  1 ) )  =  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )
10058, 99syl 16 . . . . . . . . . . 11  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 ( j  +  1 ) )  =  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )
10196, 100sseq12d 3397 . . . . . . . . . 10  |-  ( j  e.  NN  ->  (
( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  C_  ( (
n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 ( j  +  1 ) )  <->  ( ( `' F " { k } )  i^i  ( A `  j )
)  C_  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
102101ralbiia 2759 . . . . . . . . 9  |-  ( A. j  e.  NN  (
( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 j )  C_  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  (
j  +  1 ) )  <->  A. j  e.  NN  ( ( `' F " { k } )  i^i  ( A `  j ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )
10354, 69sseq12d 3397 . . . . . . . . . 10  |-  ( n  =  j  ->  (
( ( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  <->  ( ( `' F " { k } )  i^i  ( A `  j )
)  C_  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) ) )
104103cbvralv 2959 . . . . . . . . 9  |-  ( A. n  e.  NN  (
( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) )  <->  A. j  e.  NN  ( ( `' F " { k } )  i^i  ( A `  j )
)  C_  ( ( `' F " { k } )  i^i  ( A `  ( j  +  1 ) ) ) )
105102, 104bitr4i 252 . . . . . . . 8  |-  ( A. j  e.  NN  (
( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 j )  C_  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  (
j  +  1 ) )  <->  A. n  e.  NN  ( ( `' F " { k } )  i^i  ( A `  n ) )  C_  ( ( `' F " { k } )  i^i  ( A `  ( n  +  1
) ) ) )
10693, 105sylibr 212 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  A. j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  C_  ( (
n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 ( j  +  1 ) ) )
107 volsup 21049 . . . . . . 7  |-  ( ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) : NN --> dom  vol  /\ 
A. j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  C_  ( (
n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) `
 ( j  +  1 ) ) )  ->  ( vol `  U. ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  sup (
( vol " ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) ,  RR* ,  <  ) )
10892, 106, 107syl2anc 661 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( vol `  U. ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  sup (
( vol " ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) ,  RR* ,  <  ) )
10996iuneq2i 4201 . . . . . . . . . 10  |-  U_ j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  =  U_ j  e.  NN  ( ( `' F " { k } )  i^i  ( A `  j )
)
11054cbviunv 4221 . . . . . . . . . 10  |-  U_ n  e.  NN  ( ( `' F " { k } )  i^i  ( A `  n )
)  =  U_ j  e.  NN  ( ( `' F " { k } )  i^i  ( A `  j )
)
111 iunin2 4246 . . . . . . . . . 10  |-  U_ n  e.  NN  ( ( `' F " { k } )  i^i  ( A `  n )
)  =  ( ( `' F " { k } )  i^i  U_ n  e.  NN  ( A `  n )
)
112109, 110, 1113eqtr2i 2469 . . . . . . . . 9  |-  U_ j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  =  ( ( `' F " { k } )  i^i  U_ n  e.  NN  ( A `  n )
)
113 ffn 5571 . . . . . . . . . . . . . 14  |-  ( A : NN --> dom  vol  ->  A  Fn  NN )
114 fniunfv 5976 . . . . . . . . . . . . . 14  |-  ( A  Fn  NN  ->  U_ n  e.  NN  ( A `  n )  =  U. ran  A )
11513, 113, 1143syl 20 . . . . . . . . . . . . 13  |-  ( ph  ->  U_ n  e.  NN  ( A `  n )  =  U. ran  A
)
116 itg1climres.3 . . . . . . . . . . . . 13  |-  ( ph  ->  U. ran  A  =  RR )
117115, 116eqtrd 2475 . . . . . . . . . . . 12  |-  ( ph  ->  U_ n  e.  NN  ( A `  n )  =  RR )
118117adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  U_ n  e.  NN  ( A `  n )  =  RR )
119118ineq2d 3564 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( ( `' F " { k } )  i^i  U_ n  e.  NN  ( A `  n )
)  =  ( ( `' F " { k } )  i^i  RR ) )
12011adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( `' F " { k } )  e.  dom  vol )
121120, 22syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( `' F " { k } ) 
C_  RR )
122 df-ss 3354 . . . . . . . . . . 11  |-  ( ( `' F " { k } )  C_  RR  <->  ( ( `' F " { k } )  i^i  RR )  =  ( `' F " { k } ) )
123121, 122sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( ( `' F " { k } )  i^i  RR )  =  ( `' F " { k } ) )
124119, 123eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( ( `' F " { k } )  i^i  U_ n  e.  NN  ( A `  n )
)  =  ( `' F " { k } ) )
125112, 124syl5eq 2487 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  U_ j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  =  ( `' F " { k } ) )
126 ffn 5571 . . . . . . . . 9  |-  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) : NN --> dom  vol  ->  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) )  Fn  NN )
127 fniunfv 5976 . . . . . . . . 9  |-  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) )  Fn  NN  ->  U_ j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  =  U. ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
12892, 126, 1273syl 20 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  U_ j  e.  NN  ( ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) `  j
)  =  U. ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
129125, 128eqtr3d 2477 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( `' F " { k } )  =  U. ran  (
n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
130129fveq2d 5707 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( vol `  ( `' F " { k } ) )  =  ( vol `  U. ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
131 frn 5577 . . . . . . . . 9  |-  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) : NN --> RR  ->  ran  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  C_  RR )
13234, 131syl 16 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  C_  RR )
133 fdm 5575 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) : NN --> RR  ->  dom  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  =  NN )
13434, 133syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  dom  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  NN )
135 1nn 10345 . . . . . . . . . . 11  |-  1  e.  NN
136 ne0i 3655 . . . . . . . . . . 11  |-  ( 1  e.  NN  ->  NN  =/=  (/) )
137135, 136mp1i 12 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  NN  =/=  (/) )
138134, 137eqnetrd 2638 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  dom  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  =/=  (/) )
139 dm0rn0 5068 . . . . . . . . . 10  |-  ( dom  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  =  (/) 
<->  ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  (/) )
140139necon3bii 2652 . . . . . . . . 9  |-  ( dom  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  =/=  (/) 
<->  ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  =/=  (/) )
141138, 140sylib 196 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  =/=  (/) )
142 ffn 5571 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) : NN --> RR  ->  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  Fn  NN )
143 breq1 4307 . . . . . . . . . . . 12  |-  ( z  =  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  ->  ( z  <_  x 
<->  ( ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) `  j )  <_  x ) )
144143ralrn 5858 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  Fn  NN  ->  ( A. z  e.  ran  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) z  <_  x  <->  A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  x
) )
14534, 142, 1443syl 20 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( A. z  e.  ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) z  <_  x  <->  A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  x
) )
146145rexbidv 2748 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( E. x  e.  RR  A. z  e. 
ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) z  <_  x  <->  E. x  e.  RR  A. j  e.  NN  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  <_  x
) )
14789, 146mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  E. x  e.  RR  A. z  e.  ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) z  <_  x )
148 supxrre 11302 . . . . . . . 8  |-  ( ( ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  C_  RR  /\  ran  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  =/=  (/)  /\  E. x  e.  RR  A. z  e. 
ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) z  <_  x
)  ->  sup ( ran  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) , 
RR* ,  <  )  =  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ,  RR ,  <  )
)
149132, 141, 147, 148syl3anc 1218 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) , 
RR* ,  <  )  =  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ,  RR ,  <  )
)
150 rnco2 5357 . . . . . . . . 9  |-  ran  ( vol  o.  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  =  ( vol " ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
151 eqidd 2444 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) )  =  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
152 volf 21024 . . . . . . . . . . . . 13  |-  vol : dom  vol --> ( 0 [,] +oo )
153152a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  vol : dom  vol --> ( 0 [,] +oo )
)
154153feqmptd 5756 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  vol  =  (
y  e.  dom  vol  |->  ( vol `  y ) ) )
155 fveq2 5703 . . . . . . . . . . 11  |-  ( y  =  ( ( `' F " { k } )  i^i  ( A `  n )
)  ->  ( vol `  y )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )
15617, 151, 154, 155fmptco 5888 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( vol  o.  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
157156rneqd 5079 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ran  ( vol  o.  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) )
158150, 157syl5reqr 2490 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ran  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  ( vol " ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) )
159158supeq1d 7708 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) , 
RR* ,  <  )  =  sup ( ( vol " ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) , 
RR* ,  <  ) )
160149, 159eqtr3d 2477 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ,  RR ,  <  )  =  sup ( ( vol " ran  ( n  e.  NN  |->  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) , 
RR* ,  <  ) )
161108, 130, 1603eqtr4d 2485 . . . . 5  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( vol `  ( `' F " { k } ) )  =  sup ( ran  (
n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ,  RR ,  <  )
)
16290, 161breqtrrd 4330 . . . 4  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) )  ~~>  ( vol `  ( `' F " { k } ) ) )
163 i1ff 21166 . . . . . . . 8  |-  ( F  e.  dom  S.1  ->  F : RR --> RR )
164 frn 5577 . . . . . . . 8  |-  ( F : RR --> RR  ->  ran 
F  C_  RR )
1653, 163, 1643syl 20 . . . . . . 7  |-  ( ph  ->  ran  F  C_  RR )
166165ssdifssd 3506 . . . . . 6  |-  ( ph  ->  ( ran  F  \  { 0 } ) 
C_  RR )
167166sselda 3368 . . . . 5  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  k  e.  RR )
168167recnd 9424 . . . 4  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  k  e.  CC )
169 nnex 10340 . . . . . 6  |-  NN  e.  _V
170169mptex 5960 . . . . 5  |-  ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )  e.  _V
171170a1i 11 . . . 4  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )  e.  _V )
17234ffvelrnda 5855 . . . . 5  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  e.  RR )
173172recnd 9424 . . . 4  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j )  e.  CC )
17455oveq2d 6119 . . . . . . 7  |-  ( n  =  j  ->  (
k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  =  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  j ) ) ) ) )
175 eqid 2443 . . . . . . 7  |-  ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )  =  ( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
176 ovex 6128 . . . . . . 7  |-  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  j ) ) ) )  e.  _V
177174, 175, 176fvmpt 5786 . . . . . 6  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j )  =  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) ) )
17857oveq2d 6119 . . . . . 6  |-  ( j  e.  NN  ->  (
k  x.  ( ( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j ) )  =  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) ) )
179177, 178eqtr4d 2478 . . . . 5  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j )  =  ( k  x.  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j ) ) )
180179adantl 466 . . . 4  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j )  =  ( k  x.  (
( n  e.  NN  |->  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) `  j ) ) )
1811, 9, 162, 168, 171, 173, 180climmulc2 13126 . . 3  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )  ~~>  ( k  x.  ( vol `  ( `' F " { k } ) ) ) )
182169mptex 5960 . . . 4  |-  ( n  e.  NN  |->  ( S.1 `  G ) )  e. 
_V
183182a1i 11 . . 3  |-  ( ph  ->  ( n  e.  NN  |->  ( S.1 `  G ) )  e.  _V )
184167adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  k  e.  RR )
185184, 32remulcld 9426 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  n  e.  NN )  ->  (
k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )  e.  RR )
186185, 175fmptd 5879 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ran  F  \  {
0 } ) )  ->  ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) ) : NN --> RR )
187186ffvelrnda 5855 . . . . 5  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j )  e.  RR )
188187recnd 9424 . . . 4  |-  ( ( ( ph  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j )  e.  CC )
189188anasss 647 . . 3  |-  ( (
ph  /\  ( k  e.  ( ran  F  \  { 0 } )  /\  j  e.  NN ) )  ->  (
( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j )  e.  CC )
1903adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  F  e. 
dom  S.1 )
191 itg1climres.5 . . . . . . . . . 10  |-  G  =  ( x  e.  RR  |->  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 ) )
192191i1fres 21195 . . . . . . . . 9  |-  ( ( F  e.  dom  S.1  /\  ( A `  n
)  e.  dom  vol )  ->  G  e.  dom  S.1 )
193190, 14, 192syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  G  e. 
dom  S.1 )
1948adantr 465 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ran 
F  \  { 0 } )  e.  Fin )
195 ffn 5571 . . . . . . . . . . . . . 14  |-  ( F : RR --> RR  ->  F  Fn  RR )
1963, 163, 1953syl 20 . . . . . . . . . . . . 13  |-  ( ph  ->  F  Fn  RR )
197196adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  F  Fn  RR )
198 fnfvelrn 5852 . . . . . . . . . . . 12  |-  ( ( F  Fn  RR  /\  x  e.  RR )  ->  ( F `  x
)  e.  ran  F
)
199197, 198sylan 471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  x )  e.  ran  F )
200 i1f0rn 21172 . . . . . . . . . . . . 13  |-  ( F  e.  dom  S.1  ->  0  e.  ran  F )
2013, 200syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  0  e.  ran  F
)
202201ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  0  e.  ran  F )
203 ifcl 3843 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  e.  ran  F  /\  0  e.  ran  F )  ->  if (
x  e.  ( A `
 n ) ,  ( F `  x
) ,  0 )  e.  ran  F )
204199, 202, 203syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  e.  ran  F
)
205204, 191fmptd 5879 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  G : RR
--> ran  F )
206 frn 5577 . . . . . . . . 9  |-  ( G : RR --> ran  F  ->  ran  G  C_  ran  F )
207 ssdif 3503 . . . . . . . . 9  |-  ( ran 
G  C_  ran  F  -> 
( ran  G  \  {
0 } )  C_  ( ran  F  \  {
0 } ) )
208205, 206, 2073syl 20 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ran 
G  \  { 0 } )  C_  ( ran  F  \  { 0 } ) )
209165adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ran  F  C_  RR )
210209ssdifd 3504 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ran 
F  \  { 0 } )  C_  ( RR  \  { 0 } ) )
211 itg1val2 21174 . . . . . . . 8  |-  ( ( G  e.  dom  S.1  /\  ( ( ran  F  \  { 0 } )  e.  Fin  /\  ( ran  G  \  { 0 } )  C_  ( ran  F  \  { 0 } )  /\  ( ran  F  \  { 0 } )  C_  ( RR  \  { 0 } ) ) )  -> 
( S.1 `  G )  =  sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( `' G " { k } ) ) ) )
212193, 194, 208, 210, 211syl13anc 1220 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.1 `  G )  =  sum_ k  e.  ( ran  F 
\  { 0 } ) ( k  x.  ( vol `  ( `' G " { k } ) ) ) )
213 fvex 5713 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F `
 x )  e. 
_V
214 c0ex 9392 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  _V
215213, 214ifex 3870 . . . . . . . . . . . . . . . . . . . 20  |-  if ( x  e.  ( A `
 n ) ,  ( F `  x
) ,  0 )  e.  _V
216191fvmpt2 5793 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  e.  _V )  ->  ( G `  x
)  =  if ( x  e.  ( A `
 n ) ,  ( F `  x
) ,  0 ) )
217215, 216mpan2 671 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  ( G `  x )  =  if ( x  e.  ( A `  n
) ,  ( F `
 x ) ,  0 ) )
218217adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( G `  x
)  =  if ( x  e.  ( A `
 n ) ,  ( F `  x
) ,  0 ) )
219218eqeq1d 2451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( G `  x )  =  k  <-> 
if ( x  e.  ( A `  n
) ,  ( F `
 x ) ,  0 )  =  k ) )
220 eldifsni 4013 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ( ran  F  \  { 0 } )  ->  k  =/=  0
)
221220ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  k  =/=  0 )
222 neeq1 2628 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k  -> 
( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =/=  0  <->  k  =/=  0
) )
223221, 222syl5ibrcom 222 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k  ->  if (
x  e.  ( A `
 n ) ,  ( F `  x
) ,  0 )  =/=  0 ) )
224 iffalse 3811 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  x  e.  ( A `
 n )  ->  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  0 )
225224necon1ai 2665 . . . . . . . . . . . . . . . . . . 19  |-  ( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =/=  0  ->  x  e.  ( A `  n ) )
226223, 225syl6 33 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k  ->  x  e.  ( A `  n ) ) )
227226pm4.71rd 635 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k  <->  ( x  e.  ( A `  n
)  /\  if (
x  e.  ( A `
 n ) ,  ( F `  x
) ,  0 )  =  k ) ) )
228219, 227bitrd 253 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( G `  x )  =  k  <-> 
( x  e.  ( A `  n )  /\  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k ) ) )
229 iftrue 3809 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( A `  n )  ->  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
230229eqeq1d 2451 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A `  n )  ->  ( if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k  <->  ( F `  x )  =  k ) )
231230pm5.32i 637 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( A `
 n )  /\  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k )  <-> 
( x  e.  ( A `  n )  /\  ( F `  x )  =  k ) )
232 ancom 450 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( A `
 n )  /\  ( F `  x )  =  k )  <->  ( ( F `  x )  =  k  /\  x  e.  ( A `  n
) ) )
233231, 232bitri 249 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( A `
 n )  /\  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 )  =  k )  <-> 
( ( F `  x )  =  k  /\  x  e.  ( A `  n ) ) )
234228, 233syl6bb 261 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( G `  x )  =  k  <-> 
( ( F `  x )  =  k  /\  x  e.  ( A `  n ) ) ) )
235234pm5.32da 641 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( (
x  e.  RR  /\  ( G `  x )  =  k )  <->  ( x  e.  RR  /\  ( ( F `  x )  =  k  /\  x  e.  ( A `  n
) ) ) ) )
236 anass 649 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  RR  /\  ( F `  x
)  =  k )  /\  x  e.  ( A `  n ) )  <->  ( x  e.  RR  /\  ( ( F `  x )  =  k  /\  x  e.  ( A `  n
) ) ) )
237235, 236syl6bbr 263 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( (
x  e.  RR  /\  ( G `  x )  =  k )  <->  ( (
x  e.  RR  /\  ( F `  x )  =  k )  /\  x  e.  ( A `  n ) ) ) )
238 i1ff 21166 . . . . . . . . . . . . . . . 16  |-  ( G  e.  dom  S.1  ->  G : RR --> RR )
239 ffn 5571 . . . . . . . . . . . . . . . 16  |-  ( G : RR --> RR  ->  G  Fn  RR )
240193, 238, 2393syl 20 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  G  Fn  RR )
241240adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  G  Fn  RR )
242 fniniseg 5836 . . . . . . . . . . . . . 14  |-  ( G  Fn  RR  ->  (
x  e.  ( `' G " { k } )  <->  ( x  e.  RR  /\  ( G `
 x )  =  k ) ) )
243241, 242syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( x  e.  ( `' G " { k } )  <-> 
( x  e.  RR  /\  ( G `  x
)  =  k ) ) )
244 elin 3551 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( `' F " { k } )  i^i  ( A `  n )
)  <->  ( x  e.  ( `' F " { k } )  /\  x  e.  ( A `  n ) ) )
245197adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  F  Fn  RR )
246 fniniseg 5836 . . . . . . . . . . . . . . . 16  |-  ( F  Fn  RR  ->  (
x  e.  ( `' F " { k } )  <->  ( x  e.  RR  /\  ( F `
 x )  =  k ) ) )
247245, 246syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( x  e.  ( `' F " { k } )  <-> 
( x  e.  RR  /\  ( F `  x
)  =  k ) ) )
248247anbi1d 704 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( (
x  e.  ( `' F " { k } )  /\  x  e.  ( A `  n
) )  <->  ( (
x  e.  RR  /\  ( F `  x )  =  k )  /\  x  e.  ( A `  n ) ) ) )
249244, 248syl5bb 257 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( x  e.  ( ( `' F " { k } )  i^i  ( A `  n ) )  <->  ( (
x  e.  RR  /\  ( F `  x )  =  k )  /\  x  e.  ( A `  n ) ) ) )
250237, 243, 2493bitr4d 285 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( x  e.  ( `' G " { k } )  <-> 
x  e.  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )
251250alrimiv 1685 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  A. x
( x  e.  ( `' G " { k } )  <->  x  e.  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
252 nfmpt1 4393 . . . . . . . . . . . . . . 15  |-  F/_ x
( x  e.  RR  |->  if ( x  e.  ( A `  n ) ,  ( F `  x ) ,  0 ) )
253191, 252nfcxfr 2587 . . . . . . . . . . . . . 14  |-  F/_ x G
254253nfcnv 5030 . . . . . . . . . . . . 13  |-  F/_ x `' G
255 nfcv 2589 . . . . . . . . . . . . 13  |-  F/_ x { k }
256254, 255nfima 5189 . . . . . . . . . . . 12  |-  F/_ x
( `' G " { k } )
257 nfcv 2589 . . . . . . . . . . . 12  |-  F/_ x
( ( `' F " { k } )  i^i  ( A `  n ) )
258256, 257cleqf 2615 . . . . . . . . . . 11  |-  ( ( `' G " { k } )  =  ( ( `' F " { k } )  i^i  ( A `  n ) )  <->  A. x
( x  e.  ( `' G " { k } )  <->  x  e.  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
259251, 258sylibr 212 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( `' G " { k } )  =  ( ( `' F " { k } )  i^i  ( A `  n )
) )
260259fveq2d 5707 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( vol `  ( `' G " { k } ) )  =  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) )
261260oveq2d 6119 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( k  x.  ( vol `  ( `' G " { k } ) ) )  =  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
262261sumeq2dv 13192 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( `' G " { k } ) ) )  =  sum_ k  e.  ( ran  F 
\  { 0 } ) ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
263212, 262eqtrd 2475 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( S.1 `  G )  =  sum_ k  e.  ( ran  F 
\  { 0 } ) ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
264263mpteq2dva 4390 . . . . 5  |-  ( ph  ->  ( n  e.  NN  |->  ( S.1 `  G ) )  =  ( n  e.  NN  |->  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) )
265264fveq1d 5705 . . . 4  |-  ( ph  ->  ( ( n  e.  NN  |->  ( S.1 `  G
) ) `  j
)  =  ( ( n  e.  NN  |->  sum_ k  e.  ( ran 
F  \  { 0 } ) ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) ) `  j
) )
266174sumeq2sdv 13193 . . . . . 6  |-  ( n  =  j  ->  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) )  = 
sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j ) ) ) ) )
267 eqid 2443 . . . . . 6  |-  ( n  e.  NN  |->  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) )  =  ( n  e.  NN  |->  sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n ) ) ) ) )
268 sumex 13177 . . . . . 6  |-  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) )  e. 
_V
269266, 267, 268fvmpt 5786 . . . . 5  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  sum_ k  e.  ( ran 
F  \  { 0 } ) ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) ) `  j
)  =  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) ) )
270177sumeq2sdv 13193 . . . . 5  |-  ( j  e.  NN  ->  sum_ k  e.  ( ran  F  \  { 0 } ) ( ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) ) `  j
)  =  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  j )
) ) ) )
271269, 270eqtr4d 2478 . . . 4  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  sum_ k  e.  ( ran 
F  \  { 0 } ) ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) ) `  j
)  =  sum_ k  e.  ( ran  F  \  { 0 } ) ( ( n  e.  NN  |->  ( k  x.  ( vol `  (
( `' F " { k } )  i^i  ( A `  n ) ) ) ) ) `  j
) )
272265, 271sylan9eq 2495 . . 3  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( n  e.  NN  |->  ( S.1 `  G ) ) `  j )  =  sum_ k  e.  ( ran  F  \  {
0 } ) ( ( n  e.  NN  |->  ( k  x.  ( vol `  ( ( `' F " { k } )  i^i  ( A `  n )
) ) ) ) `
 j ) )
2731, 2, 8, 181, 183, 189, 272climfsum 13295 . 2  |-  ( ph  ->  ( n  e.  NN  |->  ( S.1 `  G ) )  ~~>  sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( `' F " { k } ) ) ) )
274 itg1val 21173 . . 3  |-  ( F  e.  dom  S.1  ->  ( S.1 `  F )  =  sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( `' F " { k } ) ) ) )
2753, 274syl 16 . 2  |-  ( ph  ->  ( S.1 `  F
)  =  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( `' F " { k } ) ) ) )
276273, 275breqtrrd 4330 1  |-  ( ph  ->  ( n  e.  NN  |->  ( S.1 `  G ) )  ~~>  ( S.1 `  F
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756    =/= wne 2618   A.wral 2727   E.wrex 2728   _Vcvv 2984    \ cdif 3337    i^i cin 3339    C_ wss 3340   (/)c0 3649   ifcif 3803   {csn 3889   U.cuni 4103   U_ciun 4183   class class class wbr 4304    e. cmpt 4362   `'ccnv 4851   dom cdm 4852   ran crn 4853   "cima 4855    o. ccom 4856    Fn wfn 5425   -->wf 5426   ` cfv 5430  (class class class)co 6103   Fincfn 7322   supcsup 7702   CCcc 9292   RRcr 9293   0cc0 9294   1c1 9295    + caddc 9297    x. cmul 9299   +oocpnf 9427   RR*cxr 9429    < clt 9430    <_ cle 9431   NNcn 10334   [,]cicc 11315    ~~> cli 12974   sum_csu 13175   vol*covol 20958   volcvol 20959   S.1citg1 21107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-inf2 7859  ax-cc 8616  ax-cnex 9350  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371  ax-pre-sup 9372  ax-addf 9373
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rmo 2735  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-int 4141  df-iun 4185  df-disj 4275  df-br 4305  df-opab 4363  df-mpt 4364  df-tr 4398  df-eprel 4644  df-id 4648  df-po 4653  df-so 4654  df-fr 4691  df-se 4692  df-we 4693  df-ord 4734  df-on 4735  df-lim 4736  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-isom 5439  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-of 6332  df-om 6489  df-1st 6589  df-2nd 6590  df-recs 6844  df-rdg 6878  df-1o 6932  df-2o 6933  df-oadd 6936  df-er 7113  df-map 7228  df-pm 7229  df-en 7323  df-dom 7324  df-sdom 7325  df-fin 7326  df-fi 7673  df-sup 7703  df-oi 7736  df-card 8121  df-cda 8349  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610  df-div 10006  df-nn 10335  df-2 10392  df-3 10393  df-n0 10592  df-z 10659  df-uz 10874  df-q 10966  df-rp 11004  df-xneg 11101  df-xadd 11102  df-xmul 11103  df-ioo 11316  df-ico 11318  df-icc 11319  df-fz 11450  df-fzo 11561  df-fl 11654  df-seq 11819  df-exp 11878  df-hash 12116  df-cj 12600  df-re 12601  df-im 12602  df-sqr 12736  df-abs 12737  df-clim 12978  df-rlim 12979  df-sum 13176  df-rest 14373  df-topgen 14394  df-psmet 17821  df-xmet 17822  df-met 17823  df-bl 17824  df-mopn 17825  df-top 18515  df-bases 18517  df-topon 18518  df-cmp 19002  df-ovol 20960  df-vol 20961  df-mbf 21111  df-itg1 21112
This theorem is referenced by:  itg2monolem1  21240
  Copyright terms: Public domain W3C validator