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

Theorem hoidmvlelem1 38417
Description: The supremum of  U belongs to  U. Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvlelem1.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 )
) ) ) ) )
hoidmvlelem1.x  |-  ( ph  ->  X  e.  Fin )
hoidmvlelem1.y  |-  ( ph  ->  Y  C_  X )
hoidmvlelem1.z  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
hoidmvlelem1.w  |-  W  =  ( Y  u.  { Z } )
hoidmvlelem1.a  |-  ( ph  ->  A : W --> RR )
hoidmvlelem1.b  |-  ( ph  ->  B : W --> RR )
hoidmvlelem1.c  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
hoidmvlelem1.d  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
hoidmvlelem1.r  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
hoidmvlelem1.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
) ) ) ) )
hoidmvlelem1.g  |-  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
hoidmvlelem1.e  |-  ( ph  ->  E  e.  RR+ )
hoidmvlelem1.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 ) ) ) ) ) ) }
hoidmvlelem1.s  |-  S  =  sup ( U ,  RR ,  <  )
hoidmvlelem1.ab  |-  ( ph  ->  ( A `  Z
)  <  ( B `  Z ) )
Assertion
Ref Expression
hoidmvlelem1  |-  ( ph  ->  S  e.  U )
Distinct variable groups:    A, a,
b, j, k, x    A, c, j, k, x   
z, A, j    B, a, b, k    B, c   
z, B    C, a,
b, k    C, c    z, C    D, a, b, k    D, c    z, D    E, c    z, E    G, c    z, G    H, a, b, k    H, c    z, H    L, c    z, L    S, a,
b, j, k, x    S, c    z, S    U, a, b, j, k, x    U, c    z, U    W, a, b, j, k, x    W, c    z, W    Y, a, b, j, k, x    Y, c    Z, a, b, j, k, x    Z, c    z, Z    ph, a, b, j, k, x    ph, c
Allowed substitution hints:    ph( z)    B( x, j)    C( x, j)    D( x, j)    E( x, j, k, a, b)    G( x, j, k, a, b)    H( x, j)    L( x, j, k, a, b)    X( x, z, j, k, a, b, c)    Y( z)

Proof of Theorem hoidmvlelem1
Dummy variables  u  h  r  s  t 
v  w  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmvlelem1.s . . . . . 6  |-  S  =  sup ( U ,  RR ,  <  )
21a1i 11 . . . . 5  |-  ( ph  ->  S  =  sup ( U ,  RR ,  <  ) )
3 hoidmvlelem1.a . . . . . . 7  |-  ( ph  ->  A : W --> RR )
4 hoidmvlelem1.z . . . . . . . . . 10  |-  ( ph  ->  Z  e.  ( X 
\  Y ) )
5 snidg 3994 . . . . . . . . . 10  |-  ( Z  e.  ( X  \  Y )  ->  Z  e.  { Z } )
64, 5syl 17 . . . . . . . . 9  |-  ( ph  ->  Z  e.  { Z } )
7 elun2 3602 . . . . . . . . 9  |-  ( Z  e.  { Z }  ->  Z  e.  ( Y  u.  { Z }
) )
86, 7syl 17 . . . . . . . 8  |-  ( ph  ->  Z  e.  ( Y  u.  { Z }
) )
9 hoidmvlelem1.w . . . . . . . 8  |-  W  =  ( Y  u.  { Z } )
108, 9syl6eleqr 2540 . . . . . . 7  |-  ( ph  ->  Z  e.  W )
113, 10ffvelrnd 6023 . . . . . 6  |-  ( ph  ->  ( A `  Z
)  e.  RR )
12 hoidmvlelem1.b . . . . . . 7  |-  ( ph  ->  B : W --> RR )
1312, 10ffvelrnd 6023 . . . . . 6  |-  ( ph  ->  ( B `  Z
)  e.  RR )
14 hoidmvlelem1.u . . . . . . . 8  |-  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 ) ) ) ) ) ) }
15 ssrab2 3514 . . . . . . . 8  |-  { 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
) )
1614, 15eqsstri 3462 . . . . . . 7  |-  U  C_  ( ( A `  Z ) [,] ( B `  Z )
)
1716a1i 11 . . . . . 6  |-  ( ph  ->  U  C_  ( ( A `  Z ) [,] ( B `  Z
) ) )
1811leidd 10180 . . . . . . . . . . 11  |-  ( ph  ->  ( A `  Z
)  <_  ( A `  Z ) )
19 hoidmvlelem1.ab . . . . . . . . . . . 12  |-  ( ph  ->  ( A `  Z
)  <  ( B `  Z ) )
2011, 13, 19ltled 9783 . . . . . . . . . . 11  |-  ( ph  ->  ( A `  Z
)  <_  ( B `  Z ) )
2111, 13, 11, 18, 20eliccd 37601 . . . . . . . . . 10  |-  ( ph  ->  ( A `  Z
)  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
2211recnd 9669 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A `  Z
)  e.  CC )
2322subidd 9974 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  Z )  -  ( A `  Z )
)  =  0 )
2423oveq2d 6306 . . . . . . . . . . . 12  |-  ( ph  ->  ( G  x.  (
( A `  Z
)  -  ( A `
 Z ) ) )  =  ( G  x.  0 ) )
25 rge0ssre 11740 . . . . . . . . . . . . . . 15  |-  ( 0 [,) +oo )  C_  RR
26 hoidmvlelem1.g . . . . . . . . . . . . . . . 16  |-  G  =  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)
27 hoidmvlelem1.l . . . . . . . . . . . . . . . . 17  |-  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 )
) ) ) ) )
28 hoidmvlelem1.x . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  X  e.  Fin )
29 hoidmvlelem1.y . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Y  C_  X )
3028, 29ssfid 37414 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Y  e.  Fin )
31 ssun1 3597 . . . . . . . . . . . . . . . . . . . 20  |-  Y  C_  ( Y  u.  { Z } )
3231, 9sseqtr4i 3465 . . . . . . . . . . . . . . . . . . 19  |-  Y  C_  W
3332a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Y  C_  W )
343, 33fssresd 5750 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  |`  Y ) : Y --> RR )
3512, 33fssresd 5750 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  |`  Y ) : Y --> RR )
3627, 30, 34, 35hoidmvcl 38404 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  |`  Y ) ( L `
 Y ) ( B  |`  Y )
)  e.  ( 0 [,) +oo ) )
3726, 36syl5eqel 2533 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e.  ( 0 [,) +oo ) )
3825, 37sseldi 3430 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  e.  RR )
3938recnd 9669 . . . . . . . . . . . . 13  |-  ( ph  ->  G  e.  CC )
4039mul01d 9832 . . . . . . . . . . . 12  |-  ( ph  ->  ( G  x.  0 )  =  0 )
4124, 40eqtrd 2485 . . . . . . . . . . 11  |-  ( ph  ->  ( G  x.  (
( A `  Z
)  -  ( A `
 Z ) ) )  =  0 )
