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

Theorem hoidmvlelem2 38536
Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvlelem2.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 )
) ) ) ) )
hoidmvlelem2.x  |-  ( ph  ->  X  e.  Fin )
hoidmvlelem2.y  |-  ( ph  ->  Y  C_  X )
hoidmvlelem2.z  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
hoidmvlelem2.w  |-  W  =  ( Y  u.  { Z } )
hoidmvlelem2.a  |-  ( ph  ->  A : W --> RR )
hoidmvlelem2.b  |-  ( ph  ->  B : W --> RR )
hoidmvlelem2.c  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
hoidmvlelem2.f  |-  F  =  ( y  e.  Y  |->  0 )
hoidmvlelem2.j  |-  J  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) )
hoidmvlelem2.d  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
hoidmvlelem2.k  |-  K  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) )
hoidmvlelem2.r  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
hoidmvlelem2.h  |-  H  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W ) 
|->  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `
 j ) ,  if ( ( c `
 j )  <_  x ,  ( c `  j ) ,  x
) ) ) ) )
hoidmvlelem2.g  |-  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
hoidmvlelem2.e  |-  ( ph  ->  E  e.  RR+ )
hoidmvlelem2.u  |-  U  =  { z  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  |  ( G  x.  ( z  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) }
hoidmvlelem2.su  |-  ( ph  ->  S  e.  U )
hoidmvlelem2.sb  |-  ( ph  ->  S  <  ( B `
 Z ) )
hoidmvlelem2.p  |-  P  =  ( j  e.  NN  |->  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
hoidmvlelem2.m  |-  ( ph  ->  M  e.  NN )
hoidmvlelem2.le  |-  ( ph  ->  G  <_  ( (
1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( P `  j
) ) )
hoidmvlelem2.O  |-  O  =  ran  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )
hoidmvlelem2.v  |-  V  =  ( { ( B `
 Z ) }  u.  O )
hoidmvlelem2.q  |-  Q  = inf ( V ,  RR ,  <  )
Assertion
Ref Expression
hoidmvlelem2  |-  ( ph  ->  E. u  e.  U  S  <  u )
Distinct variable groups:    A, a,
b, k    z, A    B, a, b, k    y, B    z, B    C, a,
b, j, k    C, i, j    z, C, j    D, a, b, j, k    D, c, j, k    D, i    y, D, j    z, D    z, E    F, a,
b, k    z, G    H, a, b, k    z, H    J, a, b, k    K, a, b, k    z, L    i, M, j    i, O    P, a, b, k, x    Q, a, b, j, k, x    Q, c, x    u, Q    z, Q    S, a, b, j, k, x    S, c    S, i, x    u, S   
z, S    u, U    x, V, y    W, a, b, j, k, x    W, c    z, W    Y, a, b, j, k, x    Y, c    y, Y    Z, c, j, k, x    i, Z    y, Z    z, Z    ph, a, b, j, k, x    ph, c    ph, i    ph, y
Allowed substitution hints:    ph( z, u)    A( x, y, u, i, j, c)    B( x, u, i, j, c)    C( x, y, u, c)    D( x, u)    P( y,
z, u, i, j, c)    Q( y, i)    S( y)    U( x, y, z, i, j, k, a, b, c)    E( x, y, u, i, j, k, a, b, c)    F( x, y, z, u, i, j, c)    G( x, y, u, i, j, k, a, b, c)    H( x, y, u, i, j, c)    J( x, y, z, u, i, j, c)    K( x, y, z, u, i, j, c)    L( x, y, u, i, j, k, a, b, c)    M( x, y, z, u, k, a, b, c)    O( x, y, z, u, j, k, a, b, c)    V( z, u, i, j, k, a, b, c)    W( y, u, i)    X( x, y, z, u, i, j, k, a, b, c)    Y( z, u, i)    Z( u, a, b)

Proof of Theorem hoidmvlelem2
Dummy variable  l is distinct from all other variables.
StepHypRef Expression
1 hoidmvlelem2.a . . . . . . 7  |-  ( ph  ->  A : W --> RR )
2 hoidmvlelem2.z . . . . . . . . . 10  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
3 snidg 3986 . . . . . . . . . 10  |-  ( Z  e.  ( X  \  Y )  ->  Z  e.  { Z } )
42, 3syl 17 . . . . . . . . 9  |-  ( ph  ->  Z  e.  { Z } )
5 elun2 3593 . . . . . . . . 9  |-  ( Z  e.  { Z }  ->  Z  e.  ( Y  u.  { Z }
) )
64, 5syl 17 . . . . . . . 8  |-  ( ph  ->  Z  e.  ( Y  u.  { Z }
) )
7 hoidmvlelem2.w . . . . . . . 8  |-  W  =  ( Y  u.  { Z } )
86, 7syl6eleqr 2560 . . . . . . 7  |-  ( ph  ->  Z  e.  W )
91, 8ffvelrnd 6038 . . . . . 6  |-  ( ph  ->  ( A `  Z
)  e.  RR )
10 hoidmvlelem2.b . . . . . . 7  |-  ( ph  ->  B : W --> RR )
1110, 8ffvelrnd 6038 . . . . . 6  |-  ( ph  ->  ( B `  Z
)  e.  RR )
12 hoidmvlelem2.v . . . . . . . 8  |-  V  =  ( { ( B `
 Z ) }  u.  O )
1311snssd 4108 . . . . . . . . 9  |-  ( ph  ->  { ( B `  Z ) }  C_  RR )
14 hoidmvlelem2.O . . . . . . . . . 10  |-  O  =  ran  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )
15 nfv 1769 . . . . . . . . . . 11  |-  F/ i
ph
16 eqid 2471 . . . . . . . . . . 11  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  |->  ( ( D `  i ) `
 Z ) )  =  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )
17 simpl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ph )
18 fz1ssnn 11856 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  C_  NN
19 elrabi 3181 . . . . . . . . . . . . . 14  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  i  e.  ( 1 ... M
) )
2018, 19sseldi 3416 . . . . . . . . . . . . 13  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  i  e.  NN )
2120adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  i  e.  NN )
22 eleq1 2537 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
j  e.  NN  <->  i  e.  NN ) )
2322anbi2d 718 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ph  /\  j  e.  NN )  <->  ( ph  /\  i  e.  NN ) ) )
24 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( D `  j )  =  ( D `  i ) )
2524fveq1d 5881 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( D `  j
) `  Z )  =  ( ( D `
 i ) `  Z ) )
