Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmvlelem5 Structured version   Visualization version   Unicode version

Theorem hoidmvlelem5 38539
Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvlelem5.l  |-  L  =  ( x  e.  Fin  |->  ( a  e.  ( RR  ^m  x ) ,  b  e.  ( RR  ^m  x ) 
|->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) ) )
hoidmvlelem5.f  |-  ( ph  ->  X  e.  Fin )
hoidmvlelem5.y  |-  ( ph  ->  Y  C_  X )
hoidmvlelem5.z  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
hoidmvlelem5.w  |-  W  =  ( Y  u.  { Z } )
hoidmvlelem5.a  |-  ( ph  ->  A : W --> RR )
hoidmvlelem5.b  |-  ( ph  ->  B : W --> RR )
hoidmvlelem5.c  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
hoidmvlelem5.d  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
hoidmvlelem5.i  |-  ( ph  ->  A. e  e.  ( RR  ^m  Y ) A. f  e.  ( RR  ^m  Y ) A. g  e.  ( ( RR  ^m  Y
)  ^m  NN ) A. h  e.  (
( RR  ^m  Y
)  ^m  NN )
( X_ k  e.  Y  ( ( e `  k ) [,) (
f `  k )
)  C_  U_ j  e.  NN  X_ k  e.  Y  ( ( ( g `
 j ) `  k ) [,) (
( h `  j
) `  k )
)  ->  ( e
( L `  Y
) f )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( g `  j ) ( L `
 Y ) ( h `  j ) ) ) ) ) )