42 1red 9658 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  RR )
43 hoidmvlelem1.e . . . . . . . . . . . . . 14  |-  ( ph  ->  E  e.  RR+ )
4443rpred 11341 . . . . . . . . . . . . 13  |-  ( ph  ->  E  e.  RR )
4542, 44readdcld 9670 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
46 0red 9644 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  RR )
47 0lt1 10136 . . . . . . . . . . . . . . 15  |-  0  <  1
4847a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  1 )
4942, 43ltaddrpd 11371 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  <  ( 1  +  E ) )
5046, 42, 45, 48, 49lttrd 9796 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 1  +  E ) )
5146, 45, 50ltled 9783 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( 1  +  E ) )
52 nnex 10615 . . . . . . . . . . . . . . 15  |-  NN  e.  _V
5352a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  e.  _V )
54 icossicc 11721 . . . . . . . . . . . . . . . 16  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
55 snfi 7650 . . . . . . . . . . . . . . . . . . . . 21  |-  { Z }  e.  Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { Z }  e.  Fin )
57 unfi 7838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Y  e.  Fin  /\  { Z }  e.  Fin )  ->  ( Y  u.  { Z } )  e. 
Fin )
5830, 56, 57syl2anc 667 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Y  u.  { Z } )  e.  Fin )
599, 58syl5eqel 2533 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  W  e.  Fin )
6059adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  W  e. 
Fin )
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  C : NN --> ( RR 
^m  W ) )
6261ffvelrnda 6022 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j )  e.  ( RR  ^m  W
) )
63 elmapi 7493 . . . . . . . . . . . . . . . . . 18  |-  ( ( C `  j )  e.  ( RR  ^m  W )  ->  ( C `  j ) : W --> RR )
6462, 63syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( C `
 j ) : W --> RR )
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19  |-  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
) ) ) ) )
66 eleq1 2517 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  h  ->  (
j  e.  Y  <->  h  e.  Y ) )
67 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  h  ->  (
c `  j )  =  ( c `  h ) )
6867breq1d 4412 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  h  ->  (
( c `  j
)  <_  x  <->  ( c `  h )  <_  x
) )
6968, 67ifbieq1d 3904 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  h  ->  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
)  =  if ( ( c `  h
)  <_  x , 
( c `  h
) ,  x ) )
7066, 67, 69ifbieq12d 3908 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  h  ->  if ( j  e.  Y ,  ( c `  j ) ,  if ( ( c `  j )  <_  x ,  ( c `  j ) ,  x
) )  =  if ( h  e.  Y ,  ( c `  h ) ,  if ( ( c `  h )  <_  x ,  ( c `  h ) ,  x
) ) )
7170cbvmptv 4495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  W  |->  if ( j  e.  Y , 
( c `  j
) ,  if ( ( c `  j
)  <_  x , 
( c `  j
) ,  x ) ) )  =  ( h  e.  W  |->  if ( h  e.  Y ,  ( c `  h ) ,  if ( ( c `  h )  <_  x ,  ( c `  h ) ,  x
) ) )
7271mpteq2i 4486 . . . . . . . . . . . . . . . . . . . 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 ) 
|->  ( h  e.  W  |->  if ( h  e.  Y ,  ( c `
 h ) ,  if ( ( c `
 h )  <_  x ,  ( c `  h ) ,  x
) ) ) )
7372mpteq2i 4486 . . . . . . . . . . . . . . . . . . 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
)  |->  ( h  e.  W  |->  if ( h  e.  Y ,  ( c `  h ) ,  if ( ( c `  h )  <_  x ,  ( c `  h ) ,  x ) ) ) ) )
7465, 73eqtri 2473 . . . . . . . . . . . . . . . . . 18  |-  H  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  W ) 
|->  ( h  e.  W  |->  if ( h  e.  Y ,  ( c `
 h ) ,  if ( ( c `
 h )  <_  x ,  ( c `  h ) ,  x
) ) ) ) )
7511adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( A `
 Z )  e.  RR )
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  D : NN --> ( RR 
^m  W ) )
7776ffvelrnda 6022 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j )  e.  ( RR  ^m  W
) )
78 elmapi 7493 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D `  j )  e.  ( RR  ^m  W )  ->  ( D `  j ) : W --> RR )
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( D `
 j ) : W --> RR )
8074, 75, 60, 79hsphoif 38398 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( H `  ( A `
 Z ) ) `
 ( D `  j ) ) : W --> RR )
8127, 60, 64, 80hoidmvcl 38404 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 ( A `  Z ) ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
8254, 81sseldi 3430 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 ( A `  Z ) ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
83 eqid 2451 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( H `
 ( A `  Z ) ) `  ( D `  j ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) )
8482, 83fmptd 6046 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) : NN --> ( 0 [,] +oo ) )
8553, 84sge0cl 38223 . . . . . . . . . . . . 13  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  e.  ( 0 [,] +oo )
)
8653, 84sge0xrcl 38227 . . . . . . . . . . . . . 14  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  e.  RR* )
87 pnfxr 11412 . . . . . . . . . . . . . . 15  |- +oo  e.  RR*
8887a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  -> +oo  e.  RR* )
89 hoidmvlelem1.r . . . . . . . . . . . . . . . 16  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e.  RR )
9089rexrd 9690 . . . . . . . . . . . . . . 15  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  e. 
RR* )
91 nfv 1761 . . . . . . . . . . . . . . . 16  |-  F/ j
ph
9227, 60, 64, 79hoidmvcl 38404 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( D `  j ) )  e.  ( 0 [,) +oo ) )
9354, 92sseldi 3430 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( D `  j ) )  e.  ( 0 [,] +oo ) )
944eldifbd 3417 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  Z  e.  Y
)
9510, 94eldifd 3415 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Z  e.  ( W 
\  Y ) )
9695adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  Z  e.  ( W  \  Y
) )
9727, 60, 96, 9, 75, 74, 64, 79hsphoidmvle 38408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 ( A `  Z ) ) `  ( D `  j ) ) )  <_  (
( C `  j
) ( L `  W ) ( D `
 j ) ) )