2625eleq1d 2533 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ( D `  j ) `  Z
)  e.  RR  <->  ( ( D `  i ) `  Z )  e.  RR ) )
2723, 26imbi12d 327 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  (
( ( ph  /\  j  e.  NN )  ->  ( ( D `  j ) `  Z
)  e.  RR )  <-> 
( ( ph  /\  i  e.  NN )  ->  ( ( D `  i ) `  Z
)  e.  RR ) ) )
28 hoidmvlelem2.d . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
2928ffvelrnda 6037 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  W
) )
30 elmapi 7511 . . . . . . . . . . . . . . 15  |-  ( ( D `  j )  e.  ( RR  ^m  W )  ->  ( D `  j ) : W --> RR )
3129, 30syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : W --> RR )
328adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  Z  e.  W )
3331, 32ffvelrnd 6038 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j ) `
 Z )  e.  RR )
3427, 33chvarv 2120 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( D `  i ) `
 Z )  e.  RR )
3517, 21, 34syl2anc 673 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ( ( D `
 i ) `  Z )  e.  RR )
3615, 16, 35rnmptssd 37544 . . . . . . . . . 10  |-  ( ph  ->  ran  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )  C_  RR )
3714, 36syl5eqss 3462 . . . . . . . . 9  |-  ( ph  ->  O  C_  RR )
3813, 37unssd 3601 . . . . . . . 8  |-  ( ph  ->  ( { ( B `
 Z ) }  u.  O )  C_  RR )
3912, 38syl5eqss 3462 . . . . . . 7  |-  ( ph  ->  V  C_  RR )
40 hoidmvlelem2.q . . . . . . . 8  |-  Q  = inf ( V ,  RR ,  <  )
41 ltso 9732 . . . . . . . . . 10  |-  <  Or  RR
4241a1i 11 . . . . . . . . 9  |-  ( ph  ->  <  Or  RR )
43 snfi 7668 . . . . . . . . . . . 12  |-  { ( B `  Z ) }  e.  Fin
4443a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  { ( B `  Z ) }  e.  Fin )
45 fzfi 12223 . . . . . . . . . . . . . . 15  |-  ( 1 ... M )  e. 
Fin
46 rabfi 7814 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M )  e.  Fin  ->  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  e.  Fin )
4745, 46ax-mp 5 . . . . . . . . . . . . . 14  |-  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  e.  Fin
4847a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  e.  Fin )
4916rnmptfi 37508 . . . . . . . . . . . . 13  |-  ( { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  e.  Fin  ->  ran  ( i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )  e. 
Fin )
5048, 49syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ran  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )  e. 
Fin )
5114, 50syl5eqel 2553 . . . . . . . . . . 11  |-  ( ph  ->  O  e.  Fin )
52 unfi 7856 . . . . . . . . . . 11  |-  ( ( { ( B `  Z ) }  e.  Fin  /\  O  e.  Fin )  ->  ( { ( B `  Z ) }  u.  O )  e.  Fin )
5344, 51, 52syl2anc 673 . . . . . . . . . 10  |-  ( ph  ->  ( { ( B `
 Z ) }  u.  O )  e. 
Fin )
5412, 53syl5eqel 2553 . . . . . . . . 9  |-  ( ph  ->  V  e.  Fin )
55 fvex 5889 . . . . . . . . . . . . . 14  |-  ( B `
 Z )  e. 
_V
5655snid 3988 . . . . . . . . . . . . 13  |-  ( B `
 Z )  e. 
{ ( B `  Z ) }
57 elun1 3592 . . . . . . . . . . . . 13  |-  ( ( B `  Z )  e.  { ( B `
 Z ) }  ->  ( B `  Z )  e.  ( { ( B `  Z ) }  u.  O ) )
5856, 57ax-mp 5 . . . . . . . . . . . 12  |-  ( B `
 Z )  e.  ( { ( B `
 Z ) }  u.  O )