hoidmvlelem5.s  |-  ( ph  -> 
X_ k  e.  W  ( ( A `  k ) [,) ( B `  k )
)  C_  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
hoidmvlelem5.n  |-  ( ph  ->  Y  =/=  (/) )
Assertion
Ref Expression
hoidmvlelem5  |-  ( ph  ->  ( A ( L `
 W ) B )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
Distinct variable groups:    A, a,
b, h, j, k, x    A, e, f, g, h, j, k    B, a, b, h, j, k, x    B, f, g    C, a, b, h, j, k, x    C, g    D, a, b, h, j, k, x    D, g    L, a, b, h, j, k, x    e, L, f, g    W, a, b, h, j, k, x    g, W    Y, a, b, h, j, k, x    e, Y, f, g    Z, a, b, h, j, k, x    g, Z    ph, a,
b, h, j, k, x
Allowed substitution hints:    ph( e, f, g)    B( e)    C( e, f)    D( e, f)    W( e, f)    X( x, e, f, g, h, j, k, a, b)    Z( e, f)

Proof of Theorem hoidmvlelem5
Dummy variables  r 
s  c  w  z  i  l  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1769 . . . . 5  |-  F/ s
ph
2 nfre1 2846 . . . . 5  |-  F/ s E. s  e.  W  ( B `  s )  <_  ( A `  s )
31, 2nfan 2031 . . . 4  |-  F/ s ( ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s
) )
4 hoidmvlelem5.l . . . 4  |-  L  =  ( x  e.  Fin  |->  ( a  e.  ( RR  ^m  x ) ,  b  e.  ( RR  ^m  x ) 
|->  if ( x  =  (/) ,  0 ,  prod_ k  e.  x  ( vol `  ( ( a `  k ) [,) (
b `  k )
) ) ) ) )
5 hoidmvlelem5.w . . . . . 6  |-  W  =  ( Y  u.  { Z } )
6 hoidmvlelem5.f . . . . . . . 8  |-  ( ph  ->  X  e.  Fin )
7 hoidmvlelem5.y . . . . . . . 8  |-  ( ph  ->  Y  C_  X )
8 ssfi 7810 . . . . . . . 8  |-  ( ( X  e.  Fin  /\  Y  C_  X )  ->  Y  e.  Fin )
96, 7, 8syl2anc 673 . . . . . . 7  |-  ( ph  ->  Y  e.  Fin )
10 snfi 7668 . . . . . . . 8  |-  { Z }  e.  Fin
1110a1i 11 . . . . . . 7  |-  ( ph  ->  { Z }  e.  Fin )
12 unfi 7856 . . . . . . 7  |-  ( ( Y  e.  Fin  /\  { Z }  e.  Fin )  ->  ( Y  u.  { Z } )  e. 
Fin )
139, 11, 12syl2anc 673 . . . . . 6  |-  ( ph  ->  ( Y  u.  { Z } )  e.  Fin )
145, 13syl5eqel 2553 . . . . 5  |-  ( ph  ->  W  e.  Fin )
1514adantr 472 . . . 4  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  W  e.  Fin )
16 hoidmvlelem5.a . . . . 5  |-  ( ph  ->  A : W --> RR )
1716adantr 472 . . . 4  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  A : W
--> RR )
18 hoidmvlelem5.b . . . . 5  |-  ( ph  ->  B : W --> RR )
1918adantr 472 . . . 4  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  B : W
--> RR )
20 simpr 468 . . . 4  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)
213, 4, 15, 17, 19, 20hoidmvval0 38527 . . 3  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  ( A
( L `  W
) B )  =  0 )
22 nnex 10637 . . . . . 6  |-  NN  e.  _V
2322a1i 11 . . . . 5  |-  ( ph  ->  NN  e.  _V )
24 icossicc 11746 . . . . . . 7  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
2514adantr 472 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  W  e. 
Fin )
26 hoidmvlelem5.c . . . . . . . . . 10  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
2726ffvelrnda 6037 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  W
) )
28 elmapi 7511 . . . . . . . . 9  |-  ( ( C `  j )  e.  ( RR  ^m  W )  ->  ( C `  j ) : W --> RR )
2927, 28syl 17 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j ) : W --> RR )
30 hoidmvlelem5.d . . . . . . . . . 10  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
3130ffvelrnda 6037 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  W
) )
32 elmapi 7511 . . . . . . . . 9  |-  ( ( D `  j )  e.  ( RR  ^m  W )  ->  ( D `  j ) : W --> RR )
3331, 32syl 17 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : W --> RR )
344, 25, 29, 33hoidmvcl 38522 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( D `  j ) )  e.  ( 0 [,) +oo ) )
3524, 34sseldi 3416 . . . . . 6  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( D `  j ) )  e.  ( 0 [,] +oo ) )
36 eqid 2471 . . . . . 6  |-  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( D `  j ) ) )  =  ( j  e.  NN  |->  ( ( C `
 j ) ( L `  W ) ( D `  j
) ) )
3735, 36fmptd 6061 . . . . 5  |-  ( ph  ->  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) : NN --> ( 0 [,] +oo ) )
3823, 37sge0ge0 38340 . . . 4  |-  ( ph  ->  0  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
3938adantr 472 . . 3  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  0  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) ) )
4021, 39eqbrtrd 4416 . 2  |-  ( (
ph  /\  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  ( A
( L `  W
) B )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
41 icossxr 11744 . . . . . . 7  |-  ( 0 [,) +oo )  C_  RR*
424, 14, 16, 18hoidmvcl 38522 . . . . . . 7  |-  ( ph  ->  ( A ( L `
 W ) B )  e.  ( 0 [,) +oo ) )
4341, 42sseldi 3416 . . . . . 6  |-  ( ph  ->  ( A ( L `
 W ) B )  e.  RR* )
4443adantr 472 . . . . 5  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ( A ( L `  W ) B )  e.  RR* )
4523, 37sge0xrcl 38341 . . . . . 6  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e. 
RR* )
4645adantr 472 . . . . 5  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR* )
47 rge0ssre 11766 . . . . . . . . 9  |-  ( 0 [,) +oo )  C_  RR
4847, 42sseldi 3416 . . . . . . . 8  |-  ( ph  ->  ( A ( L `
 W ) B )  e.  RR )