9891, 53, 82, 93, 97sge0lempt 38252 . . . . . . . . . . . . . . 15  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) ) )
9989ltpnfd 11423 . . . . . . . . . . . . . . 15  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( D `  j ) ) ) )  < +oo )
10086, 90, 88, 98, 99xrlelttrd 11457 . . . . . . . . . . . . . 14  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  < +oo )
10186, 88, 100xrltned 37580 . . . . . . . . . . . . 13  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  =/= +oo )
102 ge0xrre 37633 . . . . . . . . . . . . 13  |-  ( ( (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  e.  ( 0 [,] +oo )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  =/= +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  e.  RR )
10385, 101, 102syl2anc 667 . . . . . . . . . . . 12  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  e.  RR )
10453, 84sge0ge0 38226 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) )
105 mulge0 10132 . . . . . . . . . . . 12  |-  ( ( ( ( 1  +  E )  e.  RR  /\  0  <_  ( 1  +  E ) )  /\  ( (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) )  e.  RR  /\  0  <_  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) )  ->  0  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) )
10645, 51, 103, 104, 105syl22anc 1269 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) )
10741, 106eqbrtrd 4423 . . . . . . . . . 10  |-  ( ph  ->  ( G  x.  (
( A `  Z
)  -  ( A `
 Z ) ) )  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) )
10821, 107jca 535 . . . . . . . . 9  |-  ( ph  ->  ( ( A `  Z )  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  /\  ( G  x.  ( ( A `  Z )  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) ) )
109 oveq1 6297 . . . . . . . . . . . 12  |-  ( z  =  ( A `  Z )  ->  (
z  -  ( A `
 Z ) )  =  ( ( A `
 Z )  -  ( A `  Z ) ) )
110109oveq2d 6306 . . . . . . . . . . 11  |-  ( z  =  ( A `  Z )  ->  ( G  x.  ( z  -  ( A `  Z ) ) )  =  ( G  x.  ( ( A `  Z )  -  ( A `  Z )
) ) )
111 fveq2 5865 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( A `  Z )  ->  ( H `  z )  =  ( H `  ( A `  Z ) ) )
112111fveq1d 5867 . . . . . . . . . . . . . . 15  |-  ( z  =  ( A `  Z )  ->  (
( H `  z
) `  ( D `  j ) )  =  ( ( H `  ( A `  Z ) ) `  ( D `
 j ) ) )
113112oveq2d 6306 . . . . . . . . . . . . . 14  |-  ( z  =  ( A `  Z )  ->  (
( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) )  =  ( ( C `
 j ) ( L `  W ) ( ( H `  ( A `  Z ) ) `  ( D `
 j ) ) ) )
114113mpteq2dv 4490 . . . . . . . . . . . . 13  |-  ( z  =  ( A `  Z )  ->  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( H `
 ( A `  Z ) ) `  ( D `  j ) ) ) ) )
115114fveq2d 5869 . . . . . . . . . . . 12  |-  ( z  =  ( A `  Z )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) ) ) )  =  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  ( A `
 Z ) ) `
 ( D `  j ) ) ) ) ) )
116115oveq2d 6306 . . . . . . . . . . 11  |-  ( z  =  ( A `  Z )  ->  (
( 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 `  ( A `
 Z ) ) `
 ( D `  j ) ) ) ) ) ) )
117110, 116breq12d 4415 . . . . . . . . . 10  |-  ( z  =  ( A `  Z )  ->  (
( G  x.  (
z  -  ( A `
 Z ) ) )  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) )  <->  ( G  x.  ( ( A `  Z )  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) ) )
118117elrab 3196 . . . . . . . . 9  |-  ( ( A `  Z )  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 ) ) ) ) ) ) }  <-> 
( ( A `  Z )  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  /\  ( G  x.  ( ( A `  Z )  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  ( A `  Z )
) `  ( D `  j ) ) ) ) ) ) ) )
119108, 118sylibr 216 . . . . . . . 8  |-  ( ph  ->  ( A `  Z
)  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 ) ) ) ) ) ) } )
120119, 14syl6eleqr 2540 . . . . . . 7  |-  ( ph  ->  ( A `  Z
)  e.  U )
121 ne0i 3737 . . . . . . 7  |-  ( ( A `  Z )  e.  U  ->  U  =/=  (/) )
122120, 121syl 17 . . . . . 6  |-  ( ph  ->  U  =/=  (/) )
12311, 13, 17, 122supicc 11780 . . . . 5  |-  ( ph  ->  sup ( U ,  RR ,  <  )  e.  ( ( A `  Z ) [,] ( B `  Z )
) )
1242, 123eqeltrd 2529 . . . 4  |-  ( ph  ->  S  e.  ( ( A `  Z ) [,] ( B `  Z ) ) )
1252oveq1d 6305 . . . . . . 7  |-  ( ph  ->  ( S  -  ( A `  Z )
)  =  ( sup ( U ,  RR ,  <  )  -  ( A `  Z )
) )
126125oveq2d 6306 . . . . . 6  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  =  ( G  x.  ( sup ( U ,  RR ,  <  )  -  ( A `  Z ) ) ) )
12711, 13iccssred 37602 . . . . . . . . 9  |-  ( ph  ->  ( ( A `  Z ) [,] ( B `  Z )
)  C_  RR )
12817, 127sstrd 3442 . . . . . . . 8  |-  ( ph  ->  U  C_  RR )
12911, 13jca 535 . . . . . . . . . 10  |-  ( ph  ->  ( ( A `  Z )  e.  RR  /\  ( B `  Z
)  e.  RR ) )
130 iccsupr 11727 . . . . . . . . . 10  |-  ( ( ( ( A `  Z )  e.  RR  /\  ( B `  Z
)  e.  RR )  /\  U  C_  (
( A `  Z
) [,] ( B `
 Z ) )  /\  ( A `  Z )  e.  U
)  ->  ( U  C_  RR  /\  U  =/=  (/)  /\  E. y  e.  RR  A. z  e.  U  z  <_  y
) )
131129, 17, 120, 130syl3anc 1268 . . . . . . . . 9  |-  ( ph  ->  ( U  C_  RR  /\  U  =/=  (/)  /\  E. y  e.  RR  A. z  e.  U  z  <_  y ) )
132131simp3d 1022 . . . . . . . 8  |-  ( ph  ->  E. y  e.  RR  A. z  e.  U  z  <_  y )
133 eqid 2451 . . . . . . . 8  |-  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  =  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }
134128, 122, 132, 11, 133supsubc 37576 . . . . . . 7  |-  ( ph  ->  ( sup ( U ,  RR ,  <  )  -  ( A `  Z ) )  =  sup ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } ,  RR ,  <  ) )
135134oveq2d 6306 . . . . . 6  |-  ( ph  ->  ( G  x.  ( sup ( U ,  RR ,  <  )  -  ( A `  Z )
) )  =  ( G  x.  sup ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } ,  RR ,  <  ) ) )
13646rexrd 9690 . . . . . . . 8  |-  ( ph  ->  0  e.  RR* )
137 icogelb 11686 . . . . . . . 8  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  G  e.  ( 0 [,) +oo ) )  ->  0  <_  G )
138136, 88, 37, 137syl3anc 1268 . . . . . . 7  |-  ( ph  ->  0  <_  G )
139 vex 3048 . . . . . . . . . . . 12  |-  r  e. 
_V
140 eqeq1 2455 . . . . . . . . . . . . 13  |-  ( w  =  r  ->  (
w  =  ( u  -  ( A `  Z ) )  <->  r  =  ( u  -  ( A `  Z )
) ) )
141140rexbidv 2901 . . . . . . . . . . . 12  |-  ( w  =  r  ->  ( E. u  e.  U  w  =  ( u  -  ( A `  Z ) )  <->  E. u  e.  U  r  =  ( u  -  ( A `  Z )
) ) )
142139, 141elab 3185 . . . . . . . . . . 11  |-  ( r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  <->  E. u  e.  U  r  =  ( u  -  ( A `  Z ) ) )
143142biimpi 198 . . . . . . . . . 10  |-  ( r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  ->  E. u  e.  U  r  =  ( u  -  ( A `  Z ) ) )
144143adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  ->  E. u  e.  U  r  =  ( u  -  ( A `  Z ) ) )
145 nfv 1761 . . . . . . . . . . 11  |-  F/ u ph
146 nfcv 2592 . . . . . . . . . . . 12  |-  F/_ u
r
147 nfre1 2848 . . . . . . . . . . . . 13  |-  F/ u E. u  e.  U  w  =  ( u  -  ( A `  Z ) )
148147nfab 2596 . . . . . . . . . . . 12  |-  F/_ u { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }
149146, 148nfel 2604 . . . . . . . . . . 11  |-  F/ u  r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }
150145, 149nfan 2011 . . . . . . . . . 10  |-  F/ u
( ph  /\  r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } )
151 nfv 1761 . . . . . . . . . 10  |-  F/ u
0  <_  r
15211rexrd 9690 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A `  Z
)  e.  RR* )
153152adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  ( A `  Z )  e.  RR* )
15413rexrd 9690 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B `  Z
)  e.  RR* )
155154adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  ( B `  Z )  e.  RR* )
15617sselda 3432 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  u  e.  ( ( A `  Z ) [,] ( B `  Z )
) )
157 iccgelb 11691 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  Z
)  e.  RR*  /\  ( B `  Z )  e.  RR*  /\  u  e.  ( ( A `  Z ) [,] ( B `  Z )
) )  ->  ( A `  Z )  <_  u )
158153, 155, 156, 157syl3anc 1268 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( A `  Z )  <_  u )
159128sselda 3432 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  u  e.  RR )
16011adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  ( A `  Z )  e.  RR )
161159, 160subge0d 10203 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  (
0  <_  ( u  -  ( A `  Z ) )  <->  ( A `  Z )  <_  u
) )
162158, 161mpbird 236 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  0  <_  ( u  -  ( A `  Z )
) )
1631623adant3 1028 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  U  /\  r  =  ( u  -  ( A `
 Z ) ) )  ->  0  <_  ( u  -  ( A `
 Z ) ) )
164 id 22 . . . . . . . . . . . . . . 15  |-  ( r  =  ( u  -  ( A `  Z ) )  ->  r  =  ( u  -  ( A `  Z )
) )
165164eqcomd 2457 . . . . . . . . . . . . . 14  |-  ( r  =  ( u  -  ( A `  Z ) )  ->  ( u  -  ( A `  Z ) )  =  r )
1661653ad2ant3 1031 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  U  /\  r  =  ( u  -  ( A `
 Z ) ) )  ->  ( u  -  ( A `  Z ) )  =  r )
167163, 166breqtrd 4427 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U  /\  r  =  ( u  -  ( A `
 Z ) ) )  ->  0  <_  r )