5912eqcomi 2480 . . . . . . . . . . . 12  |-  ( { ( B `  Z
) }  u.  O
)  =  V
6058, 59eleqtri 2547 . . . . . . . . . . 11  |-  ( B `
 Z )  e.  V
6160a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( B `  Z
)  e.  V )
62 ne0i 3728 . . . . . . . . . 10  |-  ( ( B `  Z )  e.  V  ->  V  =/=  (/) )
6361, 62syl 17 . . . . . . . . 9  |-  ( ph  ->  V  =/=  (/) )
64 fiinfcl 8035 . . . . . . . . 9  |-  ( (  <  Or  RR  /\  ( V  e.  Fin  /\  V  =/=  (/)  /\  V  C_  RR ) )  -> inf ( V ,  RR ,  <  )  e.  V )
6542, 54, 63, 39, 64syl13anc 1294 . . . . . . . 8  |-  ( ph  -> inf ( V ,  RR ,  <  )  e.  V
)
6640, 65syl5eqel 2553 . . . . . . 7  |-  ( ph  ->  Q  e.  V )
6739, 66sseldd 3419 . . . . . 6  |-  ( ph  ->  Q  e.  RR )
68 hoidmvlelem2.u . . . . . . . . . . . 12  |-  U  =  { z  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  |  ( G  x.  ( z  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) }
69 ssrab2 3500 . . . . . . . . . . . 12  |-  { z  e.  ( ( A `
 Z ) [,] ( B `  Z
) )  |  ( G  x.  ( z  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) } 
C_  ( ( A `
 Z ) [,] ( B `  Z
) )
7068, 69eqsstri 3448 . . . . . . . . . . 11  |-  U  C_  ( ( A `  Z ) [,] ( B `  Z )
)
7170a1i 11 . . . . . . . . . 10  |-  ( ph  ->  U  C_  ( ( A `  Z ) [,] ( B `  Z
) ) )
729, 11iccssred 37698 . . . . . . . . . 10  |-  ( ph  ->  ( ( A `  Z ) [,] ( B `  Z )
)  C_  RR )
7371, 72sstrd 3428 . . . . . . . . 9  |-  ( ph  ->  U  C_  RR )
74 hoidmvlelem2.su . . . . . . . . 9  |-  ( ph  ->  S  e.  U )
7573, 74sseldd 3419 . . . . . . . 8  |-  ( ph  ->  S  e.  RR )
769rexrd 9708 . . . . . . . . 9  |-  ( ph  ->  ( A `  Z
)  e.  RR* )
7711rexrd 9708 . . . . . . . . 9  |-  ( ph  ->  ( B `  Z
)  e.  RR* )
7870, 74sseldi 3416 . . . . . . . . 9  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
79 iccgelb 11716 . . . . . . . . 9  |-  ( ( ( A `  Z
)  e.  RR*  /\  ( B `  Z )  e.  RR*  /\  S  e.  ( ( A `  Z ) [,] ( B `  Z )
) )  ->  ( A `  Z )  <_  S )
8076, 77, 78, 79syl3anc 1292 . . . . . . . 8  |-  ( ph  ->  ( A `  Z
)  <_  S )
81 hoidmvlelem2.sb . . . . . . . . . . . . . . 15  |-  ( ph  ->  S  <  ( B `
 Z ) )
8281adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  ( B `  Z ) )  ->  S  <  ( B `  Z ) )
83 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( B `  Z )  ->  x  =  ( B `  Z ) )
8483eqcomd 2477 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B `  Z )  ->  ( B `  Z )  =  x )
8584adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  ( B `  Z ) )  ->  ( B `  Z )  =  x )
8682, 85breqtrd 4420 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  =  ( B `  Z ) )  ->  S  <  x )
8786adantlr 729 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  V )  /\  x  =  ( B `  Z ) )  ->  S  <  x )
88 simpll 768 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  V )  /\  -.  x  =  ( B `  Z ) )  ->  ph )
89 id 22 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  V  ->  x  e.  V )
9089, 12syl6eleq 2559 . . . . . . . . . . . . . . . 16  |-  ( x  e.  V  ->  x  e.  ( { ( B `
 Z ) }  u.  O ) )
9190adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  V  /\  -.  x  =  ( B `  Z )
)  ->  x  e.  ( { ( B `  Z ) }  u.  O ) )
92 elsni 3985 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  { ( B `
 Z ) }  ->  x  =  ( B `  Z ) )
9392con3i 142 . . . . . . . . . . . . . . . 16  |-  ( -.  x  =  ( B `
 Z )  ->  -.  x  e.  { ( B `  Z ) } )
9493adantl 473 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  V  /\  -.  x  =  ( B `  Z )
)  ->  -.  x  e.  { ( B `  Z ) } )
95 elunnel1 3566 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( { ( B `  Z
) }  u.  O
)  /\  -.  x  e.  { ( B `  Z ) } )  ->  x  e.  O
)
9691, 94, 95syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( x  e.  V  /\  -.  x  =  ( B `  Z )
)  ->  x  e.  O )
9796adantll 728 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  V )  /\  -.  x  =  ( B `  Z ) )  ->  x  e.  O )
98 id 22 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  O  ->  x  e.  O )
9998, 14syl6eleq 2559 . . . . . . . . . . . . . . . 16  |-  ( x  e.  O  ->  x  e.  ran  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) ) )
100 vex 3034 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
10116elrnmpt 5087 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  _V  ->  (
x  e.  ran  (
i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  |->  ( ( D `  i ) `
 Z ) )  <->  E. i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) } x  =  ( ( D `  i ) `  Z
) ) )
102100, 101ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ran  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  |->  ( ( D `  i ) `
 Z ) )  <->  E. i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) } x  =  ( ( D `  i ) `  Z
) )
10399, 102sylib 201 . . . . . . . . . . . . . . 15  |-  ( x  e.  O  ->  E. i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) } x  =  ( ( D `  i
) `  Z )
)
104103adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  O )  ->  E. i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) } x  =  ( ( D `  i
) `  Z )
)
105 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  i  ->  ( C `  j )  =  ( C `  i ) )
106105fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  i  ->  (
( C `  j
) `  Z )  =  ( ( C `
 i ) `  Z ) )
107106eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  i  ->  (
( ( C `  j ) `  Z
)  e.  RR  <->  ( ( C `  i ) `  Z )  e.  RR ) )
10823, 107imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  i  ->  (
( ( ph  /\  j  e.  NN )  ->  ( ( C `  j ) `  Z
)  e.  RR )  <-> 
( ( ph  /\  i  e.  NN )  ->  ( ( C `  i ) `  Z
)  e.  RR ) ) )
109 hoidmvlelem2.c . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
110109ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  W
) )
111 elmapi 7511 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( C `  j )  e.  ( RR  ^m  W )  ->  ( C `  j ) : W --> RR )
112110, 111syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j ) : W --> RR )
113112, 32ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) `
 Z )  e.  RR )
114108, 113chvarv 2120 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( C `  i ) `
 Z )  e.  RR )
115114rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( C `  i ) `
 Z )  e. 
RR* )
11617, 21, 115syl2anc 673 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ( ( C `
 i ) `  Z )  e.  RR* )
11734rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( D `  i ) `
 Z )  e. 
RR* )
11817, 21, 117syl2anc 673 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ( ( D `
 i ) `  Z )  e.  RR* )