49 ltpnf 11445 . . . . . . . 8  |-  ( ( A ( L `  W ) B )  e.  RR  ->  ( A ( L `  W ) B )  < +oo )
5048, 49syl 17 . . . . . . 7  |-  ( ph  ->  ( A ( L `
 W ) B )  < +oo )
5150adantr 472 . . . . . 6  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ( A ( L `  W ) B )  < +oo )
52 id 22 . . . . . . . 8  |-  ( (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )
5352eqcomd 2477 . . . . . . 7  |-  ( (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo  -> +oo  =  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
5453adantl 473 . . . . . 6  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  -> +oo  =  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
5551, 54breqtrd 4420 . . . . 5  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ( A ( L `  W ) B )  <  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
5644, 46, 55xrltled 37574 . . . 4  |-  ( (
ph  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ( A ( L `  W ) B )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
5756adantlr 729 . . 3  |-  ( ( ( ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ( A ( L `  W ) B )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
58 simpll 768 . . . 4  |-  ( ( ( ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s ) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ph )
59 simpr 468 . . . . . 6  |-  ( (
ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)
6016ffvelrnda 6037 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  W )  ->  ( A `  s )  e.  RR )
6118ffvelrnda 6037 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  W )  ->  ( B `  s )  e.  RR )
6260, 61ltnled 9799 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  W )  ->  (
( A `  s
)  <  ( B `  s )  <->  -.  ( B `  s )  <_  ( A `  s
) ) )
6362ralbidva 2828 . . . . . . . 8  |-  ( ph  ->  ( A. s  e.  W  ( A `  s )  <  ( B `  s )  <->  A. s  e.  W  -.  ( B `  s )  <_  ( A `  s ) ) )
64 ralnex 2834 . . . . . . . . 9  |-  ( A. s  e.  W  -.  ( B `  s )  <_  ( A `  s )  <->  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)
6564a1i 11 . . . . . . . 8  |-  ( ph  ->  ( A. s  e.  W  -.  ( B `
 s )  <_ 
( A `  s
)  <->  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
) )
6663, 65bitrd 261 . . . . . . 7  |-  ( ph  ->  ( A. s  e.  W  ( A `  s )  <  ( B `  s )  <->  -. 
E. s  e.  W  ( B `  s )  <_  ( A `  s ) ) )
6766adantr 472 . . . . . 6  |-  ( (
ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  ( A. s  e.  W  ( A `  s )  <  ( B `  s
)  <->  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
) )
6859, 67mpbird 240 . . . . 5  |-  ( (
ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  A. s  e.  W  ( A `  s )  <  ( B `  s )
)
6968adantr 472 . . . 4  |-  ( ( ( ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s ) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  A. s  e.  W  ( A `  s )  <  ( B `  s )
)
70 simpr 468 . . . . . 6  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo )  ->  -.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )
7122a1i 11 . . . . . . 7  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo )  ->  NN  e.  _V )
7237adantr 472 . . . . . . 7  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo )  ->  ( j  e.  NN  |->  ( ( C `
 j ) ( L `  W ) ( D `  j
) ) ) : NN --> ( 0 [,] +oo ) )
7371, 72sge0repnf 38342 . . . . . 6  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo )  ->  ( (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR  <->  -.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo ) )
7470, 73mpbird 240 . . . . 5  |-  ( (
ph  /\  -.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  = +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
7574adantlr 729 . . . 4  |-  ( ( ( ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s ) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )
76 simpll 768 . . . . . . 7  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s )
) )
77 fveq2 5879 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  ( C `  j )  =  ( C `  i ) )
78 fveq2 5879 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  ( D `  j )  =  ( D `  i ) )
7977, 78oveq12d 6326 . . . . . . . . . . . 12  |-  ( j  =  i  ->  (
( C `  j
) ( L `  W ) ( D `
 j ) )  =  ( ( C `
 i ) ( L `  W ) ( D `  i
) ) )
8079cbvmptv 4488 . . . . . . . . . . 11  |-  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( D `  j ) ) )  =  ( i  e.  NN  |->  ( ( C `
 i ) ( L `  W ) ( D `  i
) ) )
8180fveq2i 5882 . . . . . . . . . 10  |-  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  =  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )
8281eleq1i 2540 . . . . . . . . 9  |-  ( (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR  <->  (Σ^ `  (
i  e.  NN  |->  ( ( C `  i
) ( L `  W ) ( D `
 i ) ) ) )  e.  RR )