1681673exp 1207 . . . . . . . . . . 11  |-  ( ph  ->  ( u  e.  U  ->  ( r  =  ( u  -  ( A `
 Z ) )  ->  0  <_  r
) ) )
169168adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
( u  e.  U  ->  ( r  =  ( u  -  ( A `
 Z ) )  ->  0  <_  r
) ) )
170150, 151, 169rexlimd 2871 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
( E. u  e.  U  r  =  ( u  -  ( A `
 Z ) )  ->  0  <_  r
) )
171144, 170mpd 15 . . . . . . . 8  |-  ( (
ph  /\  r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
0  <_  r )
172171ralrimiva 2802 . . . . . . 7  |-  ( ph  ->  A. r  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } 0  <_ 
r )
173 simp3 1010 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U  /\  w  =  ( u  -  ( A `
 Z ) ) )  ->  w  =  ( u  -  ( A `  Z )
) )
174159, 160resubcld 10047 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  U )  ->  (
u  -  ( A `
 Z ) )  e.  RR )
1751743adant3 1028 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U  /\  w  =  ( u  -  ( A `
 Z ) ) )  ->  ( u  -  ( A `  Z ) )  e.  RR )
176173, 175eqeltrd 2529 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U  /\  w  =  ( u  -  ( A `
 Z ) ) )  ->  w  e.  RR )
1771763exp 1207 . . . . . . . . . 10  |-  ( ph  ->  ( u  e.  U  ->  ( w  =  ( u  -  ( A `
 Z ) )  ->  w  e.  RR ) ) )
178177rexlimdv 2877 . . . . . . . . 9  |-  ( ph  ->  ( E. u  e.  U  w  =  ( u  -  ( A `
 Z ) )  ->  w  e.  RR ) )
179178alrimiv 1773 . . . . . . . 8  |-  ( ph  ->  A. w ( E. u  e.  U  w  =  ( u  -  ( A `  Z ) )  ->  w  e.  RR ) )
180 abss 3498 . . . . . . . 8  |-  ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) }  C_  RR  <->  A. w ( E. u  e.  U  w  =  ( u  -  ( A `  Z )
)  ->  w  e.  RR ) )
181179, 180sylibr 216 . . . . . . 7  |-  ( ph  ->  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  C_  RR )
18223eqcomd 2457 . . . . . . . . . 10  |-  ( ph  ->  0  =  ( ( A `  Z )  -  ( A `  Z ) ) )
183 oveq1 6297 . . . . . . . . . . . 12  |-  ( u  =  ( A `  Z )  ->  (
u  -  ( A `
 Z ) )  =  ( ( A `
 Z )  -  ( A `  Z ) ) )
184183eqeq2d 2461 . . . . . . . . . . 11  |-  ( u  =  ( A `  Z )  ->  (
0  =  ( u  -  ( A `  Z ) )  <->  0  =  ( ( A `  Z )  -  ( A `  Z )
) ) )
185184rspcev 3150 . . . . . . . . . 10  |-  ( ( ( A `  Z
)  e.  U  /\  0  =  ( ( A `  Z )  -  ( A `  Z ) ) )  ->  E. u  e.  U 
0  =  ( u  -  ( A `  Z ) ) )
186120, 182, 185syl2anc 667 . . . . . . . . 9  |-  ( ph  ->  E. u  e.  U 
0  =  ( u  -  ( A `  Z ) ) )
187 c0ex 9637 . . . . . . . . . 10  |-  0  e.  _V
188 eqeq1 2455 . . . . . . . . . . 11  |-  ( w  =  0  ->  (
w  =  ( u  -  ( A `  Z ) )  <->  0  =  ( u  -  ( A `  Z )
) ) )
189188rexbidv 2901 . . . . . . . . . 10  |-  ( w  =  0  ->  ( E. u  e.  U  w  =  ( u  -  ( A `  Z ) )  <->  E. u  e.  U  0  =  ( u  -  ( A `  Z )
) ) )
190187, 189elab 3185 . . . . . . . . 9  |-  ( 0  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  <->  E. u  e.  U 
0  =  ( u  -  ( A `  Z ) ) )
191186, 190sylibr 216 . . . . . . . 8  |-  ( ph  ->  0  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } )
192 ne0i 3737 . . . . . . . 8  |-  ( 0  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  ->  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  =/=  (/) )
193191, 192syl 17 . . . . . . 7  |-  ( ph  ->  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  =/=  (/) )
19413, 11resubcld 10047 . . . . . . . 8  |-  ( ph  ->  ( ( B `  Z )  -  ( A `  Z )
)  e.  RR )
195 vex 3048 . . . . . . . . . . . . 13  |-  s  e. 
_V
196 eqeq1 2455 . . . . . . . . . . . . . 14  |-  ( w  =  s  ->  (
w  =  ( u  -  ( A `  Z ) )  <->  s  =  ( u  -  ( A `  Z )
) ) )
197196rexbidv 2901 . . . . . . . . . . . . 13  |-  ( w  =  s  ->  ( E. u  e.  U  w  =  ( u  -  ( A `  Z ) )  <->  E. u  e.  U  s  =  ( u  -  ( A `  Z )
) ) )
198195, 197elab 3185 . . . . . . . . . . . 12  |-  ( s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  <->  E. u  e.  U  s  =  ( u  -  ( A `  Z ) ) )
199198biimpi 198 . . . . . . . . . . 11  |-  ( s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  ->  E. u  e.  U  s  =  ( u  -  ( A `  Z ) ) )
200199adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  ->  E. u  e.  U  s  =  ( u  -  ( A `  Z ) ) )
201 nfcv 2592 . . . . . . . . . . . . 13  |-  F/_ u
s
202201, 148nfel 2604 . . . . . . . . . . . 12  |-  F/ u  s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }
203145, 202nfan 2011 . . . . . . . . . . 11  |-  F/ u
( ph  /\  s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } )
204 nfv 1761 . . . . . . . . . . 11  |-  F/ u  s  <_  ( ( B `
 Z )  -  ( A `  Z ) )
205 simp3 1010 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  s  =  ( u  -  ( A `  Z )
) )
2061603adant3 1028 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  ( A `  Z )  e.  RR )
207133ad2ant1 1029 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  ( B `  Z )  e.  RR )
2081563adant3 1028 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  u  e.  ( ( A `  Z ) [,] ( B `  Z )
) )
209213ad2ant1 1029 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  ( A `  Z )  e.  ( ( A `  Z
) [,] ( B `
 Z ) ) )