119106, 25oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  i  ->  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) )  =  ( ( ( C `  i ) `
 Z ) [,) ( ( D `  i ) `  Z
) ) )
120119eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  i  ->  ( S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  <->  S  e.  ( ( ( C `
 i ) `  Z ) [,) (
( D `  i
) `  Z )
) ) )
121120elrab 3184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  <->  ( i  e.  ( 1 ... M
)  /\  S  e.  ( ( ( C `
 i ) `  Z ) [,) (
( D `  i
) `  Z )
) ) )
122121biimpi 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  (
i  e.  ( 1 ... M )  /\  S  e.  ( (
( C `  i
) `  Z ) [,) ( ( D `  i ) `  Z
) ) ) )
123122simprd 470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  S  e.  ( ( ( C `
 i ) `  Z ) [,) (
( D `  i
) `  Z )
) )
124123adantl 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  S  e.  ( ( ( C `  i ) `  Z
) [,) ( ( D `  i ) `
 Z ) ) )
125 icoltub 37703 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( C `  i ) `  Z
)  e.  RR*  /\  (
( D `  i
) `  Z )  e.  RR*  /\  S  e.  ( ( ( C `
 i ) `  Z ) [,) (
( D `  i
) `  Z )
) )  ->  S  <  ( ( D `  i ) `  Z
) )
126116, 118, 124, 125syl3anc 1292 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  S  <  (
( D `  i
) `  Z )
)
1271263adant3 1050 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  /\  x  =  ( ( D `  i ) `  Z ) )  ->  S  <  ( ( D `
 i ) `  Z ) )
128 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( ( D `
 i ) `  Z )  ->  x  =  ( ( D `
 i ) `  Z ) )
129128eqcomd 2477 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( ( D `
 i ) `  Z )  ->  (
( D `  i
) `  Z )  =  x )
1301293ad2ant3 1053 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  /\  x  =  ( ( D `  i ) `  Z ) )  -> 
( ( D `  i ) `  Z
)  =  x )
131127, 130breqtrd 4420 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  /\  x  =  ( ( D `  i ) `  Z ) )  ->  S  <  x )
1321313exp 1230 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( i  e.  {
j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  ->  ( x  =  ( ( D `  i ) `
 Z )  ->  S  <  x ) ) )
133132adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  O )  ->  (
i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  (
x  =  ( ( D `  i ) `
 Z )  ->  S  <  x ) ) )
134133rexlimdv 2870 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  O )  ->  ( E. i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) } x  =  ( ( D `  i ) `  Z
)  ->  S  <  x ) )
135104, 134mpd 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  O )  ->  S  <  x )
13688, 97, 135syl2anc 673 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  V )  /\  -.  x  =  ( B `  Z ) )  ->  S  <  x )
13787, 136pm2.61dan 808 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  V )  ->  S  <  x )
138137ralrimiva 2809 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  V  S  <  x )
139 breq2 4399 . . . . . . . . . . 11  |-  ( x  = inf ( V ,  RR ,  <  )  -> 
( S  <  x  <->  S  < inf ( V ,  RR ,  <  ) ) )
140139rspcva 3134 . . . . . . . . . 10  |-  ( (inf ( V ,  RR ,  <  )  e.  V  /\  A. x  e.  V  S  <  x )  ->  S  < inf ( V ,  RR ,  <  ) )
14165, 138, 140syl2anc 673 . . . . . . . . 9  |-  ( ph  ->  S  < inf ( V ,  RR ,  <  )
)
14240eqcomi 2480 . . . . . . . . . 10  |- inf ( V ,  RR ,  <  )  =  Q
143142a1i 11 . . . . . . . . 9  |-  ( ph  -> inf ( V ,  RR ,  <  )  =  Q )
144141, 143breqtrd 4420 . . . . . . . 8  |-  ( ph  ->  S  <  Q )
1459, 75, 67, 80, 144lelttrd 9810 . . . . . . 7  |-  ( ph  ->  ( A `  Z
)  <  Q )
1469, 67, 145ltled 9800 . . . . . 6  |-  ( ph  ->  ( A `  Z
)  <_  Q )
147 fiminre 10577 . . . . . . . . 9  |-  ( ( V  C_  RR  /\  V  e.  Fin  /\  V  =/=  (/) )  ->  E. x  e.  V  A. y  e.  V  x  <_  y )
14839, 54, 63, 147syl3anc 1292 . . . . . . . 8  |-  ( ph  ->  E. x  e.  V  A. y  e.  V  x  <_  y )
149 lbinfle 10585 . . . . . . . 8  |-  ( ( V  C_  RR  /\  E. x  e.  V  A. y  e.  V  x  <_  y  /\  ( B `
 Z )  e.  V )  -> inf ( V ,  RR ,  <  )  <_  ( B `  Z ) )
15039, 148, 61, 149syl3anc 1292 . . . . . . 7  |-  ( ph  -> inf ( V ,  RR ,  <  )  <_  ( B `  Z )
)
15140, 150syl5eqbr 4429 . . . . . 6  |-  ( ph  ->  Q  <_  ( B `  Z ) )
1529, 11, 67, 146, 151eliccd 37697 . . . . 5  |-  ( ph  ->  Q  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
15367recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
15475recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  S  e.  CC )
1559recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  ( A `  Z
)  e.  CC )
156153, 154, 155npncand 10029 . . . . . . . . 9  |-  ( ph  ->  ( ( Q  -  S )  +  ( S  -  ( A `
 Z ) ) )  =  ( Q  -  ( A `  Z ) ) )
157156eqcomd 2477 . . . . . . . 8  |-  ( ph  ->  ( Q  -  ( A `  Z )
)  =  ( ( Q  -  S )  +  ( S  -  ( A `  Z ) ) ) )
158157oveq2d 6324 . . . . . . 7  |-  ( ph  ->  ( G  x.  ( Q  -  ( A `  Z ) ) )  =  ( G  x.  ( ( Q  -  S )  +  ( S  -  ( A `
 Z ) ) ) ) )