8382biimpi 199 . . . . . . . 8  |-  ( (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR  ->  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )
8483ad2antlr 741 . . . . . . 7  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  (Σ^ `  (
i  e.  NN  |->  ( ( C `  i
) ( L `  W ) ( D `
 i ) ) ) )  e.  RR )
85 simpr 468 . . . . . . 7  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  r  e.  RR+ )
866ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  X  e.  Fin )
877ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  Y  C_  X )
88 hoidmvlelem5.n . . . . . . . . 9  |-  ( ph  ->  Y  =/=  (/) )
8988ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  Y  =/=  (/) )
90 hoidmvlelem5.z . . . . . . . . 9  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
9190ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  Z  e.  ( X  \  Y
) )
9216ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  A : W --> RR )
9318ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  B : W --> RR )
94 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( s  =  k  ->  ( A `  s )  =  ( A `  k ) )
95 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( s  =  k  ->  ( B `  s )  =  ( B `  k ) )
9694, 95breq12d 4408 . . . . . . . . . . . . 13  |-  ( s  =  k  ->  (
( A `  s
)  <  ( B `  s )  <->  ( A `  k )  <  ( B `  k )
) )
9796cbvralv 3005 . . . . . . . . . . . 12  |-  ( A. s  e.  W  ( A `  s )  <  ( B `  s
)  <->  A. k  e.  W  ( A `  k )  <  ( B `  k ) )
9897biimpi 199 . . . . . . . . . . 11  |-  ( A. s  e.  W  ( A `  s )  <  ( B `  s
)  ->  A. k  e.  W  ( A `  k )  <  ( B `  k )
)
9998adantr 472 . . . . . . . . . 10  |-  ( ( A. s  e.  W  ( A `  s )  <  ( B `  s )  /\  k  e.  W )  ->  A. k  e.  W  ( A `  k )  <  ( B `  k )
)
100 simpr 468 . . . . . . . . . 10  |-  ( ( A. s  e.  W  ( A `  s )  <  ( B `  s )  /\  k  e.  W )  ->  k  e.  W )
101 rspa 2774 . . . . . . . . . 10  |-  ( ( A. k  e.  W  ( A `  k )  <  ( B `  k )  /\  k  e.  W )  ->  ( A `  k )  <  ( B `  k
) )
10299, 100, 101syl2anc 673 . . . . . . . . 9  |-  ( ( A. s  e.  W  ( A `  s )  <  ( B `  s )  /\  k  e.  W )  ->  ( A `  k )  <  ( B `  k
) )
103102ad5ant25 1272 . . . . . . . 8  |-  ( ( ( ( ( ph  /\ 
A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  /\  k  e.  W )  ->  ( A `  k )  <  ( B `  k
) )
10426ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  C : NN --> ( RR  ^m  W ) )
10530ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  D : NN --> ( RR  ^m  W ) )
10682biimpri 211 . . . . . . . . 9  |-  ( (Σ^ `  (
i  e.  NN  |->  ( ( C `  i
) ( L `  W ) ( D `
 i ) ) ) )  e.  RR  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
