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 38428
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 3996 . . . . . . . . . 10  |-  ( Z  e.  ( X  \  Y )  ->  Z  e.  { Z } )
42, 3syl 17 . . . . . . . . 9  |-  ( ph  ->  Z  e.  { Z } )
5 elun2 3604 . . . . . . . . 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 2542 . . . . . . 7  |-  ( ph  ->  Z  e.  W )
91, 8ffvelrnd 6028 . . . . . 6  |-  ( ph  ->  ( A `  Z
)  e.  RR )
10 hoidmvlelem2.b . . . . . . 7  |-  ( ph  ->  B : W --> RR )
1110, 8ffvelrnd 6028 . . . . . 6  |-  ( ph  ->  ( B `  Z
)  e.  RR )
12 hoidmvlelem2.v . . . . . . . 8  |-  V  =  ( { ( B `
 Z ) }  u.  O )
1311snssd 4120 . . . . . . . . 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 1763 . . . . . . . . . . 11  |-  F/ i
ph
16 eqid 2453 . . . . . . . . . . 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 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ph )
18 fz1ssnn 11837 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  C_  NN
19 elrabi 3195 . . . . . . . . . . . . . 14  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  i  e.  ( 1 ... M
) )
2018, 19sseldi 3432 . . . . . . . . . . . . 13  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  i  e.  NN )
2120adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  i  e.  NN )
22 eleq1 2519 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
j  e.  NN  <->  i  e.  NN ) )
2322anbi2d 711 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ph  /\  j  e.  NN )  <->  ( ph  /\  i  e.  NN ) ) )
24 fveq2 5870 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( D `  j )  =  ( D `  i ) )
2524fveq1d 5872 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( D `  j
) `  Z )  =  ( ( D `
 i ) `  Z ) )
2625eleq1d 2515 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ( D `  j ) `  Z
)  e.  RR  <->  ( ( D `  i ) `  Z )  e.  RR ) )
2723, 26imbi12d 322 . . . . . . . . . . . . 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 6027 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  W
) )
30 elmapi 7498 . . . . . . . . . . . . . . 15  |-  ( ( D `  j )  e.  ( RR  ^m  W )  ->  ( D `  j ) : W --> RR )
3129, 30syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : W --> RR )
328adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  Z  e.  W )
3331, 32ffvelrnd 6028 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j ) `
 Z )  e.  RR )
3427, 33chvarv 2109 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( D `  i ) `
 Z )  e.  RR )
3517, 21, 34syl2anc 667 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ( ( D `
 i ) `  Z )  e.  RR )
3615, 16, 35rnmptssd 37483 . . . . . . . . . 10  |-  ( ph  ->  ran  ( i  e. 
{ j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) }  |->  ( ( D `
 i ) `  Z ) )  C_  RR )