159 rge0ssre 11766 . . . . . . . . . 10  |-  ( 0 [,) +oo )  C_  RR
160 hoidmvlelem2.g . . . . . . . . . . 11  |-  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
161 hoidmvlelem2.l . . . . . . . . . . . 12  |-  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 )
) ) ) ) )
162 hoidmvlelem2.x . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  Fin )
163 hoidmvlelem2.y . . . . . . . . . . . . 13  |-  ( ph  ->  Y  C_  X )
164162, 163ssfid 37473 . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  Fin )
165 ssun1 3588 . . . . . . . . . . . . . . 15  |-  Y  C_  ( Y  u.  { Z } )
166165, 7sseqtr4i 3451 . . . . . . . . . . . . . 14  |-  Y  C_  W
167166a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  C_  W )
1681, 167fssresd 5762 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  |`  Y ) : Y --> RR )
16910, 167fssresd 5762 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  |`  Y ) : Y --> RR )
170161, 164, 168, 169hoidmvcl 38522 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  ( 0 [,) +oo ) )
171160, 170syl5eqel 2553 . . . . . . . . . 10  |-  ( ph  ->  G  e.  ( 0 [,) +oo ) )
172159, 171sseldi 3416 . . . . . . . . 9  |-  ( ph  ->  G  e.  RR )
173172recnd 9687 . . . . . . . 8  |-  ( ph  ->  G  e.  CC )
174153, 154subcld 10005 . . . . . . . 8  |-  ( ph  ->  ( Q  -  S
)  e.  CC )
175154, 155subcld 10005 . . . . . . . 8  |-  ( ph  ->  ( S  -  ( A `  Z )
)  e.  CC )
176173, 174, 175adddid 9685 . . . . . . 7  |-  ( ph  ->  ( G  x.  (
( Q  -  S
)  +  ( S  -  ( A `  Z ) ) ) )  =  ( ( G  x.  ( Q  -  S ) )  +  ( G  x.  ( S  -  ( A `  Z )
) ) ) )
177173, 174mulcld 9681 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( Q  -  S )
)  e.  CC )
178173, 175mulcld 9681 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  e.  CC )
179177, 178addcomd 9853 . . . . . . 7  |-  ( ph  ->  ( ( G  x.  ( Q  -  S
) )  +  ( G  x.  ( S  -  ( A `  Z ) ) ) )  =  ( ( G  x.  ( S  -  ( A `  Z ) ) )  +  ( G  x.  ( Q  -  S
) ) ) )
180158, 176, 1793eqtrd 2509 . . . . . 6  |-  ( ph  ->  ( G  x.  ( Q  -  ( A `  Z ) ) )  =  ( ( G  x.  ( S  -  ( A `  Z ) ) )  +  ( G  x.  ( Q  -  S ) ) ) )
18167, 75jca 541 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  e.  RR  /\  S  e.  RR ) )
182 resubcl 9958 . . . . . . . . . . . . 13  |-  ( ( Q  e.  RR  /\  S  e.  RR )  ->  ( Q  -  S
)  e.  RR )
183181, 182syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  -  S
)  e.  RR )
184172, 183jca 541 . . . . . . . . . . 11  |-  ( ph  ->  ( G  e.  RR  /\  ( Q  -  S
)  e.  RR ) )
185 remulcl 9642 . . . . . . . . . . 11  |-  ( ( G  e.  RR  /\  ( Q  -  S
)  e.  RR )  ->  ( G  x.  ( Q  -  S
) )  e.  RR )
186184, 185syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( G  x.  ( Q  -  S )
)  e.  RR )
18775, 9jca 541 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  RR  /\  ( A `  Z
)  e.  RR ) )
188 resubcl 9958 . . . . . . . . . . . . 13  |-  ( ( S  e.  RR  /\  ( A `  Z )  e.  RR )  -> 
( S  -  ( A `  Z )
)  e.  RR )
189187, 188syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  -  ( A `  Z )
)  e.  RR )
190172, 189jca 541 . . . . . . . . . . 11  |-  ( ph  ->  ( G  e.  RR  /\  ( S  -  ( A `  Z )
)  e.  RR ) )
191 remulcl 9642 . . . . . . . . . . 11  |-  ( ( G  e.  RR  /\  ( S  -  ( A `  Z )
)  e.  RR )  ->  ( G  x.  ( S  -  ( A `  Z )
) )  e.  RR )
192190, 191syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  e.  RR )
193186, 192jca 541 . . . . . . . . 9  |-  ( ph  ->  ( ( G  x.  ( Q  -  S
) )  e.  RR  /\  ( G  x.  ( S  -  ( A `  Z ) ) )  e.  RR ) )
194 readdcl 9640 . . . . . . . . 9  |-  ( ( ( G  x.  ( Q  -  S )
)  e.  RR  /\  ( G  x.  ( S  -  ( A `  Z ) ) )  e.  RR )  -> 
( ( G  x.  ( Q  -  S
) )  +  ( G  x.  ( S  -  ( A `  Z ) ) ) )  e.  RR )
195193, 194syl 17 . . . . . . . 8  |-  ( ph  ->  ( ( G  x.  ( Q  -  S
) )  +  ( G  x.  ( S  -  ( A `  Z ) ) ) )  e.  RR )
196179, 195eqeltrrd 2550 . . . . . . 7  |-  ( ph  ->  ( ( G  x.  ( S  -  ( A `  Z )
) )  +  ( G  x.  ( Q  -  S ) ) )  e.  RR )
197 1red 9676 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
198 hoidmvlelem2.e . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR+ )
199198rpred 11364 . . . . . . . . . 10  |-  ( ph  ->  E  e.  RR )
200197, 199readdcld 9688 . . . . . . . . 9  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
2012eldifbd 3403 . . . . . . . . . . 11  |-  ( ph  ->  -.  Z  e.  Y
)
2028, 201eldifd 3401 . . . . . . . . . 10  |-  ( ph  ->  Z  e.  ( W 
\  Y ) )
203 hoidmvlelem2.r . . . . . . . . . 10  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
204 hoidmvlelem2.h . . . . . . . . . 10  |-  H  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W ) 
|->  ( j  e.  W  |->  if ( j  e.  Y ,  ( c `
 j ) ,  if ( ( c `
 j )  <_  x ,  ( c `  j ) ,  x
) ) ) ) )
205161, 164, 202, 7, 109, 28, 203, 204, 75sge0hsphoire 38529 . . . . . . . . 9  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  RR )
206200, 205remulcld 9689 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  e.  RR )
207 fzfid 12224 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
208183adantr 472 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( Q  -  S )  e.  RR )
209 simpl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ph )
210 elfznn 11854 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... M )  ->  j  e.  NN )
211210adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  j  e.  NN )
212 id 22 . . . . . . . . . . . . . . . 16  |-  ( j  e.  NN  ->  j  e.  NN )
213 ovex 6336 . . . . . . . . . . . . . . . . 17  |-  ( ( J `  j ) ( L `  Y
) ( K `  j ) )  e. 
_V
214213a1i 11 . . . . . . . . . . . . . . . 16  |-  ( j  e.  NN  ->  (
( J `  j
) ( L `  Y ) ( K `
 j ) )  e.  _V )