210206, 207, 208, 209iccsuble 37620 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  ( u  -  ( A `  Z ) )  <_ 
( ( B `  Z )  -  ( A `  Z )
) )
211205, 210eqbrtrd 4423 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  U  /\  s  =  ( u  -  ( A `
 Z ) ) )  ->  s  <_  ( ( B `  Z
)  -  ( A `
 Z ) ) )
2122113exp 1207 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  U  ->  ( s  =  ( u  -  ( A `
 Z ) )  ->  s  <_  (
( B `  Z
)  -  ( A `
 Z ) ) ) ) )
213212adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
( u  e.  U  ->  ( s  =  ( u  -  ( A `
 Z ) )  ->  s  <_  (
( B `  Z
)  -  ( A `
 Z ) ) ) ) )
214203, 204, 213rexlimd 2871 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
( E. u  e.  U  s  =  ( u  -  ( A `
 Z ) )  ->  s  <_  (
( B `  Z
)  -  ( A `
 Z ) ) ) )
215200, 214mpd 15 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
s  <_  ( ( B `  Z )  -  ( A `  Z ) ) )
216215ralrimiva 2802 . . . . . . . 8  |-  ( ph  ->  A. s  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } s  <_ 
( ( B `  Z )  -  ( A `  Z )
) )
217 breq2 4406 . . . . . . . . . 10  |-  ( r  =  ( ( B `
 Z )  -  ( A `  Z ) )  ->  ( s  <_  r  <->  s  <_  (
( B `  Z
)  -  ( A `
 Z ) ) ) )
218217ralbidv 2827 . . . . . . . . 9  |-  ( r  =  ( ( B `
 Z )  -  ( A `  Z ) )  ->  ( A. s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_  r  <->  A. s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_ 
( ( B `  Z )  -  ( A `  Z )
) ) )
219218rspcev 3150 . . . . . . . 8  |-  ( ( ( ( B `  Z )  -  ( A `  Z )
)  e.  RR  /\  A. s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_  ( ( B `  Z )  -  ( A `  Z ) ) )  ->  E. r  e.  RR  A. s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_  r )
220194, 216, 219syl2anc 667 . . . . . . 7  |-  ( ph  ->  E. r  e.  RR  A. s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_  r )
221 eqid 2451 . . . . . . . 8  |-  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) }  =  {
v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) }
222 biid 240 . . . . . . . 8  |-  ( ( ( G  e.  RR  /\  0  <_  G  /\  A. r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 0  <_  r )  /\  ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 
C_  RR  /\  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  =/=  (/)  /\  E. r  e.  RR  A. s  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_ 
r ) )  <->  ( ( G  e.  RR  /\  0  <_  G  /\  A. r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 0  <_ 
r )  /\  ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  C_  RR  /\ 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  =/=  (/)  /\  E. r  e.  RR  A. s  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_ 
r ) ) )
223221, 222supmul1 10576 . . . . . . 7  |-  ( ( ( G  e.  RR  /\  0  <_  G  /\  A. r  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 0  <_  r )  /\  ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 
C_  RR  /\  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  =/=  (/)  /\  E. r  e.  RR  A. s  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } s  <_ 
r ) )  -> 
( G  x.  sup ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } ,  RR ,  <  ) )  =  sup ( { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } ,  RR ,  <  ) )
22438, 138, 172, 181, 193, 220, 223syl33anc 1283 . . . . . 6  |-  ( ph  ->  ( G  x.  sup ( { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } ,  RR ,  <  ) )  =  sup ( { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } ,  RR ,  <  ) )
225126, 135, 2243eqtrd 2489 . . . . 5  |-  ( ph  ->  ( G  x.  ( S  -  ( A `  Z ) ) )  =  sup ( { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } ,  RR ,  <  ) )
226 vex 3048 . . . . . . . . . . . 12  |-  c  e. 
_V
227 eqeq1 2455 . . . . . . . . . . . . 13  |-  ( v  =  c  ->  (
v  =  ( G  x.  t )  <->  c  =  ( G  x.  t
) ) )
228227rexbidv 2901 . . . . . . . . . . . 12  |-  ( v  =  c  ->  ( E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t )  <->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t
) ) )
229226, 228elab 3185 . . . . . . . . . . 11  |-  ( c  e.  { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  <->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t
) )
230229biimpi 198 . . . . . . . . . 10  |-  ( c  e.  { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  ->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t
) )
231 nfv 1761 . . . . . . . . . . . 12  |-  F/ t E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z )
) )
232 vex 3048 . . . . . . . . . . . . . . . . 17  |-  t  e. 
_V
233 eqeq1 2455 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  t  ->  (
w  =  ( u  -  ( A `  Z ) )  <->  t  =  ( u  -  ( A `  Z )
) ) )
234233rexbidv 2901 . . . . . . . . . . . . . . . . 17  |-  ( w  =  t  ->  ( E. u  e.  U  w  =  ( u  -  ( A `  Z ) )  <->  E. u  e.  U  t  =  ( u  -  ( A `  Z )
) ) )
235232, 234elab 3185 . . . . . . . . . . . . . . . 16  |-  ( t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  <->  E. u  e.  U  t  =  ( u  -  ( A `  Z ) ) )
236235biimpi 198 . . . . . . . . . . . . . . 15  |-  ( t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  ->  E. u  e.  U  t  =  ( u  -  ( A `  Z ) ) )
237236adantr 467 . . . . . . . . . . . . . 14  |-  ( ( t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  /\  c  =  ( G  x.  t ) )  ->  E. u  e.  U  t  =  ( u  -  ( A `  Z )
) )
238 simpl 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( G  x.  t )  /\  t  =  ( u  -  ( A `  Z ) ) )  ->  c  =  ( G  x.  t ) )
239 oveq2 6298 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  ( u  -  ( A `  Z ) )  ->  ( G  x.  t )  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )
240239adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  ( G  x.  t )  /\  t  =  ( u  -  ( A `  Z ) ) )  ->  ( G  x.  t )  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )
241238, 240eqtrd 2485 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  ( G  x.  t )  /\  t  =  ( u  -  ( A `  Z ) ) )  ->  c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )
242241ex 436 . . . . . . . . . . . . . . . 16  |-  ( c  =  ( G  x.  t )  ->  (
t  =  ( u  -  ( A `  Z ) )  -> 
c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) ) )
243242reximdv 2861 . . . . . . . . . . . . . . 15  |-  ( c  =  ( G  x.  t )  ->  ( E. u  e.  U  t  =  ( u  -  ( A `  Z ) )  ->  E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z )
) ) ) )
244243adantl 468 . . . . . . . . . . . . . 14  |-  ( ( t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  /\  c  =  ( G  x.  t ) )  ->  ( E. u  e.  U  t  =  ( u  -  ( A `  Z ) )  ->  E. u  e.  U  c  =  ( G  x.  (
u  -  ( A `
 Z ) ) ) ) )
245237, 244mpd 15 . . . . . . . . . . . . 13  |-  ( ( t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  /\  c  =  ( G  x.  t ) )  ->  E. u  e.  U  c  =  ( G  x.  (
u  -  ( A `
 Z ) ) ) )
246245ex 436 . . . . . . . . . . . 12  |-  ( t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  ->  ( c  =  ( G  x.  t
)  ->  E. u  e.  U  c  =  ( G  x.  (
u  -  ( A `
 Z ) ) ) ) )
247231, 246rexlimi 2869 . . . . . . . . . . 11  |-  ( E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t )  ->  E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z )
) ) )
248247a1i 11 . . . . . . . . . 10  |-  ( c  e.  { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  ->  ( E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t )  ->  E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z )
) ) ) )
249230, 248mpd 15 . . . . . . . . 9  |-  ( c  e.  { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  ->  E. u  e.  U  c  =  ( G  x.  (
u  -  ( A `
 Z ) ) ) )
250249adantl 468 . . . . . . . 8  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  ->  E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z )
) ) )
251 simp3 1010 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U  /\  c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )  ->  c  =  ( G  x.  (
u  -  ( A `
 Z ) ) ) )
25238adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  G  e.  RR )
253252, 174remulcld 9671 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  ( G  x.  ( u  -  ( A `  Z ) ) )  e.  RR )
25445adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  (
1  +  E )  e.  RR )
25552a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  ->  NN  e.  _V )
25660adantlr 721 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  W  e.  Fin )
25764adantlr 721 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  ( C `  j ) : W --> RR )
258159adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  u  e.  RR )
25979adantlr 721 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  ( D `  j ) : W --> RR )
26074, 258, 256, 259hsphoif 38398 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( H `  u
) `  ( D `  j ) ) : W --> RR )
26127, 256, 257, 260hoidmvcl 38404 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) )  e.  ( 0 [,) +oo ) )
26254, 261sseldi 3430 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) )  e.  ( 0 [,] +oo ) )
263 eqid 2451 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( H `
 u ) `  ( D `  j ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) )