3714, 36syl5eqss 3478 . . . . . . . . 9  |-  ( ph  ->  O  C_  RR )
3813, 37unssd 3612 . . . . . . . 8  |-  ( ph  ->  ( { ( B `
 Z ) }  u.  O )  C_  RR )
3912, 38syl5eqss 3478 . . . . . . 7  |-  ( ph  ->  V  C_  RR )
40 hoidmvlelem2.q . . . . . . . 8  |-  Q  = inf ( V ,  RR ,  <  )
41 ltso 9719 . . . . . . . . . 10  |-  <  Or  RR
4241a1i 11 . . . . . . . . 9  |-  ( ph  ->  <  Or  RR )
43 snfi 7655 . . . . . . . . . . . 12  |-  { ( B `  Z ) }  e.  Fin
4443a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  { ( B `  Z ) }  e.  Fin )
45 fzfi 12192 . . . . . . . . . . . . . . 15  |-  ( 1 ... M )  e. 
Fin
46 rabfi 7801 . . . . . . . . . . . . . . 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 37445 . . . . . . . . . . . . 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 2535 . . . . . . . . . . 11  |-  ( ph  ->  O  e.  Fin )
52 unfi 7843 . . . . . . . . . . 11  |-  ( ( { ( B `  Z ) }  e.  Fin  /\  O  e.  Fin )  ->  ( { ( B `  Z ) }  u.  O )  e.  Fin )
5344, 51, 52syl2anc 667 . . . . . . . . . 10  |-  ( ph  ->  ( { ( B `
 Z ) }  u.  O )  e. 
Fin )
5412, 53syl5eqel 2535 . . . . . . . . 9  |-  ( ph  ->  V  e.  Fin )
55 fvex 5880 . . . . . . . . . . . . . 14  |-  ( B `
 Z )  e. 
_V
5655snid 3998 . . . . . . . . . . . . 13  |-  ( B `
 Z )  e. 
{ ( B `  Z ) }
57 elun1 3603 . . . . . . . . . . . . 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 2462 . . . . . . . . . . . 12  |-  ( { ( B `  Z
) }  u.  O
)  =  V
6058, 59eleqtri 2529 . . . . . . . . . . 11  |-  ( B `
 Z )  e.  V
6160a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( B `  Z
)  e.  V )
62 ne0i 3739 . . . . . . . . . 10  |-  ( ( B `  Z )  e.  V  ->  V  =/=  (/) )
6361, 62syl 17 . . . . . . . . 9  |-  ( ph  ->  V  =/=  (/) )
64 fiinfcl 8022 . . . . . . . . 9  |-  ( (  <  Or  RR  /\  ( V  e.  Fin  /\  V  =/=  (/)  /\  V  C_  RR ) )  -> inf ( V ,  RR ,  <  )  e.  V )
6542, 54, 63, 39, 64syl13anc 1271 . . . . . . . 8  |-  ( ph  -> inf ( V ,  RR ,  <  )  e.  V
)
6640, 65syl5eqel 2535 . . . . . . 7  |-  ( ph  ->  Q  e.  V )
6739, 66sseldd 3435 . . . . . 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 3516 . . . . . . . . . . . 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 3464 . . . . . . . . . . 11  |-  U  C_  ( ( A `  Z ) [,] ( B `  Z )
)
7170a1i 11 . . . . . . . . . 10  |-  ( ph  ->  U  C_  ( ( A `  Z ) [,] ( B `  Z
) ) )
729, 11iccssred 37612 . . . . . . . . . 10  |-  ( ph  ->  ( ( A `  Z ) [,] ( B `  Z )
)  C_  RR )
7371, 72sstrd 3444 . . . . . . . . 9  |-  ( ph  ->  U  C_  RR )
74 hoidmvlelem2.su . . . . . . . . 9  |-  ( ph  ->  S  e.  U )
7573, 74sseldd 3435 . . . . . . . 8  |-  ( ph  ->  S  e.  RR )
769rexrd 9695 . . . . . . . . 9  |-  ( ph  ->  ( A `  Z
)  e.  RR* )
7711rexrd 9695 . . . . . . . . 9  |-  ( ph  ->  ( B `  Z
)  e.  RR* )
7870, 74sseldi 3432 . . . . . . . . 9  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
79 iccgelb 11698 . . . . . . . . 9  |-  ( ( ( A `  Z
)  e.  RR*  /\  ( B `  Z )  e.  RR*  /\  S  e.  ( ( A `  Z ) [,] ( B `  Z )
) )  ->  ( A `  Z )  <_  S )
8076, 77, 78, 79syl3anc 1269 . . . . . . . 8  |-  ( ph  ->  ( A `  Z
)  <_  S )
81 hoidmvlelem2.sb . . . . . . . . . . . . . . 15  |-  ( ph  ->  S  <  ( B `
 Z ) )
8281adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  ( B `  Z ) )  ->  S  <  ( B `  Z ) )
83 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( B `  Z )  ->  x  =  ( B `  Z ) )
8483eqcomd 2459 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B `  Z )  ->  ( B `  Z )  =  x )
8584adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  ( B `  Z ) )  ->  ( B `  Z )  =  x )
8682, 85breqtrd 4430 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  =  ( B `  Z ) )  ->  S  <  x )
8786adantlr 722 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  V )  /\  x  =  ( B `  Z ) )  ->  S  <  x )
88 simpll 761 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  V )  /\  -.  x  =  ( B `  Z ) )  ->  ph )
89 id 22 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  V  ->  x  e.  V )
9089, 12syl6eleq 2541 . . . . . . . . . . . . . . . 16  |-  ( x  e.  V  ->  x  e.  ( { ( B `
 Z ) }  u.  O ) )