215 hoidmvlelem2.p . . . . . . . . . . . . . . . . 17  |-  P  =  ( j  e.  NN  |->  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
216215fvmpt2 5972 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  NN  /\  ( ( J `  j ) ( L `
 Y ) ( K `  j ) )  e.  _V )  ->  ( P `  j
)  =  ( ( J `  j ) ( L `  Y
) ( K `  j ) ) )
217212, 214, 216syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  ->  ( P `  j )  =  ( ( J `
 j ) ( L `  Y ) ( K `  j
) ) )
218217adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  =  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
219164adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e. 
Fin )
220166a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN )  ->  Y  C_  W )
221112, 220fssresd 5762 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j )  |`  Y ) : Y --> RR )
222221adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( C `  j
)  |`  Y ) : Y --> RR )
223 iftrue 3878 . . . . . . . . . . . . . . . . . . . 20  |-  ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  ( ( C `  j )  |`  Y ) )
224223adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  ( ( C `  j )  |`  Y ) )
225224feq1d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  ( if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) : Y --> RR  <->  ( ( C `  j )  |`  Y ) : Y --> RR ) )
226222, 225mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) : Y --> RR )
227 0red 9662 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  Y )  ->  0  e.  RR )
228 hoidmvlelem2.f . . . . . . . . . . . . . . . . . . . 20  |-  F  =  ( y  e.  Y  |->  0 )
229227, 228fmptd 6061 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : Y --> RR )
230229ad2antrr 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F : Y --> RR )
231 iffalse 3881 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  F )
232231adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  F )
233232feq1d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  -> 
( if ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR 
<->  F : Y --> RR ) )
234230, 233mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) : Y --> RR )
235226, 234pm2.61dan 808 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR )
236 simpr 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  NN )
237 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C `
 j )  e. 
_V
238237resex 5154 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( C `  j )  |`  Y )  e.  _V
239238a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( C `  j )  |`  Y )  e.  _V )
240162, 163ssexd 4543 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Y  e.  _V )
241 mptexg 6151 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Y  e.  _V  ->  (
y  e.  Y  |->  0 )  e.  _V )
242240, 241syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( y  e.  Y  |->  0 )  e.  _V )
243228, 242syl5eqel 2553 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  e.  _V )
244239, 243ifcld 3915 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( C `  j )  |`  Y ) ,  F
)  e.  _V )
245244adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F )  e.  _V )
246 hoidmvlelem2.j . . . . . . . . . . . . . . . . . . 19  |-  J  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
) )
247246fvmpt2 5972 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  NN  /\  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  e.  _V )  ->  ( J `  j
)  =  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) )
248236, 245, 247syl2anc 673 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j )  =  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( C `  j )  |`  Y ) ,  F
) )
249248feq1d 5724 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( J `  j ) : Y --> RR  <->  if ( S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR ) )
250235, 249mpbird 240 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j ) : Y --> RR )
25131, 220fssresd 5762 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j )  |`  Y ) : Y --> RR )
252251adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( D `  j
)  |`  Y ) : Y --> RR )
253 iftrue 3878 . . . . . . . . . . . . . . . . . . . 20  |-  ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  ( ( D `  j )  |`  Y ) )
254253adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  ( ( D `  j )  |`  Y ) )
255254feq1d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  ( if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) : Y --> RR  <->  ( ( D `  j )  |`  Y ) : Y --> RR ) )
256252, 255mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) : Y --> RR )
257 iffalse 3881 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  F )
258257adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  F )
259258feq1d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  -> 
( if ( S  e.  ( ( ( C `  j ) `
 Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F ) : Y --> RR 
<->  F : Y --> RR ) )
260230, 259mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) : Y --> RR )
261256, 260pm2.61dan 808 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F ) : Y --> RR )
262 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D `
 j )  e. 
_V
263262resex 5154 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D `  j )  |`  Y )  e.  _V
264263a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D `  j )  |`  Y )  e.  _V )
265264, 243ifcld 3915 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( D `  j )  |`  Y ) ,  F
)  e.  _V )
266265adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F )  e.  _V )
267 hoidmvlelem2.k . . . . . . . . . . . . . . . . . . 19  |-  K  =  ( j  e.  NN  |->  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
) )
268267fvmpt2 5972 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  NN  /\  if ( S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  e.  _V )  ->  ( K `  j
)  =  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F ) )
269236, 266, 268syl2anc 673 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j )  =  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( D `  j )  |`  Y ) ,  F
) )
270269feq1d 5724 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( K `  j ) : Y --> RR  <->  if ( S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F ) : Y --> RR ) )
271261, 270mpbird 240 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j ) : Y --> RR )
272161, 219, 250, 271hoidmvcl 38522 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( J `  j ) ( L `  Y
) ( K `  j ) )  e.  ( 0 [,) +oo ) )
273218, 272eqeltrd 2549 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  ( 0 [,) +oo ) )
274159, 273sseldi 3416 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  RR )
275209, 211, 274syl2anc 673 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P `  j )  e.  RR )
276208, 275remulcld 9689 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( Q  -  S
)  x.  ( P `
 j ) )  e.  RR )
277207, 276fsumrecl 13877 . . . . . . . . 9  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
)  e.  RR )
278200, 277remulcld 9689 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) )  e.  RR )
279206, 278readdcld 9688 . . . . . . 7  |-  ( ph  ->  ( ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) )  +  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) ) )  e.  RR )
280161, 164, 202, 7, 109, 28, 203, 204, 67sge0hsphoire 38529 . . . . . . . 8  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  Q
) `  ( D `  j ) ) ) ) )  e.  RR )
281200, 280remulcld 9689 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  Q ) `
 ( D `  j ) ) ) ) ) )  e.  RR )
28274, 68syl6eleq 2559 . . . . . . . . . 10  |-  ( ph  ->  S  e.  { z  e.  ( ( A `
 Z ) [,] ( B `  Z
) )  |  ( G  x.  ( z  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) } )
283 oveq1 6315 . . . . . . . . . . . . 13  |-  ( z  =  S  ->  (
z  -  ( A `
 Z ) )  =  ( S  -  ( A `  Z ) ) )
284283oveq2d 6324 . . . . . . . . . . . 12  |-  ( z  =  S  ->  ( G  x.  ( z  -  ( A `  Z ) ) )  =  ( G  x.  ( S  -  ( A `  Z )
) ) )
285 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( z  =  S  ->  ( H `  z )  =  ( H `  S ) )
286285fveq1d 5881 . . . . . . . . . . . . . . . 16  |-  ( z  =  S  ->  (
( H `  z
) `  ( D `  j ) )  =  ( ( H `  S ) `  ( D `  j )
) )
287286oveq2d 6324 . . . . . . . . . . . . . . 15  |-  ( z  =  S  ->  (
( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) )  =  ( ( C `
 j ) ( L `  W ) ( ( H `  S ) `  ( D `  j )
) ) )
288287mpteq2dv 4483 . . . . . . . . . . . . . 14  |-  ( z  =  S  ->  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) ) ) )
289288fveq2d 5883 . . . . . . . . . . . . 13  |-  ( z  =  S  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) ) ) )  =  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )
290289oveq2d 6324 . . . . . . . . . . . 12  |-  ( z  =  S  ->  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) )  =  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )
291284, 290breq12d 4408 . . . . . . . . . . 11  |-  ( z  =  S  ->  (
( G  x.  (
z  -  ( A `
 Z ) ) )  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) )  <->  ( G  x.  ( S  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) ) )