107106ad2antlr 741 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )
108 fveq1 5878 . . . . . . . . . . . . 13  |-  ( d  =  c  ->  (
d `  i )  =  ( c `  i ) )
109108breq1d 4405 . . . . . . . . . . . . . 14  |-  ( d  =  c  ->  (
( d `  i
)  <_  x  <->  ( c `  i )  <_  x
) )
110109, 108ifbieq1d 3895 . . . . . . . . . . . . 13  |-  ( d  =  c  ->  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
)  =  if ( ( c `  i
)  <_  x , 
( c `  i
) ,  x ) )
111108, 110ifeq12d 3892 . . . . . . . . . . . 12  |-  ( d  =  c  ->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) )  =  if ( i  e.  Y ,  ( c `  i ) ,  if ( ( c `  i )  <_  x ,  ( c `  i ) ,  x
) ) )
112111mpteq2dv 4483 . . . . . . . . . . 11  |-  ( d  =  c  ->  (
i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) )  =  ( i  e.  W  |->  if ( i  e.  Y ,  ( c `
 i ) ,  if ( ( c `
 i )  <_  x ,  ( c `  i ) ,  x
) ) ) )
113 eleq1 2537 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  (
i  e.  Y  <->  j  e.  Y ) )
114 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  (
c `  i )  =  ( c `  j ) )
115114breq1d 4405 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  (
( c `  i
)  <_  x  <->  ( c `  j )  <_  x
) )
116115, 114ifbieq1d 3895 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  if ( ( c `  i )  <_  x ,  ( c `  i ) ,  x
)  =  if ( ( c `  j
)  <_  x , 
( c `  j
) ,  x ) )
117113, 114, 116ifbieq12d 3899 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  if ( i  e.  Y ,  ( c `  i ) ,  if ( ( c `  i )  <_  x ,  ( c `  i ) ,  x
) )  =  if ( j  e.  Y ,  ( c `  j ) ,  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
) ) )
118117cbvmptv 4488 . . . . . . . . . . . 12  |-  ( i  e.  W  |->  if ( i  e.  Y , 
( c `  i
) ,  if ( ( c `  i
)  <_  x , 
( c `  i
) ,  x ) ) )  =  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `  j ) ,  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
) ) )
119118a1i 11 . . . . . . . . . . 11  |-  ( d  =  c  ->  (
i  e.  W  |->  if ( i  e.  Y ,  ( c `  i ) ,  if ( ( c `  i )  <_  x ,  ( c `  i ) ,  x
) ) )  =  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `
 j ) ,  if ( ( c `
 j )  <_  x ,  ( c `  j ) ,  x
) ) ) )
120112, 119eqtrd 2505 . . . . . . . . . 10  |-  ( d  =  c  ->  (
i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) )  =  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `
 j ) ,  if ( ( c `
 j )  <_  x ,  ( c `  j ) ,  x
) ) ) )
121120cbvmptv 4488 . . . . . . . . 9  |-  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) ) ) )  =  ( c  e.  ( RR  ^m  W ) 
|->  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `
 j ) ,  if ( ( c `
 j )  <_  x ,  ( c `  j ) ,  x
) ) ) )
122121mpteq2i 4479 . . . . . . . 8  |-  ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) ) ) ) )  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W
)  |->  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `  j ) ,  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x ) ) ) ) )
123 eqid 2471 . . . . . . . 8  |-  ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
124 simpr 468 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  r  e.  RR+ )
125 oveq1 6315 . . . . . . . . . . 11  |-  ( w  =  z  ->  (
w  -  ( A `
 Z ) )  =  ( z  -  ( A `  Z ) ) )
126125oveq2d 6324 . . . . . . . . . 10  |-  ( w  =  z  ->  (
( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  x.  ( w  -  ( A `  Z ) ) )  =  ( ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  x.  ( z  -  ( A `  Z )
) ) )
127 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  x  ->  (
( d `  i
)  <_  w  <->  ( d `  i )  <_  x
) )
128 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  x  ->  (
d `  i )  =  ( d `  i ) )
129 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  x  ->  w  =  x )
130127, 128, 129ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  x  ->  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w
)  =  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) )
131130ifeq2d 3891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  x  ->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w
) )  =  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) )
132131mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  x  ->  (
i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w
) ) )  =  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  x ,  ( d `  i ) ,  x
) ) ) )
133132mpteq2dv 4483 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  x  ->  (
d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w
) ) ) )  =  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x ) ) ) ) )
134133cbvmptv 4488 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  w , 
( d `  i
) ,  w ) ) ) ) )  =  ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x ) ) ) ) )
135134a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( w  =  z  ->  (
w  e.  RR  |->  ( d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w
) ) ) ) )  =  ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) ) ) ) ) )
136 id 22 . . . . . . . . . . . . . . . . 17  |-  ( w  =  z  ->  w  =  z )
137135, 136fveq12d 5885 . . . . . . . . . . . . . . . 16  |-  ( w  =  z  ->  (
( w  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  w ,  ( d `  i ) ,  w
) ) ) ) ) `  w )  =  ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) ) ) ) ) `
 z ) )