9190adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  V  /\  -.  x  =  ( B `  Z )
)  ->  x  e.  ( { ( B `  Z ) }  u.  O ) )
92 elsni 3995 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  { ( B `
 Z ) }  ->  x  =  ( B `  Z ) )
9392con3i 141 . . . . . . . . . . . . . . . 16  |-  ( -.  x  =  ( B `
 Z )  ->  -.  x  e.  { ( B `  Z ) } )
9493adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  V  /\  -.  x  =  ( B `  Z )
)  ->  -.  x  e.  { ( B `  Z ) } )
95 elunnel1 3577 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( { ( B `  Z
) }  u.  O
)  /\  -.  x  e.  { ( B `  Z ) } )  ->  x  e.  O
)
9691, 94, 95syl2anc 667 . . . . . . . . . . . . . 14  |-  ( ( x  e.  V  /\  -.  x  =  ( B `  Z )
)  ->  x  e.  O )
9796adantll 721 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  V )  /\  -.  x  =  ( B `  Z ) )  ->  x  e.  O )
98 id 22 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  O  ->  x  e.  O )
9998, 14syl6eleq 2541 . . . . . . . . . . . . . . . 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 3050 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
10116elrnmpt 5084 . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . 15  |-  ( x  e.  O  ->  E. i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) } x  =  ( ( D `  i
) `  Z )
)
104103adantl 468 . . . . . . . . . . . . . 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 5870 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  i  ->  ( C `  j )  =  ( C `  i ) )
106105fveq1d 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  i  ->  (
( C `  j
) `  Z )  =  ( ( C `
 i ) `  Z ) )
107106eleq1d 2515 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  i  ->  (
( ( C `  j ) `  Z
)  e.  RR  <->  ( ( C `  i ) `  Z )  e.  RR ) )
10823, 107imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . 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 6027 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  W
) )
111 elmapi 7498 . . . . . . . . . . . . . . . . . . . . . . . . 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 6028 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) `
 Z )  e.  RR )
114108, 113chvarv 2109 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( C `  i ) `
 Z )  e.  RR )
115114rexrd 9695 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( C `  i ) `
 Z )  e. 
RR* )
11617, 21, 115syl2anc 667 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ( ( C `
 i ) `  Z )  e.  RR* )
11734rexrd 9695 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( D `  i ) `
 Z )  e. 
RR* )
11817, 21, 117syl2anc 667 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  ( ( D `
 i ) `  Z )  e.  RR* )
119106, 25oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  i  ->  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) )  =  ( ( ( C `  i ) `
 Z ) [,) ( ( D `  i ) `  Z
) ) )
120119eleq2d 2516 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  i  ->  ( S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  <->  S  e.  ( ( ( C `
 i ) `  Z ) [,) (
( D `  i
) `  Z )
) ) )
121120elrab 3198 . . . . . . . . . . . . . . . . . . . . . . 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 198 . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  { j  e.  ( 1 ... M
)  |  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) }  ->  S  e.  ( ( ( C `
 i ) `  Z ) [,) (
( D `  i
) `  Z )
) )
124123adantl 468 . . . . . . . . . . . . . . . . . . . 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 37617 . . . . . . . . . . . . . . . . . . . 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 1269 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) } )  ->  S  <  (
( D `  i
) `  Z )
)
1271263adant3 1029 . . . . . . . . . . . . . . . . . 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 2459 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( ( D `
 i ) `  Z )  ->  (
( D `  i
) `  Z )  =  x )
1301293ad2ant3 1032 . . . . . . . . . . . . . . . . . 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 4430 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  { j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  /\  x  =  ( ( D `  i ) `  Z ) )  ->  S  <  x )
1321313exp 1208 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( i  e.  {
j  e.  ( 1 ... M )  |  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) }  ->  ( x  =  ( ( D `  i ) `
 Z )  ->  S  <  x ) ) )
133132adantr 467 . . . . . . . . . . . . . . 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 2879 . . . . . . . . . . . . . 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 667 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  V )  /\  -.  x  =  ( B `  Z ) )  ->  S  <  x )
13787, 136pm2.61dan 801 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  V )  ->  S  <  x )
138137ralrimiva 2804 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  V  S  <  x )
139 breq2 4409 . . . . . . . . . . 11  |-  ( x  = inf ( V ,  RR ,  <  )  -> 
( S  <  x  <->  S  < inf ( V ,  RR ,  <  ) ) )
140139rspcva 3150 . . . . . . . . . 10  |-  ( (inf ( V ,  RR ,  <  )  e.  V  /\  A. x  e.  V  S  <  x )  ->  S  < inf ( V ,  RR ,  <  ) )
14165, 138, 140syl2anc 667 . . . . . . . . 9  |-  ( ph  ->  S  < inf ( V ,  RR ,  <  )
)
14240eqcomi 2462 . . . . . . . . . 10  |- inf ( V ,  RR ,  <  )  =  Q
143142a1i 11 . . . . . . . . 9  |-  ( ph  -> inf ( V ,  RR ,  <  )  =  Q )
144141, 143breqtrd 4430 . . . . . . . 8  |-  ( ph  ->  S  <  Q )
1459, 75, 67, 80, 144lelttrd 9798 . . . . . . 7  |-  ( ph  ->  ( A `  Z
)  <  Q )
1469, 67, 145ltled 9788 . . . . . 6  |-  ( ph  ->  ( A `  Z
)  <_  Q )
147 fiminre 10562 . . . . . . . . 9  |-  ( ( V  C_  RR  /\  V  e.  Fin  /\  V  =/=  (/) )  ->  E. x  e.  V  A. y  e.  V  x  <_  y )
14839, 54, 63, 147syl3anc 1269 . . . . . . . 8  |-  ( ph  ->  E. x  e.  V  A. y  e.  V  x  <_  y )
149 lbinfle 10570 . . . . . . . 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 1269 . . . . . . 7  |-  ( ph  -> inf ( V ,  RR ,  <  )  <_  ( B `  Z )
)
15140, 150syl5eqbr 4439 . . . . . 6  |-  ( ph  ->  Q  <_  ( B `  Z ) )
1529, 11, 67, 146, 151eliccd 37611 . . . . 5  |-  ( ph  ->  Q  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
15367recnd 9674 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
15475recnd 9674 . . . . . . . . . 10  |-  ( ph  ->  S  e.  CC )
1559recnd 9674 . . . . . . . . . 10  |-  ( ph  ->  ( A `  Z
)  e.  CC )
156153, 154, 155npncand 10015 . . . . . . . . 9  |-  ( ph  ->  ( ( Q  -  S )  +  ( S  -  ( A `
 Z ) ) )  =  ( Q  -  ( A `  Z ) ) )
157156eqcomd 2459 . . . . . . . 8  |-  ( ph  ->  ( Q  -  ( A `  Z )
)  =  ( ( Q  -  S )  +  ( S  -  ( A `  Z ) ) ) )
158157oveq2d 6311 . . . . . . 7  |-  ( ph  ->  ( G  x.  ( Q  -  ( A `  Z ) ) )  =  ( G  x.  ( ( Q  -  S )  +  ( S  -  ( A `
 Z ) ) ) ) )
159 rge0ssre 11747 . . . . . . . . . 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 37424 . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  Fin )
165 ssun1 3599 . . . . . . . . . . . . . . 15  |-  Y  C_  ( Y  u.  { Z } )
166165, 7sseqtr4i 3467 . . . . . . . . . . . . . 14  |-  Y  C_  W
167166a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  C_  W )
1681, 167fssresd 5755 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  |`  Y ) : Y --> RR )
16910, 167fssresd 5755 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  |`  Y ) : Y --> RR )
170161, 164, 168, 169hoidmvcl 38414 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  ( 0 [,) +oo ) )
171160, 170syl5eqel 2535 . . . . . . . . . 10  |-  ( ph  ->  G  e.  ( 0 [,) +oo ) )
172159, 171sseldi 3432 . . . . . . . . 9  |-  ( ph  ->  G  e.  RR )
173172recnd 9674 . . . . . . . 8  |-  ( ph  ->  G  e.  CC )
174153, 154subcld 9991 . . . . . . . 8  |-  ( ph  ->  ( Q  -  S
)  e.  CC )
175154, 155subcld 9991 . . . . . . . 8  |-  ( ph  ->  ( S  -  ( A `  Z )
)  e.  CC )
176173, 174, 175adddid 9672 . . . . . . 7  |-  ( ph  ->  ( G  x.  (
( Q  -  S
)  +  ( S  -  ( A `  Z ) ) ) )  =  ( ( G  x.  ( Q  -  S ) )  +  ( G  x.  ( S  -  ( A `  Z )
) ) ) )
177173, 174mulcld 9668 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( Q  -  S )
)  e.  CC )
178173, 175mulcld 9668 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  e.  CC )
179177, 178addcomd 9840 . . . . . . 7  |-  ( ph  ->  ( ( G  x.  ( Q  -  S
) )  +  ( G  x.  ( S  -  ( A `  Z ) ) ) )  =  ( ( G  x.  ( S  -  ( A `  Z ) ) )  +  ( G  x.  ( Q  -  S
) ) ) )
180158, 176, 1793eqtrd 2491 . . . . . 6  |-  ( ph  ->  ( G  x.  ( Q  -  ( A `  Z ) ) )  =  ( ( G  x.  ( S  -  ( A `  Z ) ) )  +  ( G  x.  ( Q  -  S ) ) ) )
18167, 75jca 535 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  e.  RR  /\  S  e.  RR ) )
182 resubcl 9943 . . . . . . . . . . . . 13  |-  ( ( Q  e.  RR  /\  S  e.  RR )  ->  ( Q  -  S
)  e.  RR )
183181, 182syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  -  S
)  e.  RR )
184172, 183jca 535 . . . . . . . . . . 11  |-  ( ph  ->  ( G  e.  RR  /\  ( Q  -  S
)  e.  RR ) )
185 remulcl 9629 . . . . . . . . . . 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 535 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  RR  /\  ( A `  Z
)  e.  RR ) )
188 resubcl 9943 . . . . . . . . . . . . 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 535 . . . . . . . . . . 11  |-  ( ph  ->  ( G  e.  RR  /\  ( S  -  ( A `  Z )
)  e.  RR ) )
191 remulcl 9629 . . . . . . . . . . 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 535 . . . . . . . . 9  |-  ( ph  ->  ( ( G  x.  ( Q  -  S
) )  e.  RR  /\  ( G  x.  ( S  -  ( A `  Z ) ) )  e.  RR ) )
194 readdcl 9627 . . . . . . . . 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 2532 . . . . . . 7  |-  ( ph  ->  ( ( G  x.  ( S  -  ( A `  Z )
) )  +  ( G  x.  ( Q  -  S ) ) )  e.  RR )
197 1red 9663 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
198 hoidmvlelem2.e . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR+ )
199198rpred 11348 . . . . . . . . . 10  |-  ( ph  ->  E  e.  RR )
200197, 199readdcld 9675 . . . . . . . . 9  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
2012eldifbd 3419 . . . . . . . . . . 11  |-  ( ph  ->  -.  Z  e.  Y
)
2028, 201eldifd 3417 . . . . . . . . . 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 38421 . . . . . . . . 9  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  RR )
206200, 205remulcld 9676 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  e.  RR )
207 fzfid 12193 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
208183adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( Q  -  S )  e.  RR )
209 simpl 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ph )
210 elfznn 11835 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... M )  ->  j  e.  NN )
211210adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  j  e.  NN )
212 id 22 . . . . . . . . . . . . . . . 16  |-  ( j  e.  NN  ->  j  e.  NN )
213 ovex 6323 . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  NN  /\  ( ( J `  j ) ( L `
 Y ) ( K `  j ) )  e.  _V )  ->  ( P `  j
)  =  ( ( J `  j ) ( L `  Y
) ( K `  j ) ) )
217212, 214, 216syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  ->  ( P `  j )  =  ( ( J `
 j ) ( L `  Y ) ( K `  j
) ) )
218217adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  =  ( ( J `  j ) ( L `
 Y ) ( K `  j ) ) )
219164adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  Y  e. 
Fin )
220166a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN )  ->  Y  C_  W )
221112, 220fssresd 5755 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j )  |`  Y ) : Y --> RR )
222221adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( C `  j
)  |`  Y ) : Y --> RR )
223 iftrue 3889 . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . 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 5719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 9649 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  Y )  ->  0  e.  RR )
228 hoidmvlelem2.f . . . . . . . . . . . . . . . . . . . 20  |-  F  =  ( y  e.  Y  |->  0 )
229227, 228fmptd 6051 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : Y --> RR )
230229ad2antrr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  -.  S  e.  ( (
( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) )  ->  F : Y --> RR )
231 iffalse 3892 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( C `
 j )  |`  Y ) ,  F
)  =  F )
232231adantl 468 . . . . . . . . . . . . . . . . . . 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 5719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( C `  j
)  |`  Y ) ,  F ) : Y --> RR )
236 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  NN )
237 fvex 5880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C `
 j )  e. 