292291elrab 3184 . . . . . . . . . 10  |-  ( S  e.  { z  e.  ( ( A `  Z ) [,] ( B `  Z )
)  |  ( G  x.  ( z  -  ( A `  Z ) ) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) ) }  <-> 
( S  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  /\  ( G  x.  ( S  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) ) )
293282, 292sylib 201 . . . . . . . . 9  |-  ( ph  ->  ( S  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  /\  ( G  x.  ( S  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) ) )
294293simprd 470 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
295207, 275fsumrecl 13877 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( P `  j
)  e.  RR )
296200, 295remulcld 9689 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( P `  j ) )  e.  RR )
297 0red 9662 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  RR )
29875, 67posdifd 10221 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  <  Q  <->  0  <  ( Q  -  S ) ) )
299144, 298mpbid 215 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( Q  -  S ) )
300297, 183, 299ltled 9800 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( Q  -  S ) )
301 hoidmvlelem2.le . . . . . . . . . 10  |-  ( ph  ->  G  <_  ( (
1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( P `  j
) ) )
302172, 296, 183, 300, 301lemul1ad 10568 . . . . . . . . 9  |-  ( ph  ->  ( G  x.  ( Q  -  S )
)  <_  ( (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... M
) ( P `  j ) )  x.  ( Q  -  S
) ) )
303200recnd 9687 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  +  E
)  e.  CC )
304295recnd 9687 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( P `  j
)  e.  CC )
305303, 304, 174mulassd 9684 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... M ) ( P `  j
) )  x.  ( Q  -  S )
)  =  ( ( 1  +  E )  x.  ( sum_ j  e.  ( 1 ... M
) ( P `  j )  x.  ( Q  -  S )
) ) )
306275recnd 9687 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P `  j )  e.  CC )
307207, 174, 306fsummulc1 13923 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ j  e.  ( 1 ... M ) ( P `  j
)  x.  ( Q  -  S ) )  =  sum_ j  e.  ( 1 ... M ) ( ( P `  j )  x.  ( Q  -  S )
) )
308174adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( Q  -  S )  e.  CC )
309306, 308mulcomd 9682 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( P `  j
)  x.  ( Q  -  S ) )  =  ( ( Q  -  S )  x.  ( P `  j
) ) )
310309sumeq2dv 13846 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( P `  j )  x.  ( Q  -  S )
)  =  sum_ j  e.  ( 1 ... M
) ( ( Q  -  S )  x.  ( P `  j
) ) )
311307, 310eqtrd 2505 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  ( 1 ... M ) ( P `  j
)  x.  ( Q  -  S ) )  =  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) )
312311oveq2d 6324 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  E )  x.  ( sum_ j  e.  ( 1 ... M ) ( P `  j )  x.  ( Q  -  S ) ) )  =  ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )
313305, 312eqtrd 2505 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... M ) ( P `  j
) )  x.  ( Q  -  S )
)  =  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )
314302, 313breqtrd 4420 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( Q  -  S )
)  <_  ( (
1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )
315192, 186, 206, 278, 294, 314leadd12dd 37626 . . . . . . 7  |-  ( ph  ->  ( ( G  x.  ( S  -  ( A `  Z )
) )  +  ( G  x.  ( Q  -  S ) ) )  <_  ( (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) )  +  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) ) ) )
316 hoidmvlelem2.m . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  NN )
317 nnsplit 37668 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  NN  ->  NN  =  ( ( 1 ... M )  u.  ( ZZ>= `  ( M  +  1 ) ) ) )
318316, 317syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  NN  =  ( ( 1 ... M )  u.  ( ZZ>= `  ( M  +  1 ) ) ) )
319 uncom 3569 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... M )  u.  ( ZZ>= `  ( M  +  1 ) ) )  =  ( ( ZZ>= `  ( M  +  1 ) )  u.  ( 1 ... M ) )
320319a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... M )  u.  ( ZZ>=
`  ( M  + 
1 ) ) )  =  ( ( ZZ>= `  ( M  +  1
) )  u.  (
1 ... M ) ) )
321318, 320eqtr2d 2506 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ZZ>= `  ( M  +  1 ) )  u.  ( 1 ... M ) )  =  NN )
322321eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  =  ( (
ZZ>= `  ( M  + 
1 ) )  u.  ( 1 ... M
) ) )
323322mpteq1d 4477 . . . . . . . . . . . . 13  |-  ( ph  ->  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) )  =  ( j  e.  ( ( ZZ>= `  ( M  +  1
) )  u.  (
1 ... M ) ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )
324323fveq2d 5883 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  =  (Σ^ `  (
j  e.  ( (
ZZ>= `  ( M  + 
1 ) )  u.  ( 1 ... M
) )  |->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) ) ) ) )
325 nfv 1769 . . . . . . . . . . . . 13  |-  F/ j
ph
326 fvex 5889 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  ( M  +  1
) )  e.  _V
327326a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ZZ>= `  ( M  +  1 ) )  e.  _V )
328 ovex 6336 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  e. 
_V
329328a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  e.  _V )
330 incom 3616 . . . . . . . . . . . . . . 15  |-  ( (
ZZ>= `  ( M  + 
1 ) )  i^i  ( 1 ... M
) )  =  ( ( 1 ... M
)  i^i  ( ZZ>= `  ( M  +  1
) ) )
331 nnuzdisj 37665 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M )  i^i  ( ZZ>= `  ( M  +  1 ) ) )  =  (/)
332330, 331eqtri 2493 . . . . . . . . . . . . . 14  |-  ( (
ZZ>= `  ( M  + 
1 ) )  i^i  ( 1 ... M
) )  =  (/)
333332a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ZZ>= `  ( M  +  1 ) )  i^i  ( 1 ... M ) )  =  (/) )
334 icossicc 11746 . . . . . . . . . . . . . 14  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
335 ssid 3437 . . . . . . . . . . . . . . 15  |-  ( 0 [,) +oo )  C_  ( 0 [,) +oo )
336 simpl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ph )
337316peano2nnd 10648 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M  +  1 )  e.  NN )
338 uznnssnn 11229 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  +  1 )  e.  NN  ->  ( ZZ>=
`  ( M  + 
1 ) )  C_  NN )
339337, 338syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ZZ>= `  ( M  +  1 ) ) 
C_  NN )
340339adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ZZ>= `  ( M  +  1
) )  C_  NN )
341 simpr 468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  j  e.  ( ZZ>= `  ( M  +  1 ) ) )
342340, 341sseldd 3419 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  j  e.  NN )
343 snfi 7668 . . . . . . . . . . . . . . . . . . . . 21  |-  { Z }  e.  Fin
344343a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { Z }  e.  Fin )
345 unfi 7856 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Y  e.  Fin  /\  { Z }  e.  Fin )  ->  ( Y  u.  { Z } )  e. 
Fin )
346164, 344, 345syl2anc 673 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Y  u.  { Z } )  e.  Fin )
3477, 346syl5eqel 2553 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  W  e.  Fin )
348347adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  W  e. 
Fin )
349 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  l  ->  (
j  e.  Y  <->  l  e.  Y ) )
350 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  l  ->  (
c `  j )  =  ( c `  l ) )
351350breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  l  ->  (
( c `  j
)  <_  x  <->  ( c `  l )  <_  x
) )
352351, 350ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  l  ->  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
)  =  if ( ( c `  l
)  <_  x , 
( c `  l
) ,  x ) )
353349, 350, 352ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  l  ->  if ( j  e.  Y ,  ( c `  j ) ,  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
) )  =  if ( l  e.  Y ,  ( c `  l ) ,  if ( ( c `  l )  <_  x ,  ( c `  l ) ,  x
) ) )
354353cbvmptv 4488 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  W  |->  if ( j  e.  Y , 
( c `  j
) ,  if ( ( c `  j
)  <_  x , 
( c `  j
) ,  x ) ) )  =  ( l  e.  W  |->  if ( l  e.  Y ,  ( c `  l ) ,  if ( ( c `  l )  <_  x ,  ( c `  l ) ,  x
) ) )
355354mpteq2i 4479 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  e.  ( RR  ^m  W )  |->  ( j  e.  W  |->  if ( j  e.  Y , 
( c `  j
) ,  if ( ( c `  j
)  <_  x , 
( c `  j
) ,  x ) ) ) )  =  ( c  e.  ( RR  ^m  W ) 
|->  ( l  e.  W  |->  if ( l  e.  Y ,  ( c `
 l ) ,  if ( ( c `
 l )  <_  x ,  ( c `  l ) ,  x
) ) ) )
356355mpteq2i 4479 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W )  |->  ( j  e.  W  |->  if ( j  e.  Y , 
( c `  j
) ,  if ( ( c `  j
)  <_  x , 
( c `  j
) ,  x ) ) ) ) )  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W
)  |->  ( l  e.  W  |->  if ( l  e.  Y ,  ( c `  l ) ,  if ( ( c `  l )  <_  x ,  ( c `  l ) ,  x ) ) ) ) )
357204, 356eqtri 2493 . . . . . . . . . . . . . . . . . 18  |-  H  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W ) 
|->  ( l  e.  W  |->  if ( l  e.  Y ,  ( c `
 l ) ,  if ( ( c `
 l )  <_  x ,  ( c `  l ) ,  x
) ) ) ) )
35875adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  S  e.  RR )
359357, 358, 348, 31hsphoif 38516 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( H `  S ) `
 ( D `  j ) ) : W --> RR )