264262, 263fmptd 6046 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  ->  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) : NN --> ( 0 [,] +oo ) )
265255, 264sge0cl 38223 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  e.  ( 0 [,] +oo )
)
266255, 264sge0xrcl 38227 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  e.  RR* )
26787a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  -> +oo  e.  RR* )
26890adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  e.  RR* )
269 nfv 1761 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( ph  /\  u  e.  U )
27093adantlr 721 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( C `  j
) ( L `  W ) ( D `
 j ) )  e.  ( 0 [,] +oo ) )
27196adantlr 721 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  Z  e.  ( W  \  Y
) )
27227, 256, 271, 9, 258, 74, 257, 259hsphoidmvle 38408 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) )  <_  ( ( C `
 j ) ( L `  W ) ( D `  j
) ) )
273269, 255, 262, 270, 272sge0lempt 38252 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) ) )
27499adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( D `
 j ) ) ) )  < +oo )
275266, 268, 267, 273, 274xrlelttrd 11457 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  < +oo )
276266, 267, 275xrltned 37580 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  =/= +oo )
277 ge0xrre 37633 . . . . . . . . . . . . . . . 16  |-  ( ( (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) )  e.  ( 0 [,] +oo )  /\  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) )  =/= +oo )  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) )  e.  RR )
278265, 276, 277syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  e.  RR )
279254, 278remulcld 9671 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) )  e.  RR )
280127, 124sseldd 3433 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  e.  RR )
28127, 30, 95, 9, 61, 76, 89, 65, 280sge0hsphoire 38411 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) )  e.  RR )
28245, 281remulcld 9671 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  e.  RR )
283282adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) )  e.  RR )
28414eleq2i 2521 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  U  <->  u  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 ) ) ) ) ) ) } )
285284biimpi 198 . . . . . . . . . . . . . . . . 17  |-  ( u  e.  U  ->  u  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 ) ) ) ) ) ) } )
286 oveq1 6297 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  u  ->  (
z  -  ( A `
 Z ) )  =  ( u  -  ( A `  Z ) ) )
287286oveq2d 6306 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  u  ->  ( G  x.  ( z  -  ( A `  Z ) ) )  =  ( G  x.  ( u  -  ( A `  Z )
) ) )
288 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  u  ->  ( H `  z )  =  ( H `  u ) )
289288fveq1d 5867 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  u  ->  (
( H `  z
) `  ( D `  j ) )  =  ( ( H `  u ) `  ( D `  j )
) )
290289oveq2d 6306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  u  ->  (
( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) )  =  ( ( C `
 j ) ( L `  W ) ( ( H `  u ) `  ( D `  j )
) ) )
291290mpteq2dv 4490 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  u  ->  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) ) )  =  ( j  e.  NN  |->  ( ( C `  j ) ( L `  W
) ( ( H `
 u ) `  ( D `  j ) ) ) ) )
292291fveq2d 5869 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  u  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  z ) `
 ( D `  j ) ) ) ) )  =  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) ) )
293292oveq2d 6306 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  u  ->  (
( 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 `  u ) `
 ( D `  j ) ) ) ) ) ) )