138137fveq1d 5881 . . . . . . . . . . . . . . 15  |-  ( w  =  z  ->  (
( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w ) ) ) ) ) `  w ) `  ( D `  l )
)  =  ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  l ) ) )
139138oveq2d 6324 . . . . . . . . . . . . . 14  |-  ( w  =  z  ->  (
( C `  l
) ( L `  W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  w ,  ( d `  i ) ,  w
) ) ) ) ) `  w ) `
 ( D `  l ) ) )  =  ( ( C `
 l ) ( L `  W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) ) ) ) ) `
 z ) `  ( D `  l ) ) ) )
140139mpteq2dv 4483 . . . . . . . . . . . . 13  |-  ( w  =  z  ->  (
l  e.  NN  |->  ( ( C `  l
) ( L `  W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  w ,  ( d `  i ) ,  w
) ) ) ) ) `  w ) `
 ( D `  l ) ) ) )  =  ( l  e.  NN  |->  ( ( C `  l ) ( L `  W
) ( ( ( x  e.  RR  |->  ( d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  l ) ) ) ) )
141 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( l  =  j  ->  ( C `  l )  =  ( C `  j ) )
142 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( l  =  j  ->  ( D `  l )  =  ( D `  j ) )
143142fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( l  =  j  ->  (
( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x ) ) ) ) ) `  z ) `  ( D `  l )
)  =  ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  j ) ) )
144141, 143oveq12d 6326 . . . . . . . . . . . . . . 15  |-  ( l  =  j  ->  (
( C `  l
) ( L `  W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  l ) ) )  =  ( ( C `
 j ) ( L `  W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y , 
( d `  i
) ,  if ( ( d `  i
)  <_  x , 
( d `  i
) ,  x ) ) ) ) ) `
 z ) `  ( D `  j ) ) ) )
145144cbvmptv 4488 . . . . . . . . . . . . . 14  |-  ( l  e.  NN  |->  ( ( C `  l ) ( L `  W
) ( ( ( x  e.  RR  |->  ( d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  l ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( ( x  e.  RR  |->  ( d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  j ) ) ) )
146145a1i 11 . . . . . . . . . . . . 13  |-  ( w  =  z  ->  (
l  e.  NN  |->  ( ( C `  l
) ( L `  W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  l ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( ( x  e.  RR  |->  ( d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  j ) ) ) ) )
147140, 146eqtrd 2505 . . . . . . . . . . . 12  |-  ( w  =  z  ->  (
l  e.  NN  |->  ( ( C `  l
) ( L `  W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  w ,  ( d `  i ) ,  w
) ) ) ) ) `  w ) `
 ( D `  l ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( ( x  e.  RR  |->  ( d  e.  ( RR 
^m  W )  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  j ) ) ) ) )
148147fveq2d 5883 . . . . . . . . . . 11  |-  ( w  =  z  ->  (Σ^ `  (
l  e.  NN  |->  ( ( C `  l
) ( L `  W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  w ,  ( d `  i ) ,  w
) ) ) ) ) `  w ) `
 ( D `  l ) ) ) ) )  =  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W ) 
|->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `
 i ) ,  if ( ( d `
 i )  <_  x ,  ( d `  i ) ,  x
) ) ) ) ) `  z ) `
 ( D `  j ) ) ) ) ) )