360161, 348, 112, 359hoidmvcl 38522 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
361336, 342, 360syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( C `  j )
( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
362335, 361sseldi 3416 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( C `  j )
( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
363334, 362sseldi 3416 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( C `  j )
( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
364209, 211, 360syl2anc 673 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  ( 0 [,) +oo ) )
365334, 364sseldi 3416 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  ( 0 [,] +oo ) )
366325, 327, 329, 333, 363, 365sge0splitmpt 38367 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  ( ( ZZ>= `  ( M  +  1 ) )  u.  ( 1 ... M ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  =  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) +e
(Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
367 nnex 10637 . . . . . . . . . . . . . . 15  |-  NN  e.  _V
368367a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  e.  _V )
369334, 360sseldi 3416 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
370325, 368, 369, 205, 339sge0ssrempt 38361 . . . . . . . . . . . . 13  |-  ( ph  ->  (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  e.  RR )
37118a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ... M
)  C_  NN )
372325, 368, 369, 205, 371sge0ssrempt 38361 . . . . . . . . . . . . 13  |-  ( ph  ->  (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  RR )
373 rexadd 11548 . . . . . . . . . . . . 13  |-  ( ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  e.  RR  /\  (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  RR )  ->  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) +e
(Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) )  =  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )
374370, 372, 373syl2anc 673 . . . . . . . . . . . 12  |-  ( ph  ->  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) +e
(Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) )  =  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )
375324, 366, 3743eqtrd 2509 . . . . . . . . . . 11  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  =  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )
376375oveq2d 6324 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  =  ( ( 1  +  E )  x.  (
(Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) ) )
377376oveq1d 6323 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) )  +  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) ) )  =  ( ( ( 1  +  E )  x.  (
(Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )  +  ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) ) )
378375, 205eqeltrrd 2550 . . . . . . . . . . . 12  |-  ( ph  ->  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  e.  RR )
379378recnd 9687 . . . . . . . . . . 11  |-  ( ph  ->  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  e.  CC )
380277recnd 9687 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
)  e.  CC )
381303, 379, 380adddid 9685 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  E )  x.  (
( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  + 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )  =  ( ( ( 1  +  E )  x.  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )  +  ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) ) )
382381eqcomd 2477 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  +  E )  x.  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )  +  ( ( 1  +  E )  x. 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )  =  ( ( 1  +  E )  x.  (
( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  + 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) ) )
383370recnd 9687 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  e.  CC )
384372recnd 9687 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  CC )
385383, 384, 380addassd 9683 . . . . . . . . . . 11  |-  ( ph  ->  ( ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  (Σ^ `  (
j  e.  ( 1 ... M )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  + 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) )  =  ( (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  +  ( (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  +  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) ) ) )
386207, 364sge0fsummpt 38346 . . . . . . . . . . . . . 14  |-  ( ph  ->  (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  =  sum_ j  e.  ( 1 ... M ) ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) )
387386oveq1d 6323 . . . . . . . . . . . . 13  |-  ( ph  ->  ( (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  +  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) )  =  ( sum_ j  e.  ( 1 ... M ) ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  +  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )
388 ax-resscn 9614 . . . . . . . . . . . . . . . . . 18  |-  RR  C_  CC
389159, 388sstri 3427 . . . . . . . . . . . . . . . . 17  |-  ( 0 [,) +oo )  C_  CC
390389, 360sseldi 3416 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  CC )
391209, 211, 390syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  CC )
392183adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( Q  -  S )  e.  RR )
393392, 274remulcld 9689 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( Q  -  S )  x.  ( P `  j ) )  e.  RR )
394393recnd 9687 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( Q  -  S )  x.  ( P `  j ) )  e.  CC )
395211, 394syldan 478 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( Q  -  S
)  x.  ( P `
 j ) )  e.  CC )
396207, 391, 395fsumadd 13882 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( ( C `
 j ) ( L `  W ) ( ( H `  S ) `  ( D `  j )
) )  +  ( ( Q  -  S
)  x.  ( P `
 j ) ) )  =  ( sum_ j  e.  ( 1 ... M ) ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  +  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) ) )
397396eqcomd 2477 . . . . . . . . . . . . 13  |-  ( ph  ->  ( sum_ j  e.  ( 1 ... M ) ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) )  +  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) )  =  sum_ j  e.  ( 1 ... M ) ( ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) )  +  ( ( Q  -  S )  x.  ( P `  j
) ) ) )
398387, 397eqtrd 2505 . . . . . . . . . . . 12  |-  ( ph  ->  ( (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) (