_V
238237resex 5151 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( C `  j )  |`  Y )  e.  _V
239238a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( C `  j )  |`  Y )  e.  _V )
240162, 163ssexd 4553 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Y  e.  _V )
241 mptexg 6140 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Y  e.  _V  ->  (
y  e.  Y  |->  0 )  e.  _V )
242240, 241syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( y  e.  Y  |->  0 )  e.  _V )
243228, 242syl5eqel 2535 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  e.  _V )
244239, 243ifcld 3926 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( C `  j )  |`  Y ) ,  F
)  e.  _V )
245244adantr 467 . . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j )  =  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( C `  j )  |`  Y ) ,  F
) )
249248feq1d 5719 . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( J `
 j ) : Y --> RR )
25131, 220fssresd 5755 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( D `  j )  |`  Y ) : Y --> RR )
252251adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  NN )  /\  S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) )  ->  (
( D `  j
)  |`  Y ) : Y --> RR )
253 iftrue 3889 . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . 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 5719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 3892 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) )  ->  if ( S  e.  (
( ( C `  j ) `  Z
) [,) ( ( D `  j ) `
 Z ) ) ,  ( ( D `
 j )  |`  Y ) ,  F
)  =  F )
258257adantl 468 . . . . . . . . . . . . . . . . . . 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 5719 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  if ( S  e.  ( ( ( C `  j
) `  Z ) [,) ( ( D `  j ) `  Z
) ) ,  ( ( D `  j
)  |`  Y ) ,  F ) : Y --> RR )
262 fvex 5880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D `
 j )  e. 