294287, 293breq12d 4415 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  (
( G  x.  (
z  -  ( A `
 Z ) ) )  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  z
) `  ( D `  j ) ) ) ) ) )  <->  ( G  x.  ( u  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) ) ) )
295294elrab 3196 . . . . . . . . . . . . . . . . 17  |-  ( u  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 ) ) ) ) ) ) }  <-> 
( u  e.  ( ( A `  Z
) [,] ( B `
 Z ) )  /\  ( G  x.  ( u  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) ) ) )
296285, 295sylib 200 . . . . . . . . . . . . . . . 16  |-  ( u  e.  U  ->  (
u  e.  ( ( A `  Z ) [,] ( B `  Z ) )  /\  ( G  x.  (
u  -  ( A `
 Z ) ) )  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) ) ) )
297296simprd 465 . . . . . . . . . . . . . . 15  |-  ( u  e.  U  ->  ( G  x.  ( u  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) ) )
298297adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  ( G  x.  ( u  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) ) )
299281adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) )  e.  RR )
30051adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  0  <_  ( 1  +  E
) )
301280adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  NN )  ->  S  e.  RR )
30274, 301, 60, 79hsphoif 38398 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( H `  S ) `
 ( D `  j ) ) : W --> RR )
30327, 60, 64, 302hoidmvcl 38404 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,) +oo )
)
30454, 303sseldi 3430 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( C `  j ) ( L `  W
) ( ( H `
 S ) `  ( D `  j ) ) )  e.  ( 0 [,] +oo )
)
305304adantlr 721 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) )  e.  ( 0 [,] +oo ) )
306301adantlr 721 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  S  e.  RR )
307128adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  U )  ->  U  C_  RR )
308122adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  U )  ->  U  =/=  (/) )
309132adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  U )  ->  E. y  e.  RR  A. z  e.  U  z  <_  y
)
310 simpr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  U )  ->  u  e.  U )
311 suprub 10570 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( U  C_  RR  /\  U  =/=  (/)  /\  E. y  e.  RR  A. z  e.  U  z  <_  y )  /\  u  e.  U )  ->  u  <_  sup ( U ,  RR ,  <  ) )
312307, 308, 309, 310, 311syl31anc 1271 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  U )  ->  u  <_  sup ( U ,  RR ,  <  ) )
313312, 1syl6breqr 4443 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  U )  ->  u  <_  S )
314313adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  u  <_  S )
31527, 256, 271, 9, 258, 306, 314, 74, 257, 259hsphoidmvle2 38407 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  U )  /\  j  e.  NN )  ->  (
( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) )  <_  ( ( C `
 j ) ( L `  W ) ( ( H `  S ) `  ( D `  j )
) ) )
316269, 255, 262, 305, 315sge0lempt 38252 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  u ) `
 ( D `  j ) ) ) ) )  <_  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )
317278, 299, 254, 300, 316lemul2ad 10547 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  u
) `  ( D `  j ) ) ) ) ) )  <_ 
( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )
318253, 279, 283, 298, 317letrd 9792 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  U )  ->  ( G  x.  ( u  -  ( A `  Z ) ) )  <_  ( ( 1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
3193183adant3 1028 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U  /\  c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )  ->  ( G  x.  ( u  -  ( A `  Z )
) )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
320251, 319eqbrtrd 4423 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U  /\  c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )  ->  c  <_  ( ( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
3213203exp 1207 . . . . . . . . . 10  |-  ( ph  ->  ( u  e.  U  ->  ( c  =  ( G  x.  ( u  -  ( A `  Z ) ) )  ->  c  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) ) ) )
322321rexlimdv 2877 . . . . . . . . 9  |-  ( ph  ->  ( E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z ) ) )  ->  c  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) ) )
323322adantr 467 . . . . . . . 8  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
( E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z ) ) )  ->  c  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) ) )
324250, 323mpd 15 . . . . . . 7  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
c  <_  ( (
1  +  E )  x.  (Σ^ `  ( j  e.  NN  |->  ( ( C `  j ) ( L `
 W ) ( ( H `  S
) `  ( D `  j ) ) ) ) ) ) )
325324ralrimiva 2802 . . . . . 6  |-  ( ph  ->  A. c  e.  {
v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  <_ 
( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) ) )
326230adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  ->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t ) )
327 nfv 1761 . . . . . . . . . . . 12  |-  F/ t
ph
328 nfcv 2592 . . . . . . . . . . . . 13  |-  F/_ t
c
329 nfre1 2848 . . . . . . . . . . . . . 14  |-  F/ t E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
)
330329nfab 2596 . . . . . . . . . . . . 13  |-  F/_ t { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) }
331328, 330nfel 2604 . . . . . . . . . . . 12  |-  F/ t  c  e.  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) }
332327, 331nfan 2011 . . . . . . . . . . 11  |-  F/ t ( ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) } )
333 nfv 1761 . . . . . . . . . . 11  |-  F/ t  c  e.  RR
334236adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  ->  E. u  e.  U  t  =  ( u  -  ( A `  Z ) ) )
335 simpr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `  Z ) ) )  /\  c  =  ( G  x.  t ) )  -> 
c  =  ( G  x.  t ) )
3362523adant3 1028 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `
 Z ) ) )  ->  G  e.  RR )
337 simp3 1010 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `
 Z ) ) )  ->  t  =  ( u  -  ( A `  Z )
) )
3381743adant3 1028 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `
 Z ) ) )  ->  ( u  -  ( A `  Z ) )  e.  RR )
339337, 338eqeltrd 2529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `
 Z ) ) )  ->  t  e.  RR )
340336, 339remulcld 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `
 Z ) ) )  ->  ( G  x.  t )  e.  RR )
341340adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `  Z ) ) )  /\  c  =  ( G  x.  t ) )  -> 
( G  x.  t
)  e.  RR )
342335, 341eqeltrd 2529 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `  Z ) ) )  /\  c  =  ( G  x.  t ) )  -> 
c  e.  RR )
343342ex 436 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U  /\  t  =  ( u  -  ( A `
 Z ) ) )  ->  ( c  =  ( G  x.  t )  ->  c  e.  RR ) )