149148oveq2d 6324 . . . . . . . . . 10  |-  ( w  =  z  ->  (
( 1  +  r )  x.  (Σ^ `  ( l  e.  NN  |->  ( ( C `  l ) ( L `
 W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w ) ) ) ) ) `  w ) `  ( D `  l )
) ) ) ) )  =  ( ( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x ) ) ) ) ) `  z ) `  ( D `  j )
) ) ) ) ) )
150126, 149breq12d 4408 . . . . . . . . 9  |-  ( w  =  z  ->  (
( ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  x.  ( w  -  ( A `  Z ) ) )  <_  ( ( 1  +  r )  x.  (Σ^ `  ( l  e.  NN  |->  ( ( C `  l ) ( L `
 W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w ) ) ) ) ) `  w ) `  ( D `  l )
) ) ) ) )  <->  ( ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  x.  ( z  -  ( A `  Z )
) )  <_  (
( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x ) ) ) ) ) `  z ) `  ( D `  j )
) ) ) ) ) ) )
151150cbvrabv 3030 . . . . . . . 8  |-  { w  e.  ( ( A `  Z ) [,] ( B `  Z )
)  |  ( ( ( A  |`  Y ) ( L `  Y
) ( B  |`  Y ) )  x.  ( w  -  ( A `  Z )
) )  <_  (
( 1  +  r )  x.  (Σ^ `  ( l  e.  NN  |->  ( ( C `  l ) ( L `
 W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w ) ) ) ) ) `  w ) `  ( D `  l )
) ) ) ) ) }  =  {
z  e.  ( ( A `  Z ) [,] ( B `  Z ) )  |  ( ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  x.  ( z  -  ( A `  Z ) ) )  <_  ( ( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( ( x  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  x ,  ( d `  i ) ,  x ) ) ) ) ) `  z ) `  ( D `  j )
) ) ) ) ) }
152 eqid 2471 . . . . . . . 8  |-  sup ( { w  e.  (
( A `  Z
) [,] ( B `
 Z ) )  |  ( ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  x.  ( w  -  ( A `  Z )
) )  <_  (
( 1  +  r )  x.  (Σ^ `  ( l  e.  NN  |->  ( ( C `  l ) ( L `
 W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w ) ) ) ) ) `  w ) `  ( D `  l )
) ) ) ) ) } ,  RR ,  <  )  =  sup ( { w  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  |  ( ( ( A  |`  Y )
( L `  Y
) ( B  |`  Y ) )  x.  ( w  -  ( A `  Z )
) )  <_  (
( 1  +  r )  x.  (Σ^ `  ( l  e.  NN  |->  ( ( C `  l ) ( L `
 W ) ( ( ( w  e.  RR  |->  ( d  e.  ( RR  ^m  W
)  |->  ( i  e.  W  |->  if ( i  e.  Y ,  ( d `  i ) ,  if ( ( d `  i )  <_  w ,  ( d `  i ) ,  w ) ) ) ) ) `  w ) `  ( D `  l )
) ) ) ) ) } ,  RR ,  <  )
153 hoidmvlelem5.i . . . . . . . . 9  |-  ( ph  ->  A. e  e.  ( RR  ^m  Y ) A. f  e.  ( RR  ^m  Y ) A. g  e.  ( ( RR  ^m  Y
)  ^m  NN ) A. h  e.  (
( RR  ^m  Y
)  ^m  NN )
( X_ k  e.  Y  ( ( e `  k ) [,) (
f `  k )
)  C_  U_ j  e.  NN  X_ k  e.  Y  ( ( ( g `
 j ) `  k ) [,) (
( h `  j
) `  k )
)  ->  ( e
( L `  Y
) f )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( g `  j ) ( L `
 Y ) ( h `  j ) ) ) ) ) )
154153ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  A. e  e.  ( RR  ^m  Y
) A. f  e.  ( RR  ^m  Y
) A. g  e.  ( ( RR  ^m  Y )  ^m  NN ) A. h  e.  ( ( RR  ^m  Y
)  ^m  NN )
( X_ k  e.  Y  ( ( e `  k ) [,) (
f `  k )
)  C_  U_ j  e.  NN  X_ k  e.  Y  ( ( ( g `
 j ) `  k ) [,) (
( h `  j
) `  k )
)  ->  ( e
( L `  Y
) f )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( g `  j ) ( L `
 Y ) ( h `  j ) ) ) ) ) )
155 hoidmvlelem5.s . . . . . . . . 9  |-  ( ph  -> 
X_ k  e.  W  ( ( A `  k ) [,) ( B `  k )
)  C_  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
156155ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  X_ k  e.  W  ( ( A `  k ) [,) ( B `  k
) )  C_  U_ j  e.  NN  X_ k  e.  W  ( ( ( C `
 j ) `  k ) [,) (
( D `  j
) `  k )
) )
1574, 86, 87, 89, 91, 5, 92, 93, 103, 104, 105, 107, 122, 123, 124, 151, 152, 154, 156hoidmvlelem4 38538 . . . . . . 7  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( i  e.  NN  |->  ( ( C `  i ) ( L `
 W ) ( D `  i ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  ( A ( L `  W ) B )  <_  ( ( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) ) )
15876, 84, 85, 157syl21anc 1291 . . . . . 6  |-  ( ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )  /\  r  e.  RR+ )  ->  ( A ( L `  W ) B )  <_  ( ( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) ) )
159158ralrimiva 2809 . . . . 5  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  A. r  e.  RR+  ( A ( L `  W ) B )  <_  ( ( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) ) )
160 nfv 1769 . . . . . 6  |-  F/ r ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
16143ad2antrr 740 . . . . . 6  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  ( A ( L `  W ) B )  e.  RR* )
162 0xr 9705 . . . . . . . 8  |-  0  e.  RR*
163162a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  0  e.  RR* )
164 pnfxr 11435 . . . . . . . 8  |- +oo  e.  RR*
165164a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  -> +oo  e.  RR* )
16645ad2antrr 740 . . . . . . 7  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e. 
RR* )
16738ad2antrr 740 . . . . . . 7  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  0  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) ) )
168 ltpnf 11445 . . . . . . . 8  |-  ( (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  < +oo )
169168adantl 473 . . . . . . 7  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  < +oo )
170163, 165, 166, 167, 169elicod 11710 . . . . . 6  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  ( 0 [,) +oo ) )
171160, 161, 170xralrple2 37664 . . . . 5  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  ( ( A ( L `  W
) B )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  <->  A. r  e.  RR+  ( A ( L `  W ) B )  <_  (
( 1  +  r )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) ) ) )
172159, 171mpbird 240 . . . 4  |-  ( ( ( ph  /\  A. s  e.  W  ( A `  s )  <  ( B `  s
) )  /\  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR )  ->  ( A ( L `  W ) B )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) ) )
17358, 69, 75, 172syl21anc 1291 . . 3  |-  ( ( ( ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s ) )  /\  -.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  = +oo )  ->  ( A ( L `  W ) B )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
17457, 173pm2.61dan 808 . 2  |-  ( (
ph  /\  -.  E. s  e.  W  ( B `  s )  <_  ( A `  s )
)  ->  ( A
( L `  W
) B )  <_ 
(Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
17540, 174pm2.61dan 808 1  |-  ( ph  ->  ( A ( L `
 W ) B )  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3031    \ cdif 3387    u. cun 3388    C_ wss 3390   (/)c0 3722   ifcif 3872   {csn 3959   U_ciun 4269   class class class wbr 4395    |-> cmpt 4454    |` cres 4841   -->wf 5585   ` cfv 5589  (class class class)co 6308    |-> cmpt2 6310    ^m cmap 7490   X_cixp 7540   Fincfn 7587   supcsup 7972   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560    x. cmul 9562   +oocpnf 9690   RR*cxr 9692    < clt 9693    <_ cle 9694    - cmin 9880   NNcn 10631   RR+crp 11325   [,)cico 11662   [,]cicc 11663   prod_cprod 14036   volcvol 22493  Σ^csumge0 38318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-rlim 13630  df-sum 13830  df-prod 14037  df-rest 15399  df-topgen 15420  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-top 19998  df-bases 19999  df-topon 20000  df-cmp 20479  df-ovol 22494  df-vol 22496  df-sumge0 38319
This theorem is referenced by:  hoidmvle  38540
  Copyright terms: Public domain W3C validator