_V
263262resex 5151 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D `  j )  |`  Y )  e.  _V
264263a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D `  j )  |`  Y )  e.  _V )
265264, 243ifcld 3926 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( D `  j )  |`  Y ) ,  F
)  e.  _V )
266265adantr 467 . . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j )  =  if ( S  e.  ( ( ( C `
 j ) `  Z ) [,) (
( D `  j
) `  Z )
) ,  ( ( D `  j )  |`  Y ) ,  F
) )
270269feq1d 5719 . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( K `
 j ) : Y --> RR )
272161, 219, 250, 271hoidmvcl 38414 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( J `  j ) ( L `  Y
) ( K `  j ) )  e.  ( 0 [,) +oo ) )
273218, 272eqeltrd 2531 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  ( 0 [,) +oo ) )
274159, 273sseldi 3432 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  ( P `
 j )  e.  RR )
275209, 211, 274syl2anc 667 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P `  j )  e.  RR )
276208, 275remulcld 9676 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( Q  -  S
)  x.  ( P `
 j ) )  e.  RR )
277207, 276fsumrecl 13812 . . . . . . . . 9  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
)  e.  RR )
278200, 277remulcld 9676 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S
)  x.  ( P `
 j ) ) )  e.  RR )
279206, 278readdcld 9675 . . . . . . 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 38421 . . . . . . . 8  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  Q
) `  ( D `  j ) ) ) ) )  e.  RR )
281200, 280remulcld 9676 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  Q ) `
 ( D `  j ) ) ) ) ) )  e.  RR )