3443433exp 1207 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( u  e.  U  ->  ( t  =  ( u  -  ( A `
 Z ) )  ->  ( c  =  ( G  x.  t
)  ->  c  e.  RR ) ) ) )
345344rexlimdv 2877 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E. u  e.  U  t  =  ( u  -  ( A `
 Z ) )  ->  ( c  =  ( G  x.  t
)  ->  c  e.  RR ) ) )
346345adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
( E. u  e.  U  t  =  ( u  -  ( A `
 Z ) )  ->  ( c  =  ( G  x.  t
)  ->  c  e.  RR ) ) )
347334, 346mpd 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } )  -> 
( c  =  ( G  x.  t )  ->  c  e.  RR ) )
348347ex 436 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) }  ->  (
c  =  ( G  x.  t )  -> 
c  e.  RR ) ) )
349348adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
( t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) }  ->  (
c  =  ( G  x.  t )  -> 
c  e.  RR ) ) )
350332, 333, 349rexlimd 2871 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
( E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } c  =  ( G  x.  t
)  ->  c  e.  RR ) )
351326, 350mpd 15 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
c  e.  RR )
352351ralrimiva 2802 . . . . . . . 8  |-  ( ph  ->  A. c  e.  {
v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  e.  RR )
353 dfss3 3422 . . . . . . . 8  |-  ( { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) }  C_  RR  <->  A. c  e.  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  e.  RR )
354352, 353sylibr 216 . . . . . . 7  |-  ( ph  ->  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) } 
C_  RR )
35540eqcomd 2457 . . . . . . . . . 10  |-  ( ph  ->  0  =  ( G  x.  0 ) )
356 oveq2 6298 . . . . . . . . . . . 12  |-  ( t  =  0  ->  ( G  x.  t )  =  ( G  x.  0 ) )
357356eqeq2d 2461 . . . . . . . . . . 11  |-  ( t  =  0  ->  (
0  =  ( G  x.  t )  <->  0  =  ( G  x.  0
) ) )
358357rspcev 3150 . . . . . . . . . 10  |-  ( ( 0  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) }  /\  0  =  ( G  x.  0 ) )  ->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 0  =  ( G  x.  t
) )
359191, 355, 358syl2anc 667 . . . . . . . . 9  |-  ( ph  ->  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } 0  =  ( G  x.  t
) )
360 eqeq1 2455 . . . . . . . . . . 11  |-  ( v  =  0  ->  (
v  =  ( G  x.  t )  <->  0  =  ( G  x.  t
) ) )
361360rexbidv 2901 . . . . . . . . . 10  |-  ( v  =  0  ->  ( E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t )  <->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 0  =  ( G  x.  t
) ) )
362187, 361elab 3185 . . . . . . . . 9  |-  ( 0  e.  { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  <->  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } 0  =  ( G  x.  t
) )
363359, 362sylibr 216 . . . . . . . 8  |-  ( ph  ->  0  e.  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )
364 ne0i 3737 . . . . . . . 8  |-  ( 0  e.  { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  ->  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) }  =/=  (/) )
365363, 364syl 17 . . . . . . 7  |-  ( ph  ->  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) }  =/=  (/) )
36638, 194remulcld 9671 . . . . . . . 8  |-  ( ph  ->  ( G  x.  (
( B `  Z
)  -  ( A `
 Z ) ) )  e.  RR )
367194adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  (
( B `  Z
)  -  ( A `
 Z ) )  e.  RR )
368138adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  0  <_  G )
36913adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  ->  ( B `  Z )  e.  RR )
370 iccleub 11690 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A `  Z
)  e.  RR*  /\  ( B `  Z )  e.  RR*  /\  u  e.  ( ( A `  Z ) [,] ( B `  Z )
) )  ->  u  <_  ( B `  Z
) )
371153, 155, 156, 370syl3anc 1268 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  U )  ->  u  <_  ( B `  Z
) )
372159, 369, 160, 371lesub1dd 10229 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  U )  ->  (
u  -  ( A `
 Z ) )  <_  ( ( B `
 Z )  -  ( A `  Z ) ) )
373174, 367, 252, 368, 372lemul2ad 10547 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( G  x.  ( u  -  ( A `  Z ) ) )  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z )
) ) )
3743733adant3 1028 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U  /\  c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )  ->  ( G  x.  ( u  -  ( A `  Z )
) )  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z ) ) ) )
375251, 374eqbrtrd 4423 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  U  /\  c  =  ( G  x.  ( u  -  ( A `  Z ) ) ) )  ->  c  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z ) ) ) )
3763753exp 1207 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  U  ->  ( c  =  ( G  x.  ( u  -  ( A `  Z ) ) )  ->  c  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z ) ) ) ) ) )
377376rexlimdv 2877 . . . . . . . . . . 11  |-  ( ph  ->  ( E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z ) ) )  ->  c  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z ) ) ) ) )
378377adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
( E. u  e.  U  c  =  ( G  x.  ( u  -  ( A `  Z ) ) )  ->  c  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z ) ) ) ) )
379250, 378mpd 15 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  { v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } )  -> 
c  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z )
) ) )
380379ralrimiva 2802 . . . . . . . 8  |-  ( ph  ->  A. c  e.  {
v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  <_ 
( G  x.  (
( B `  Z
)  -  ( A `
 Z ) ) ) )
381 breq2 4406 . . . . . . . . . 10  |-  ( y  =  ( G  x.  ( ( B `  Z )  -  ( A `  Z )
) )  ->  (
c  <_  y  <->  c  <_  ( G  x.  ( ( B `  Z )  -  ( A `  Z ) ) ) ) )
382381ralbidv 2827 . . . . . . . . 9  |-  ( y  =  ( G  x.  ( ( B `  Z )  -  ( A `  Z )
) )  ->  ( A. c  e.  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  <_ 
y  <->  A. c  e.  {
v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  <_ 
( G  x.  (
( B `  Z
)  -  ( A `
 Z ) ) ) ) )
383382rspcev 3150 . . . . . . . 8  |-  ( ( ( G  x.  (
( B `  Z
)  -  ( A `
 Z ) ) )  e.  RR  /\  A. c  e.  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  <_ 
( G  x.  (
( B `  Z
)  -  ( A `
 Z ) ) ) )  ->  E. y  e.  RR  A. c  e. 
{ v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) } c  <_  y )
384366, 380, 383syl2anc 667 . . . . . . 7  |-  ( ph  ->  E. y  e.  RR  A. c  e.  { v  |  E. t  e. 
{ w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t
) } c  <_ 
y )
385 suprleub 10573 . . . . . . 7  |-  ( ( ( { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) }  C_  RR  /\ 
{ v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) }  =/=  (/)  /\  E. y  e.  RR  A. c  e. 
{ v  |  E. t  e.  { w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z ) ) } v  =  ( G  x.  t ) } c  <_  y )  /\  ( ( 1  +  E )  x.  (Σ^ `  (
j  e.  NN  |->  ( ( C `  j
) ( L `  W ) ( ( H `  S ) `
 ( D `  j ) ) ) ) ) )  e.  RR )  ->  ( sup ( { v  |  E. t  e.  {
w  |  E. u  e.  U  w  =  ( u  -  ( A `  Z )
) } v  =  ( G  x.  t
) } ,  RR ,  <  )  <_  (
( 1  +  E
)  x.  (Σ^ `  ( j  e.  NN