28274, 68syl6eleq 2541 . . . . . . . . . 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 6302 . . . . . . . . . . . . 13  |-  ( z  =  S  ->  (
z  -  ( A `
 Z ) )  =  ( S  -  ( A `  Z ) ) )
284283oveq2d 6311 . . . . . . . . . . . 12  |-  ( z  =  S  ->  ( G  x.  ( z  -  ( A `  Z ) ) )  =  ( G  x.  ( S  -  ( A `  Z )
) ) )
285 fveq2 5870 . . . . . . . . . . . . . . . . 17  |-  ( z  =  S  ->  ( H `  z )  =  ( H `  S ) )
286285fveq1d 5872 . . . . . . . . . . . . . . . 16  |-  ( z  =  S  ->  (
( H `  z
) `  ( D `  j ) )  =  ( ( H `  S ) `  ( D `  j )
) )
287286oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( z  =  S  ->  (
( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) )  =  ( ( C `
 j ) ( L `  W ) ( ( H `  S ) `  ( D `  j )
) ) )
288287mpteq2dv 4493 . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . 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 6311 . . . . . . . . . . . 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 4418 . . . . . . . . . . 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 3198 . . . . . . . . . 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 200 . . . . . . . . 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 465 . . . . . . . 8  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
295207, 275fsumrecl 13812 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( P `  j
)  e.  RR )
296200, 295remulcld 9676 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  E )  x.  sum_ j  e.  ( 1 ... M ) ( P `  j ) )  e.  RR )
297 0red 9649 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  RR )
29875, 67posdifd 10207 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  <  Q  <->  0  <  ( Q  -  S ) ) )
299144, 298mpbid 214 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( Q  -  S ) )
300297, 183, 299ltled 9788 . . . . . . . . . 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 10553 . . . . . . . . 9  |-  ( ph  ->  ( G  x.  ( Q  -  S )
)  <_  ( (
( 1  +  E
)  x.  sum_ j  e.  ( 1 ... M
) ( P `  j ) )  x.  ( Q  -  S
) ) )
303200recnd 9674 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  +  E
)  e.  CC )
304295recnd 9674 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( P `  j
)  e.  CC )
305303, 304, 174mulassd 9671 . . . . . . . . . 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 9674 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P `  j )  e.  CC )
307207, 174, 306fsummulc1 13858 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ j  e.  ( 1 ... M ) ( P `  j
)  x.  ( Q  -  S ) )  =  sum_ j  e.  ( 1 ... M ) ( ( P `  j )  x.  ( Q  -  S )
) )
308174adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( Q  -  S )  e.  CC )
309306, 308mulcomd 9669 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( P `  j
)  x.  ( Q  -  S ) )  =  ( ( Q  -  S )  x.  ( P `  j
) ) )
310309sumeq2dv 13781 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( P `  j )  x.  ( Q  -  S )
)  =  sum_ j  e.  ( 1 ... M
) ( ( Q  -  S )  x.  ( P `  j
) ) )
311307, 310eqtrd 2487 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  ( 1 ... M ) ( P `  j
)  x.  ( Q  -  S ) )  =  sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
) )
312311oveq2d 6311 . . . . . . . . . 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 2487 . . . . . . . . 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 4430 . . . . . . . 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 37548 . . . . . . 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 37591 . . . . . . . . . . . . . . . . 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 3580 . . . . . . . . . . . . . . . . 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 2488 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ZZ>= `  ( M  +  1 ) )  u.  ( 1 ... M ) )  =  NN )
322321eqcomd 2459 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  =  ( (
ZZ>= `  ( M  + 
1 ) )  u.  ( 1 ... M
) ) )
323322mpteq1d 4487 . . . . . . . . . . . . 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 5874 . . . . . . . . . . . 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 1763 . . . . . . . . . . . . 13  |-  F/ j
ph
326 fvex 5880 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  ( M  +  1
) )  e.  _V
327326a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ZZ>= `  ( M  +  1 ) )  e.  _V )
328 ovex 6323 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  e. 
_V
329328a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  e.  _V )
330 incom 3627 . . . . . . . . . . . . . . 15  |-  ( (
ZZ>= `  ( M  + 
1 ) )  i^i  ( 1 ... M
) )  =  ( ( 1 ... M
)  i^i  ( ZZ>= `  ( M  +  1
) ) )
331 nnuzdisj 37588 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M )  i^i  ( ZZ>= `  ( M  +  1 ) ) )  =  (/)
332330, 331eqtri 2475 . . . . . . . . . . . . . 14  |-  ( (
ZZ>= `  ( M  + 
1 ) )  i^i  ( 1 ... M
) )  =  (/)
333332a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ZZ>= `  ( M  +  1 ) )  i^i  ( 1 ... M ) )  =  (/) )
334 icossicc 11728 . . . . . . . . . . . . . 14  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
335 ssid 3453 . . . . . . . . . . . . . . 15  |-  ( 0 [,) +oo )  C_  ( 0 [,) +oo )
336 simpl 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ph )
337316peano2nnd 10633 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M  +  1 )  e.  NN )
338 uznnssnn 11213 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  +  1 )  e.  NN  ->  ( ZZ>=
`  ( M  + 
1 ) )  C_  NN )
339337, 338syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ZZ>= `  ( M  +  1 ) ) 
C_  NN )
340339adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ZZ>= `  ( M  +  1
) )  C_  NN )
341 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  j  e.  ( ZZ>= `  ( M  +  1 ) ) )
342340, 341sseldd 3435 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  j  e.  NN )
343 snfi 7655 . . . . . . . . . . . . . . . . . . . . 21  |-  { Z }  e.  Fin
344343a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { Z }  e.  Fin )
345 unfi 7843 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Y  e.  Fin  /\  { Z }  e.  Fin )  ->  ( Y  u.  { Z } )  e. 
Fin )
346164, 344, 345syl2anc 667 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Y  u.  { Z } )  e.  Fin )
3477, 346syl5eqel 2535 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  W  e.  Fin )
348347adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  W  e. 
Fin )
349 eleq1 2519 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  l  ->  (
j  e.  Y  <->  l  e.  Y ) )
350 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  l  ->  (
c `  j )  =  ( c `  l ) )
351350breq1d 4415 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  l  ->  (
( c `  j
)  <_  x  <->  ( c `  l )  <_  x
) )
352351, 350ifbieq1d 3906 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  l  ->  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
)  =  if ( ( c `  l
)  <_  x , 
( c `  l
) ,  x ) )
353349, 350, 352ifbieq12d 3910 . . . . . . . . . . . . . . . . . . . . . 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 4498 . . . . . . . . . . . . . . . . . . . . 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 4489 . . . . . . . . . . . . . . . . . . . 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 4489 . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  S  e.  RR )
359357, 358, 348, 31hsphoif 38408 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( H `  S ) `
 ( D `  j ) ) : W --> RR )
360161, 348, 112, 359hoidmvcl 38414 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
361336, 342, 360syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( C `  j )
( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
362335, 361sseldi 3432 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( C `  j )
( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
363334, 362sseldi 3432 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( C `  j )
( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
364209, 211, 360syl2anc 667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  ( 0 [,) +oo ) )
365334, 364sseldi 3432 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  ( 0 [,] +oo ) )
366325, 327, 329, 333, 363, 365sge0splitmpt 38263 . . . . . . . . . . . 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 10622 . . . . . . . . . . . . . . 15  |-  NN  e.  _V
368367a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  e.  _V )
369334, 360sseldi 3432 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
370325, 368, 369, 205, 339sge0ssrempt 38257 . . . . . . . . . . . . 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 38257 . . . . . . . . . . . . 13  |-  ( ph  ->  (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  RR )
373 rexadd 11532 . . . . . . . . . . . . 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 667 . . . . . . . . . . . 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 2491 . . . . . . . . . . 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 6311 . . . . . . . . . 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 6310 . . . . . . . . 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 2532 . . . . . . . . . . . 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 9674 . . . . . . . . . . 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 9674 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( ( Q  -  S )  x.  ( P `  j )
)  e.  CC )
381303, 379, 380adddid 9672 . . . . . . . . . 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 2459 . . . . . . . . 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 9674 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  (
ZZ>= `  ( M  + 
1 ) )  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  e.  CC )
384372recnd 9674 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  CC )
385383, 384, 380addassd 9670 . . . . . . . . . . 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 38242 . . . . . . . . . . . . . 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 6310 . . . . . . . . . . . . 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 9601 . . . . . . . . . . . . . . . . . 18  |-  RR  C_  CC
389159, 388sstri 3443 . . . . . . . . . . . . . . . . 17  |-  ( 0 [,) +oo )  C_  CC
390389, 360sseldi 3432 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  CC )
391209, 211, 390syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  CC )
392183adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( Q  -  S )  e.  RR )
393392, 274remulcld 9676 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( Q  -  S )  x.  ( P `  j ) )  e.  RR )
394393recnd 9674 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( Q  -  S )  x.  ( P `  j ) )  e.  CC )
395211, 394syldan 473 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( Q  -  S
)  x.  ( P `
 j ) )  e.  CC )
396207, 391, 395fsumadd 13817 . . . . . . . . . . . . . 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 2459 . . . . . . . . . . . . 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 2487 . . . . . . . . . . . 12  |-  ( ph  ->  ( (Σ^ `  ( j  e.  ( 1 ... M ) 
|->  ( ( C `  j ) ( L `
 W ) (