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

Theorem stoweidlem26 31697
Description: This lemma is used to prove that there is a function  g as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here  L is used to represnt j in the paper,  D is used to represent A in the paper,  S is used to represent t, and  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem26.1  |-  F/_ t F
stoweidlem26.2  |-  F/ j
ph
stoweidlem26.3  |-  F/ t
ph
stoweidlem26.4  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
stoweidlem26.5  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
stoweidlem26.6  |-  ( ph  ->  N  e.  NN )
stoweidlem26.7  |-  ( ph  ->  T  e.  _V )
stoweidlem26.8  |-  ( ph  ->  L  e.  ( 1 ... N ) )
stoweidlem26.9  |-  ( ph  ->  S  e.  ( ( D `  L ) 
\  ( D `  ( L  -  1
) ) ) )
stoweidlem26.10  |-  ( ph  ->  F : T --> RR )
stoweidlem26.11  |-  ( ph  ->  E  e.  RR+ )
stoweidlem26.12  |-  ( ph  ->  E  <  ( 1  /  3 ) )
stoweidlem26.13  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
stoweidlem26.14  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )  ->  0  <_  ( ( X `  i ) `  t
) )
stoweidlem26.15  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  t
) )
Assertion
Ref Expression
stoweidlem26  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 t ) ) ) `  S ) )
Distinct variable groups:    i, j,
t, E    i, L, j, t    i, N, j, t    S, i, t    ph, i    j, F    T, j, t    t, X
Allowed substitution hints:    ph( t, j)    B( t, i, j)    D( t, i, j)    S( j)    T( i)    F( t, i)    X( i, j)

Proof of Theorem stoweidlem26
StepHypRef Expression
1 1re 9595 . . . . . . . 8  |-  1  e.  RR
2 eleq1 2513 . . . . . . . 8  |-  ( L  =  1  ->  ( L  e.  RR  <->  1  e.  RR ) )
31, 2mpbiri 233 . . . . . . 7  |-  ( L  =  1  ->  L  e.  RR )
43adantl 466 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  L  e.  RR )
5 4re 10615 . . . . . . . 8  |-  4  e.  RR
65a1i 11 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  4  e.  RR )
7 3re 10612 . . . . . . . 8  |-  3  e.  RR
87a1i 11 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  3  e.  RR )
9 3ne0 10633 . . . . . . . 8  |-  3  =/=  0
109a1i 11 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  3  =/=  0 )
116, 8, 10redivcld 10375 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  /  3 )  e.  RR )
124, 11resubcld 9990 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  e.  RR )
13 stoweidlem26.11 . . . . . . 7  |-  ( ph  ->  E  e.  RR+ )
1413rpred 11262 . . . . . 6  |-  ( ph  ->  E  e.  RR )
1514adantr 465 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  E  e.  RR )
1612, 15remulcld 9624 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  e.  RR )
17 0red 9597 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  0  e.  RR )
18 fzfid 12059 . . . . . 6  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
1914adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  E  e.  RR )
20 stoweidlem26.13 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
21 stoweidlem26.9 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  ( ( D `  L ) 
\  ( D `  ( L  -  1
) ) ) )
22 eldif 3469 . . . . . . . . . . . . . 14  |-  ( S  e.  ( ( D `
 L )  \ 
( D `  ( L  -  1 ) ) )  <->  ( S  e.  ( D `  L
)  /\  -.  S  e.  ( D `  ( L  -  1 ) ) ) )
2321, 22sylib 196 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  ( D `  L )  /\  -.  S  e.  ( D `  ( L  -  1 ) ) ) )
2423simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  ( D `
 L ) )
25 1e0p1 11009 . . . . . . . . . . . . . . . 16  |-  1  =  ( 0  +  1 )
2625oveq1i 6288 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  =  ( ( 0  +  1 ) ... N
)
27 0z 10878 . . . . . . . . . . . . . . . 16  |-  0  e.  ZZ
28 fzp1ss 11737 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  ZZ  ->  (
( 0  +  1 ) ... N ) 
C_  ( 0 ... N ) )
2927, 28ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( 0  +  1 ) ... N )  C_  ( 0 ... N
)
3026, 29eqsstri 3517 . . . . . . . . . . . . . 14  |-  ( 1 ... N )  C_  ( 0 ... N
)
31 stoweidlem26.8 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  e.  ( 1 ... N ) )
3230, 31sseldi 3485 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  ( 0 ... N ) )
33 stoweidlem26.7 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  e.  _V )
34 rabexg 4584 . . . . . . . . . . . . . 14  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
3533, 34syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
36 oveq1 6285 . . . . . . . . . . . . . . . . 17  |-  ( j  =  L  ->  (
j  -  ( 1  /  3 ) )  =  ( L  -  ( 1  /  3
) ) )
3736oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( j  =  L  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( L  -  ( 1  / 
3 ) )  x.  E ) )
3837breq2d 4446 . . . . . . . . . . . . . . 15  |-  ( j  =  L  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) ) )
3938rabbidv 3085 . . . . . . . . . . . . . 14  |-  ( j  =  L  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) } )
40 stoweidlem26.4 . . . . . . . . . . . . . 14  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
4139, 40fvmptg 5936 . . . . . . . . . . . . 13  |-  ( ( L  e.  ( 0 ... N )  /\  { t  e.  T  | 
( F `  t
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E ) }  e.  _V )  -> 
( D `  L
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
4232, 35, 41syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( D `  L
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
4324, 42eleqtrd 2531 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
44 nfcv 2603 . . . . . . . . . . . 12  |-  F/_ t S
45 nfcv 2603 . . . . . . . . . . . 12  |-  F/_ t T
46 stoweidlem26.1 . . . . . . . . . . . . . 14  |-  F/_ t F
4746, 44nffv 5860 . . . . . . . . . . . . 13  |-  F/_ t
( F `  S
)
48 nfcv 2603 . . . . . . . . . . . . 13  |-  F/_ t  <_
49 nfcv 2603 . . . . . . . . . . . . 13  |-  F/_ t
( ( L  -  ( 1  /  3
) )  x.  E
)
5047, 48, 49nfbr 4478 . . . . . . . . . . . 12  |-  F/ t ( F `  S
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E )
51 fveq2 5853 . . . . . . . . . . . . 13  |-  ( t  =  S  ->  ( F `  t )  =  ( F `  S ) )
5251breq1d 4444 . . . . . . . . . . . 12  |-  ( t  =  S  ->  (
( F `  t
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  S )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) ) )
5344, 45, 50, 52elrabf 3239 . . . . . . . . . . 11  |-  ( S  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( L  -  ( 1  /  3
) )  x.  E
) }  <->  ( S  e.  T  /\  ( F `  S )  <_  ( ( L  -  ( 1  /  3
) )  x.  E
) ) )
5443, 53sylib 196 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  T  /\  ( F `  S
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E ) ) )
5554simpld 459 . . . . . . . . 9  |-  ( ph  ->  S  e.  T )
5655adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  S  e.  T )
5720, 56ffvelrnd 6014 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  S )  e.  RR )
5819, 57remulcld 9624 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
5918, 58fsumrecl 13532 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
)  e.  RR )
6059adantr 465 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
615, 7, 9redivcli 10314 . . . . . . 7  |-  ( 4  /  3 )  e.  RR
6261a1i 11 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  /  3 )  e.  RR )
634, 62resubcld 9990 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  e.  RR )
644recnd 9622 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  L  e.  CC )
6564subid1d 9922 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  0 )  =  L )
66 3cn 10613 . . . . . . . . . 10  |-  3  e.  CC
6766, 9dividi 10280 . . . . . . . . 9  |-  ( 3  /  3 )  =  1
68 3lt4 10708 . . . . . . . . . 10  |-  3  <  4
69 3pos 10632 . . . . . . . . . . 11  |-  0  <  3
707, 5, 7, 69ltdiv1ii 10478 . . . . . . . . . 10  |-  ( 3  <  4  <->  ( 3  /  3 )  < 
( 4  /  3
) )
7168, 70mpbi 208 . . . . . . . . 9  |-  ( 3  /  3 )  < 
( 4  /  3
)
7267, 71eqbrtrri 4455 . . . . . . . 8  |-  1  <  ( 4  /  3
)
73 breq1 4437 . . . . . . . . 9  |-  ( L  =  1  ->  ( L  <  ( 4  / 
3 )  <->  1  <  ( 4  /  3 ) ) )
7473adantl 466 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  <  ( 4  / 
3 )  <->  1  <  ( 4  /  3 ) ) )
7572, 74mpbiri 233 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  L  <  ( 4  /  3
) )
7665, 75eqbrtrd 4454 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  0 )  <  ( 4  / 
3 ) )
774, 17, 62, 76ltsub23d 10160 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  <  0 )
7813rpgt0d 11265 . . . . . 6  |-  ( ph  ->  0  <  E )
7978adantr 465 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  0  <  E )
80 mulltgt0 31348 . . . . 5  |-  ( ( ( ( L  -  ( 4  /  3
) )  e.  RR  /\  ( L  -  (
4  /  3 ) )  <  0 )  /\  ( E  e.  RR  /\  0  < 
E ) )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  0 )
8163, 77, 15, 79, 80syl22anc 1228 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  0 )
82 0cn 9588 . . . . . . . 8  |-  0  e.  CC
83 fsumconst 13581 . . . . . . . 8  |-  ( ( ( 0 ... N
)  e.  Fin  /\  0  e.  CC )  -> 
sum_ i  e.  ( 0 ... N ) 0  =  ( (
# `  ( 0 ... N ) )  x.  0 ) )
8418, 82, 83sylancl 662 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  =  ( (
# `  ( 0 ... N ) )  x.  0 ) )
85 hashcl 12404 . . . . . . . . 9  |-  ( ( 0 ... N )  e.  Fin  ->  ( # `
 ( 0 ... N ) )  e. 
NN0 )
86 nn0cn 10808 . . . . . . . . 9  |-  ( (
# `  ( 0 ... N ) )  e. 
NN0  ->  ( # `  (
0 ... N ) )  e.  CC )
8718, 85, 863syl 20 . . . . . . . 8  |-  ( ph  ->  ( # `  (
0 ... N ) )  e.  CC )
8887mul01d 9779 . . . . . . 7  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  x.  0 )  =  0 )
8984, 88eqtrd 2482 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  =  0 )
9089adantr 465 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) 0  =  0 )
91 0red 9597 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  e.  RR )
9213rpge0d 11266 . . . . . . . . 9  |-  ( ph  ->  0  <_  E )
9392adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  E )
94 stoweidlem26.3 . . . . . . . . . . . 12  |-  F/ t
ph
95 nfv 1692 . . . . . . . . . . . 12  |-  F/ t  i  e.  ( 0 ... N )
9694, 95nfan 1912 . . . . . . . . . . 11  |-  F/ t ( ph  /\  i  e.  ( 0 ... N
) )
97 nfv 1692 . . . . . . . . . . 11  |-  F/ t 0  <_  ( ( X `  i ) `  S )
9896, 97nfim 1904 . . . . . . . . . 10  |-  F/ t ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  S )
)
99 fveq2 5853 . . . . . . . . . . . 12  |-  ( t  =  S  ->  (
( X `  i
) `  t )  =  ( ( X `
 i ) `  S ) )
10099breq2d 4446 . . . . . . . . . . 11  |-  ( t  =  S  ->  (
0  <_  ( ( X `  i ) `  t )  <->  0  <_  ( ( X `  i
) `  S )
) )
101100imbi2d 316 . . . . . . . . . 10  |-  ( t  =  S  ->  (
( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  t )
)  <->  ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  S )
) ) )
102 stoweidlem26.14 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )  ->  0  <_  ( ( X `  i ) `  t
) )
1031023expia 1197 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
t  e.  T  -> 
0  <_  ( ( X `  i ) `  t ) ) )
104103com12 31 . . . . . . . . . 10  |-  ( t  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  t
) ) )
10544, 98, 101, 104vtoclgaf 3156 . . . . . . . . 9  |-  ( S  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) ) )
10656, 105mpcom 36 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) )
10719, 57, 93, 106mulge0d 10132 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( E  x.  (
( X `  i
) `  S )
) )
10818, 91, 58, 107fsumle 13589 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
109108adantr 465 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) 0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
11090, 109eqbrtrrd 4456 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  0  <_ 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) )
11116, 17, 60, 81, 110ltletrd 9742 . . 3  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) )
112 elfzelz 11694 . . . . . . . . 9  |-  ( L  e.  ( 1 ... N )  ->  L  e.  ZZ )
113 zre 10871 . . . . . . . . 9  |-  ( L  e.  ZZ  ->  L  e.  RR )
11431, 112, 1133syl 20 . . . . . . . 8  |-  ( ph  ->  L  e.  RR )
1155a1i 11 . . . . . . . . 9  |-  ( ph  ->  4  e.  RR )
1167a1i 11 . . . . . . . . 9  |-  ( ph  ->  3  e.  RR )
1179a1i 11 . . . . . . . . 9  |-  ( ph  ->  3  =/=  0 )
118115, 116, 117redivcld 10375 . . . . . . . 8  |-  ( ph  ->  ( 4  /  3
)  e.  RR )
119114, 118resubcld 9990 . . . . . . 7  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  e.  RR )
120119, 14remulcld 9624 . . . . . 6  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR )
121120adantr 465 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR )
1221a1i 11 . . . . . . . . 9  |-  ( ph  ->  1  e.  RR )
123 stoweidlem26.6 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
12414, 123nndivred 10587 . . . . . . . . 9  |-  ( ph  ->  ( E  /  N
)  e.  RR )
125122, 124resubcld 9990 . . . . . . . 8  |-  ( ph  ->  ( 1  -  ( E  /  N ) )  e.  RR )
126114, 122resubcld 9990 . . . . . . . 8  |-  ( ph  ->  ( L  -  1 )  e.  RR )
127125, 126remulcld 9624 . . . . . . 7  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  e.  RR )
12814, 127remulcld 9624 . . . . . 6  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  e.  RR )
129128adantr 465 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  e.  RR )
130 fzfid 12059 . . . . . . . 8  |-  ( ph  ->  ( 0 ... ( L  -  2 ) )  e.  Fin )
13131, 112syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  e.  ZZ )
132 2z 10899 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
133132a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  2  e.  ZZ )
134131, 133zsubcld 10976 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  2 )  e.  ZZ )
135123nnzd 10970 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
136131zred 10971 . . . . . . . . . . . . . . 15  |-  ( ph  ->  L  e.  RR )
137 2re 10608 . . . . . . . . . . . . . . . 16  |-  2  e.  RR
138137a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  e.  RR )
139136, 138resubcld 9990 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  2 )  e.  RR )
140123nnred 10554 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  RR )
141 0le2 10629 . . . . . . . . . . . . . . . 16  |-  0  <_  2
142 0red 9597 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  e.  RR )
143142, 138, 136lesub2d 10163 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  <_  2  <->  ( L  -  2 )  <_  ( L  - 
0 ) ) )
144141, 143mpbii 211 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  2 )  <_  ( L  -  0 ) )
145131zcnd 10972 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  L  e.  CC )
146145subid1d 9922 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  0 )  =  L )
147144, 146breqtrd 4458 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  2 )  <_  L )
148 elfzle2 11696 . . . . . . . . . . . . . . 15  |-  ( L  e.  ( 1 ... N )  ->  L  <_  N )
14931, 148syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  <_  N )
150139, 136, 140, 147, 149letrd 9739 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  2 )  <_  N )
151134, 135, 1503jca 1175 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2
)  <_  N )
)
152 eluz2 11093 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  ( L  -  2 ) )  <->  ( ( L  -  2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2 )  <_  N ) )
153151, 152sylibr 212 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  ( L  -  2
) ) )
154 fzss2 11729 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  ( L  -  2 ) )  ->  ( 0 ... ( L  - 
2 ) )  C_  ( 0 ... N
) )
155153, 154syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ... ( L  -  2 ) )  C_  ( 0 ... N ) )
156155sselda 3487 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  ( 0 ... N
) )
157156, 57syldan 470 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( X `  i
) `  S )  e.  RR )
158130, 157fsumrecl 13532 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `  i ) `  S
)  e.  RR )
15914, 158remulcld 9624 . . . . . 6  |-  ( ph  ->  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  e.  RR )
160159adantr 465 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  e.  RR )
16114, 126remulcld 9624 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  ( L  -  1 ) )  e.  RR )
16214, 14remulcld 9624 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  E
)  e.  RR )
163161, 162resubcld 9990 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  e.  RR )
164126, 123nndivred 10587 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  e.  RR )
165162, 164remulcld 9624 . . . . . . . . 9  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  e.  RR )
166161, 165resubcld 9990 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  (
( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) ) )  e.  RR )
167126, 14resubcld 9990 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  e.  RR )
168122, 14readdcld 9623 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
1691, 7, 9redivcli 10314 . . . . . . . . . . . . . . 15  |-  ( 1  /  3 )  e.  RR
170169a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
171 stoweidlem26.12 . . . . . . . . . . . . . 14  |-  ( ph  ->  E  <  ( 1  /  3 ) )
17214, 170, 122, 171ltadd2dd 9741 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  +  E
)  <  ( 1  +  ( 1  / 
3 ) ) )
173 ax-1cn 9550 . . . . . . . . . . . . . . 15  |-  1  e.  CC
17466, 173, 66, 9divdiri 10304 . . . . . . . . . . . . . 14  |-  ( ( 3  +  1 )  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
175 3p1e4 10664 . . . . . . . . . . . . . . 15  |-  ( 3  +  1 )  =  4
176175oveq1i 6288 . . . . . . . . . . . . . 14  |-  ( ( 3  +  1 )  /  3 )  =  ( 4  /  3
)
17767oveq1i 6288 . . . . . . . . . . . . . 14  |-  ( ( 3  /  3 )  +  ( 1  / 
3 ) )  =  ( 1  +  ( 1  /  3 ) )
178174, 176, 1773eqtr3ri 2479 . . . . . . . . . . . . 13  |-  ( 1  +  ( 1  / 
3 ) )  =  ( 4  /  3
)
179172, 178syl6breq 4473 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  E
)  <  ( 4  /  3 ) )
180168, 118, 114, 179ltsub2dd 10168 . . . . . . . . . . 11  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  <  ( L  -  ( 1  +  E ) ) )
181173a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  CC )
18213rpcnd 11264 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  CC )
183145, 181, 182subsub4d 9964 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  =  ( L  -  ( 1  +  E ) ) )
184180, 183breqtrrd 4460 . . . . . . . . . 10  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  <  ( ( L  -  1 )  -  E ) )
185119, 167, 13, 184ltmul1dd 11313 . . . . . . . . 9  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( (
( L  -  1 )  -  E )  x.  E ) )
186145, 181subcld 9933 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  -  1 )  e.  CC )
187186, 182subcld 9933 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  e.  CC )
188182, 187mulcomd 9617 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( ( L  -  1 )  -  E )  x.  E ) )
189182, 186, 182subdid 10015 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
190188, 189eqtr3d 2484 . . . . . . . . 9  |-  ( ph  ->  ( ( ( L  -  1 )  -  E )  x.  E
)  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
191185, 190breqtrd 4458 . . . . . . . 8  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
192 1zzd 10898 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
193 elfz 11684 . . . . . . . . . . . . . . . . 17  |-  ( ( L  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )  ->  ( L  e.  ( 1 ... N )  <->  ( 1  <_  L  /\  L  <_  N ) ) )
194131, 192, 135, 193syl3anc 1227 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( L  e.  ( 1 ... N )  <-> 
( 1  <_  L  /\  L  <_  N ) ) )
19531, 194mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  <_  L  /\  L  <_  N ) )
196195simprd 463 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  <_  N )
197 zlem1lt 10918 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  ZZ  /\  N  e.  ZZ )  ->  ( L  <_  N  <->  ( L  -  1 )  <  N ) )
198131, 135, 197syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  <_  N  <->  ( L  -  1 )  <  N ) )
199196, 198mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  1 )  <  N )
200123nngt0d 10582 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  N )
201 ltdiv1 10409 . . . . . . . . . . . . . 14  |-  ( ( ( L  -  1 )  e.  RR  /\  N  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) )  -> 
( ( L  - 
1 )  <  N  <->  ( ( L  -  1 )  /  N )  <  ( N  /  N ) ) )
202126, 140, 140, 200, 201syl112anc 1231 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  - 
1 )  <  N  <->  ( ( L  -  1 )  /  N )  <  ( N  /  N ) ) )
203199, 202mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  <  ( N  /  N ) )
204123nncnd 10555 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
205123nnne0d 10583 . . . . . . . . . . . . 13  |-  ( ph  ->  N  =/=  0 )
206204, 205dividd 10321 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  /  N
)  =  1 )
207203, 206breqtrd 4458 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  <  1 )
20814, 14, 78, 78mulgt0d 9737 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  ( E  x.  E ) )
209 ltmul2 10396 . . . . . . . . . . . 12  |-  ( ( ( ( L  - 
1 )  /  N
)  e.  RR  /\  1  e.  RR  /\  (
( E  x.  E
)  e.  RR  /\  0  <  ( E  x.  E ) ) )  ->  ( ( ( L  -  1 )  /  N )  <  1  <->  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) )  <  (
( E  x.  E
)  x.  1 ) ) )
210164, 122, 162, 208, 209syl112anc 1231 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  -  1 )  /  N )  <  1  <->  ( ( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) )  <  ( ( E  x.  E )  x.  1 ) ) )
211207, 210mpbid 210 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  <  ( ( E  x.  E )  x.  1 ) )
212182, 182mulcld 9616 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  E
)  e.  CC )
213212mulid1d 9613 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  E )  x.  1 )  =  ( E  x.  E ) )
214211, 213breqtrd 4458 . . . . . . . . 9  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  <  ( E  x.  E ) )
215165, 162, 161, 214ltsub2dd 10168 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) )
216120, 163, 166, 191, 215lttrd 9743 . . . . . . 7  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) )
217182, 204, 205divcld 10323 . . . . . . . . . . 11  |-  ( ph  ->  ( E  /  N
)  e.  CC )
218181, 217, 186subdird 10016 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  =  ( ( 1  x.  ( L  -  1 ) )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
219186mulid2d 9614 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  x.  ( L  -  1 ) )  =  ( L  -  1 ) )
220219oveq1d 6293 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  x.  ( L  -  1 ) )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( ( L  -  1 )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
221218, 220eqtrd 2482 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  =  ( ( L  -  1 )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
222221oveq2d 6294 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( E  x.  ( ( L  - 
1 )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) ) ) )
223217, 186mulcld 9616 . . . . . . . . 9  |-  ( ph  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  e.  CC )
224182, 186, 223subdid 10015 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  ( ( E  /  N )  x.  ( L  - 
1 ) ) ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) ) )
225182, 204, 186, 205div32d 10346 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  =  ( E  x.  ( ( L  -  1 )  /  N ) ) )
226225oveq2d 6294 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
227186, 204, 205divcld 10323 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  e.  CC )
228182, 182, 227mulassd 9619 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
229226, 228eqtr4d 2485 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( ( E  x.  E )  x.  ( ( L  -  1 )  /  N ) ) )
230229oveq2d 6294 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )
231222, 224, 2303eqtrd 2486 . . . . . . 7  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )
232216, 231breqtrrd 4460 . . . . . 6  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) ) )
233232adantr 465 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) ) )
234181, 217subcld 9933 . . . . . . . . . 10  |-  ( ph  ->  ( 1  -  ( E  /  N ) )  e.  CC )
235 fsumconst 13581 . . . . . . . . . 10  |-  ( ( ( 0 ... ( L  -  2 ) )  e.  Fin  /\  ( 1  -  ( E  /  N ) )  e.  CC )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
236130, 234, 235syl2anc 661 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
237236adantr 465 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
238 0zd 10879 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  e.  ZZ )
23931adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( 1 ... N ) )
240239, 112syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ZZ )
241132a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  e.  ZZ )
242240, 241zsubcld 10976 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  -  2 )  e.  ZZ )
243 elnnuz 11123 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  <->  N  e.  ( ZZ>= `  1 )
)
244123, 243sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
245 elfzp12 11763 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( L  e.  ( 1 ... N
)  <->  ( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N
) ) ) )
246244, 245syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  ( 1 ... N )  <-> 
( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N ) ) ) )
24731, 246mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N ) ) )
248247orcanai 911 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( (
1  +  1 ) ... N ) )
249 1p1e2 10652 . . . . . . . . . . . . . . . . . 18  |-  ( 1  +  1 )  =  2
250249a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 1  +  1 )  =  2 )
251250oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  +  1 ) ... N
)  =  ( 2 ... N ) )
252248, 251eleqtrd 2531 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( 2 ... N ) )
253 elfzle1 11695 . . . . . . . . . . . . . . 15  |-  ( L  e.  ( 2 ... N )  ->  2  <_  L )
254252, 253syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  <_  L )
255114adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  RR )
256137a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  e.  RR )
257255, 256subge0d 10145 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0  <_  ( L  -  2 )  <->  2  <_  L )
)
258254, 257mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  <_  ( L  -  2 ) )
259238, 242, 2583jca 1175 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ  /\  0  <_  ( L  - 
2 ) ) )
260 eluz2 11093 . . . . . . . . . . . 12  |-  ( ( L  -  2 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ  /\  0  <_ 
( L  -  2 ) ) )
261259, 260sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  -  2 )  e.  ( ZZ>= ` 
0 ) )
262 hashfz 12461 . . . . . . . . . . 11  |-  ( ( L  -  2 )  e.  ( ZZ>= `  0
)  ->  ( # `  (
0 ... ( L  - 
2 ) ) )  =  ( ( ( L  -  2 )  -  0 )  +  1 ) )
263261, 262syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( # `  ( 0 ... ( L  - 
2 ) ) )  =  ( ( ( L  -  2 )  -  0 )  +  1 ) )
264 2cn 10609 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
265264a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  e.  CC )
266145, 265subcld 9933 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  2 )  e.  CC )
267266subid1d 9922 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  - 
2 )  -  0 )  =  ( L  -  2 ) )
268267oveq1d 6293 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( ( L  -  2 )  +  1 ) )
269145, 265, 181subadd23d 9955 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
2 )  +  1 )  =  ( L  +  ( 1  -  2 ) ) )
270264, 173negsubdi2i 9908 . . . . . . . . . . . . . . . 16  |-  -u (
2  -  1 )  =  ( 1  -  2 )
271 2m1e1 10653 . . . . . . . . . . . . . . . . 17  |-  ( 2  -  1 )  =  1
272271negeqi 9815 . . . . . . . . . . . . . . . 16  |-  -u (
2  -  1 )  =  -u 1
273270, 272eqtr3i 2472 . . . . . . . . . . . . . . 15  |-  ( 1  -  2 )  = 
-u 1
274273a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  -  2 )  =  -u 1
)
275274oveq2d 6294 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  +  ( 1  -  2 ) )  =  ( L  +  -u 1 ) )
276145, 181negsubd 9939 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  +  -u
1 )  =  ( L  -  1 ) )
277275, 276eqtrd 2482 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  +  ( 1  -  2 ) )  =  ( L  -  1 ) )
278268, 269, 2773eqtrd 2486 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( L  -  1 ) )
279278adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( L  -  1 ) )
280263, 279eqtrd 2482 . . . . . . . . 9  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( # `  ( 0 ... ( L  - 
2 ) ) )  =  ( L  - 
1 ) )
281280oveq1d 6293 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( # `  (
0 ... ( L  - 
2 ) ) )  x.  ( 1  -  ( E  /  N
) ) )  =  ( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) ) )
282186, 234mulcomd 9617 . . . . . . . . 9  |-  ( ph  ->  ( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
283282adantr 465 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
284237, 281, 2833eqtrd 2486 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  -  1 ) ) )
285 fzfid 12059 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0 ... ( L  -  2 ) )  e.  Fin )
286 fzn0 11706 . . . . . . . . 9  |-  ( ( 0 ... ( L  -  2 ) )  =/=  (/)  <->  ( L  - 
2 )  e.  (
ZZ>= `  0 ) )
287261, 286sylibr 212 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0 ... ( L  -  2 ) )  =/=  (/) )
288125ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( 1  -  ( E  /  N ) )  e.  RR )
289 simpll 753 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ph )
290156adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  ( 0 ... N
) )
291289, 290, 57syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( ( X `  i ) `  S )  e.  RR )
29255adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  T )
293 elfzelz 11694 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  e.  ZZ )
294293zred 10971 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  e.  RR )
295294adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  RR )
296169a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
1  /  3 )  e.  RR )
297295, 296readdcld 9623 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  +  ( 1  /  3 ) )  e.  RR )
29814adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  E  e.  RR )
299297, 298remulcld 9624 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  e.  RR )
300114adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  L  e.  RR )
301137a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  2  e.  RR )
302300, 301resubcld 9990 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  RR )
303302, 296readdcld 9623 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( L  -  2 )  +  ( 1  /  3 ) )  e.  RR )
304303, 298remulcld 9624 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( ( L  - 
2 )  +  ( 1  /  3 ) )  x.  E )  e.  RR )
305 stoweidlem26.10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : T --> RR )
306305, 55jca 532 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F : T --> RR  /\  S  e.  T
) )
307306adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( F : T --> RR  /\  S  e.  T )
)
308 ffvelrn 6011 . . . . . . . . . . . . . 14  |-  ( ( F : T --> RR  /\  S  e.  T )  ->  ( F `  S
)  e.  RR )
309307, 308syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( F `  S )  e.  RR )
310 elfzle2 11696 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  <_  ( L  -  2 ) )
311310adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  <_  ( L  -  2 ) )
312295, 302, 296, 311leadd1dd 10169 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  +  ( 1  /  3 ) )  <_  ( ( L  -  2 )  +  ( 1  /  3
) ) )
31314, 78jca 532 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
314313adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  e.  RR  /\  0  <  E ) )
315 lemul1 10397 . . . . . . . . . . . . . . 15  |-  ( ( ( i  +  ( 1  /  3 ) )  e.  RR  /\  ( ( L  - 
2 )  +  ( 1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
i  +  ( 1  /  3 ) )  <_  ( ( L  -  2 )  +  ( 1  /  3
) )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
) ) )
316297, 303, 314, 315syl3anc 1227 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  <_  ( ( L  -  2 )  +  ( 1  / 
3 ) )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
) ) )
317312, 316mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( ( ( L  -  2 )  +  ( 1  / 
3 ) )  x.  E ) )
318114, 138resubcld 9990 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  2 )  e.  RR )
319318, 170readdcld 9623 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
2 )  +  ( 1  /  3 ) )  e.  RR )
320319, 14remulcld 9624 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  e.  RR )
321305, 55ffvelrnd 6014 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  S
)  e.  RR )
322126, 170resubcld 9990 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( L  - 
1 )  -  (
1  /  3 ) )  e.  RR )
323322, 14remulcld 9624 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  e.  RR )
324 addid1 9760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  CC  ->  (
1  +  0 )  =  1 )
325324eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  e.  CC  ->  1  =  ( 1  +  0 ) )
326173, 325mp1i 12 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  1  =  ( 1  +  0 ) )
327181subidd 9921 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1  -  1 )  =  0 )
328327eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  0  =  ( 1  -  1 ) )
329328oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  +  0 )  =  ( 1  +  ( 1  -  1 ) ) )
330 addsubass 9832 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
( 1  +  1 )  -  1 )  =  ( 1  +  ( 1  -  1 ) ) )
331330eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
1  +  ( 1  -  1 ) )  =  ( ( 1  +  1 )  - 
1 ) )
332181, 181, 181, 331syl3anc 1227 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  +  ( 1  -  1 ) )  =  ( ( 1  +  1 )  -  1 ) )
333326, 329, 3323eqtrd 2486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  1  =  ( ( 1  +  1 )  -  1 ) )
334333oveq2d 6294 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  -  1 )  =  ( L  -  ( ( 1  +  1 )  - 
1 ) ) )
335249a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  +  1 )  =  2 )
336335oveq1d 6293 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1  +  1 )  -  1 )  =  ( 2  -  1 ) )
337336oveq2d 6294 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  -  (
( 1  +  1 )  -  1 ) )  =  ( L  -  ( 2  -  1 ) ) )
338145, 265, 181subsubd 9961 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  -  (
2  -  1 ) )  =  ( ( L  -  2 )  +  1 ) )
339334, 337, 3383eqtrd 2486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  -  1 )  =  ( ( L  -  2 )  +  1 ) )
340339oveq1d 6293 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  =  ( ( ( L  -  2 )  +  1 )  -  ( 2  / 
3 ) ) )
341264, 66, 9divcli 10289 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  /  3 )  e.  CC
342341a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 2  /  3
)  e.  CC )
343266, 181, 342addsubassd 9953 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( L  -  2 )  +  1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  -  ( 2  /  3
) ) ) )
344173, 66, 9divcli 10289 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  /  3 )  e.  CC
345 df-3 10598 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  3  =  ( 2  +  1 )
346345oveq1i 6288 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 3  /  3 )  =  ( ( 2  +  1 )  /  3
)
347264, 173, 66, 9divdiri 10304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  +  1 )  /  3 )  =  ( ( 2  / 
3 )  +  ( 1  /  3 ) )
348346, 67, 3473eqtr3ri 2479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  /  3 )  +  ( 1  / 
3 ) )  =  1
349173, 341, 344, 348subaddrii 9911 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  -  ( 2  / 
3 ) )  =  ( 1  /  3
)
350349a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  -  (
2  /  3 ) )  =  ( 1  /  3 ) )
351350oveq2d 6294 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( L  - 
2 )  +  ( 1  -  ( 2  /  3 ) ) )  =  ( ( L  -  2 )  +  ( 1  / 
3 ) ) )
352340, 343, 3513eqtrd 2486 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  / 
3 ) ) )
353137, 7, 9redivcli 10314 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  /  3 )  e.  RR
354353a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 2  /  3
)  e.  RR )
355 1lt2 10705 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
3567, 69pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 3  e.  RR  /\  0  <  3 )
3571, 137, 3563pm3.2i 1173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  RR  /\  2  e.  RR  /\  ( 3  e.  RR  /\  0  <  3 ) )
358 ltdiv1 10409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  (
3  e.  RR  /\  0  <  3 ) )  ->  ( 1  <  2  <->  ( 1  / 
3 )  <  (
2  /  3 ) ) )
359357, 358mp1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  <  2  <->  ( 1  /  3 )  <  ( 2  / 
3 ) ) )
360355, 359mpbii 211 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1  /  3
)  <  ( 2  /  3 ) )
361170, 354, 126, 360ltsub2dd 10168 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  <  ( ( L  -  1 )  -  ( 1  / 
3 ) ) )
362352, 361eqbrtrrd 4456 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( L  - 
2 )  +  ( 1  /  3 ) )  <  ( ( L  -  1 )  -  ( 1  / 
3 ) ) )
363319, 322, 13, 362ltmul1dd 11313 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  <  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) )
36423simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  -.  S  e.  ( D `  ( L  -  1 ) ) )
365195simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  1  <_  L )
366140, 122readdcld 9623 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( N  +  1 )  e.  RR )
367140lep1d 10480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  N  <_  ( N  +  1 ) )
368114, 140, 366, 196, 367letrd 9739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  L  <_  ( N  +  1 ) )
369135peano2zd 10974 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
370 elfz 11684 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( L  e.  ZZ  /\  1  e.  ZZ  /\  ( N  +  1 )  e.  ZZ )  -> 
( L  e.  ( 1 ... ( N  +  1 ) )  <-> 
( 1  <_  L  /\  L  <_  ( N  +  1 ) ) ) )
371131, 192, 369, 370syl3anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( L  e.  ( 1 ... ( N  +  1 ) )  <-> 
( 1  <_  L  /\  L  <_  ( N  +  1 ) ) ) )
372365, 368, 371mpbir2and 920 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  L  e.  ( 1 ... ( N  + 
1 ) ) )
373145, 181npcand 9937 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( L  - 
1 )  +  1 )  =  L )
374 0p1e1 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  +  1 )  =  1
375374a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( 0  +  1 )  =  1 )
376375oveq1d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( 0  +  1 ) ... ( N  +  1 ) )  =  ( 1 ... ( N  + 
1 ) ) )
377372, 373, 3763eltr4d 2544 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( L  - 
1 )  +  1 )  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) ) )
378 0zd 10879 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  0  e.  ZZ )
379131, 192zsubcld 10976 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( L  -  1 )  e.  ZZ )
380 fzaddel 11724 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 0  e.  ZZ  /\  N  e.  ZZ )  /\  ( ( L  -  1 )  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( ( L  - 
1 )  e.  ( 0 ... N )  <-> 
( ( L  - 
1 )  +  1 )  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) ) ) )
381378, 135, 379, 192, 380syl22anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( L  - 
1 )  e.  ( 0 ... N )  <-> 
( ( L  - 
1 )  +  1 )  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) ) ) )
382377, 381mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( L  -  1 )  e.  ( 0 ... N ) )
383 rabexg 4584 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
38433, 383syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
385 oveq1 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  ( L  - 
1 )  ->  (
j  -  ( 1  /  3 ) )  =  ( ( L  -  1 )  -  ( 1  /  3
) ) )
386385oveq1d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  ( L  - 
1 )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) )
387386breq2d 4446 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  ( L  - 
1 )  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
388387rabbidv 3085 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  ( L  - 
1 )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) } )
389388, 40fvmptg 5936 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( L  -  1 )  e.  ( 0 ... N )  /\  { t  e.  T  | 
( F `  t
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) }  e.  _V )  -> 
( D `  ( L  -  1 ) )  =  { t  e.  T  |  ( F `  t )  <_  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } )
390382, 384, 389syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( D `  ( L  -  1 ) )  =  { t  e.  T  |  ( F `  t )  <_  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } )
391364, 390neleqtrd 2553 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  S  e.  {
t  e.  T  | 
( F `  t
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) } )
392 nfcv 2603 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t
( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)
39347, 48, 392nfbr 4478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ t ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )
39451breq1d 4444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  S  ->  (
( F `  t
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
39544, 45, 393, 394elrabf 3239 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( S  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) }  <->  ( S  e.  T  /\  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
396391, 395sylnib 304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  ( S  e.  T  /\  ( F `
 S )  <_ 
( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
397 ianor 488 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( S  e.  T  /\  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) )  <-> 
( -.  S  e.  T  \/  -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
398396, 397sylib 196 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
399 olc 384 . . . . . . . . . . . . . . . . . . . . 21  |-  ( S  e.  T  ->  ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  \/  S  e.  T ) )
400399anim1i 568 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( S  e.  T  /\  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )  -> 
( ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  S  e.  T )  /\  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) ) )
40155, 398, 400syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  S  e.  T )  /\  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) ) )
402 orcom 387 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  S  e.  T  \/  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) )  <->  ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  -.  S  e.  T ) )
403402anbi2i 694 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( -.  ( F `
 S )  <_ 
( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  S  e.  T )  /\  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )  <->  ( ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  \/  S  e.  T )  /\  ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  -.  S  e.  T ) ) )
404401, 403sylib 196 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  S  e.  T )  /\  ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  \/ 
-.  S  e.  T
) ) )
405 pm4.43 925 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  <->  ( ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  \/  S  e.  T )  /\  ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  -.  S  e.  T ) ) )
406404, 405sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) )
407323, 321ltnled 9732 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E )  <  ( F `  S )  <->  -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) ) )
408406, 407mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  <  ( F `  S ) )
409320, 323, 321, 363, 408lttrd 9743 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  <  ( F `  S ) )
410320, 321, 409ltled 9733 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  S ) )
411410adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( ( L  - 
2 )  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  S ) )
412299, 304, 309, 317, 411letrd 9739 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  S ) )
413 nfcv 2603 . . . . . . . . . . . . . 14  |-  F/_ t
( ( i  +  ( 1  /  3
) )  x.  E
)
414413, 48, 47nfbr 4478 . . . . . . . . . . . . 13  |-  F/ t ( ( i  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  S )
41551breq2d 4446 . . . . . . . . . . . . 13  |-  ( t  =  S  ->  (
( ( i  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  S
) ) )
41644, 45, 414, 415elrabf 3239 . . . . . . . . . . . 12  |-  ( S  e.  { t  e.  T  |  ( ( i  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) }  <->  ( S  e.  T  /\  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  S ) ) )
417292, 412, 416sylanbrc 664 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
418 rabexg 4584 . . . . . . . . . . . . . 14  |-  ( T  e.  _V  ->  { t  e.  T  |  ( ( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
41933, 418syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
420419adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  { t  e.  T  |  ( ( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
421 oveq1 6285 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  (
j  +  ( 1  /  3 ) )  =  ( i  +  ( 1  /  3
) ) )
422421oveq1d 6293 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  =  ( ( i  +  ( 1  / 
3 ) )  x.  E ) )
423422breq1d 4444 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) ) )
424423rabbidv 3085 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  =  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
425 stoweidlem26.5 . . . . . . . . . . . . 13  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
426424, 425fvmptg 5936 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... N )  /\  { t  e.  T  | 
( ( i  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) }  e.  _V )  ->  ( B `
 i )  =  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
427156, 420, 426syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( B `  i )  =  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
428417, 427eleqtrrd 2532 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  ( B `  i
) )
4291513ad2ant1 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  (
( L  -  2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2 )  <_  N ) )
430429, 152sylibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  N  e.  ( ZZ>= `  ( L  -  2 ) ) )
431430, 154syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  (
0 ... ( L  - 
2 ) )  C_  ( 0 ... N
) )
432 simp2 996 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  i  e.  ( 0 ... ( L  -  2 ) ) )
433431, 432sseldd 3488 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  i  e.  ( 0 ... N
) )
434 elex 3102 . . . . . . . . . . . . 13  |-  ( S  e.  ( B `  i )  ->  S  e.  _V )
4354343ad2ant3 1018 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )  ->  S  e.  _V )
436 nfcv 2603 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t
( 0 ... N
)
437 nfrab1 3022 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
438436, 437nfmpt 4522 . . . . . . . . . . . . . . . . . 18  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
439425, 438nfcxfr 2601 . . . . . . . . . . . . . . . . 17  |-  F/_ t B
440 nfcv 2603 . . . . . . . . . . . . . . . . 17  |-  F/_ t
i
441439, 440nffv 5860 . . . . . . . . . . . . . . . 16  |-  F/_ t
( B `  i
)
442441nfel2 2621 . . . . . . . . . . . . . . 15  |-  F/ t  S  e.  ( B `
 i )
44394, 95, 442nf3an 1914 . . . . . . . . . . . . . 14  |-  F/ t ( ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )
444 nfv 1692 . . . . . . . . . . . . . 14  |-  F/ t ( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S )
445443, 444nfim 1904 . . . . . . . . . . . . 13  |-  F/ t ( ( ph  /\  i  e.  ( 0 ... N )  /\  S  e.  ( B `  i ) )  -> 
( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S ) )
446 eleq1 2513 . . . . . . . . . . . . . . 15  |-  ( t  =  S  ->  (
t  e.  ( B `
 i )  <->  S  e.  ( B `  i ) ) )
4474463anbi3d 1304 . . . . . . . . . . . . . 14  |-  ( t  =  S  ->  (
( ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  ( B `  i ) )  <->  ( ph  /\  i  e.  ( 0 ... N )  /\  S  e.  ( B `  i ) ) ) )
44899breq2d 4446 . . . . . . . . . . . . . 14  |-  ( t  =  S  ->  (
( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) ) )
449447, 448imbi12d 320 . . . . . . . . . . . . 13  |-  ( t  =  S  ->  (
( ( ph  /\  i  e.  ( 0 ... N )  /\  t  e.  ( B `  i ) )  -> 
( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  t ) )  <->  ( ( ph  /\  i  e.  ( 0 ... N )  /\  S  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) ) ) )
450 stoweidlem26.15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  t
) )
451445, 449, 450vtoclg1f 3150 . . . . . . . . . . . 12  |-  ( S  e.  _V  ->  (
( ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) ) )
452435, 451mpcom 36 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) )
453433, 452syld3an2 1274 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  (
1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S ) )
454428, 453mpd3an3 1324 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S ) )
455454adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) )
456285, 287, 288, 291, 455fsumlt 13590 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  <  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `  i ) `  S
) )
457284, 456eqbrtrrd 4456 . . . . . 6  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  <  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `
 i ) `  S ) )
458127adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  e.  RR )
459158adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )  e.  RR )
460313adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  e.  RR  /\  0  <  E ) )
461 ltmul2 10396 . . . . . . 7  |-  ( ( ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  e.  RR  /\  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  -> 
( ( ( 1  -  ( E  /  N ) )  x.  ( L  -  1 ) )  <  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )  <->  ( E  x.  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  <  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
) ) )
462458, 459, 460, 461syl3anc 1227 . . . . . 6  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( ( 1  -  ( E  /  N ) )  x.  ( L  -  1 ) )  <  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )  <->  ( E  x.  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  <  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
) ) )
463457, 462mpbid 210 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  <  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
) )
464121, 129, 160, 233, 463lttrd 9743 . . . 4  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `  i ) `  S
) ) )
465156, 58syldan 470 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
466465adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
467466recnd 9622 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  CC )
468285, 467fsumcl 13531 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  CC )
469468addid1d 9780 . . . . . 6  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  (
( X `  i
) `  S )
)  +  0 )  =  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  (
( X `  i
) `  S )
) )
470 0red 9597 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  e.  RR )
471 fzfid 12059 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  - 
1 ) ... N
)  e.  Fin )
47214adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  E  e.  RR )
473 0red 9597 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  e.  RR )
474126adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( L  -  1 )  e.  RR )
475 elfzelz 11694 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( ( L  -  1 ) ... N )  ->  i  e.  ZZ )
476475zred 10971 . . . . . . . . . . . . . 14  |-  ( i  e.  ( ( L  -  1 ) ... N )  ->  i  e.  RR )
477476adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  RR )
478 1m1e0 10607 . . . . . . . . . . . . . . 15  |-  ( 1  -  1 )  =  0
479122, 114, 122, 365lesub1dd 10171 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  -  1 )  <_  ( L  -  1 ) )
480478, 479syl5eqbrr 4468 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <_  ( L  -  1 ) )
481480adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  ( L  -  1 ) )
482 simpr 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  ( ( L  - 
1 ) ... N
) )
483475adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  ZZ )
484379adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( L  -  1 )  e.  ZZ )
485135adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  N  e.  ZZ )
486 elfz 11684 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ZZ  /\  ( L  -  1
)  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  e.  ( ( L  -  1 ) ... N )  <-> 
( ( L  - 
1 )  <_  i  /\  i  <_  N ) ) )
487483, 484, 485, 486syl3anc 1227 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
i  e.  ( ( L  -  1 ) ... N )  <->  ( ( L  -  1 )  <_  i  /\  i  <_  N ) ) )
488482, 487mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
( L  -  1 )  <_  i  /\  i  <_  N ) )
489488simpld 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( L  -  1 )  <_  i )
490473, 474, 477, 481, 489letrd 9739 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  i )
491 elfzle2 11696 . . . . . . . . . . . . 13  |-  ( i  e.  ( ( L  -  1 ) ... N )  ->  i  <_  N )
492491adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  <_  N )
493 0zd 10879 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  e.  ZZ )
494 elfz 11684 . . . . . . . . . . . . 13  |-  ( ( i  e.  ZZ  /\  0  e.  ZZ  /\  N  e.  ZZ )  ->  (
i  e.  ( 0 ... N )  <->  ( 0  <_  i  /\  i  <_  N ) ) )
495483, 493, 485, 494syl3anc 1227 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
i  e.  ( 0 ... N )  <->  ( 0  <_  i  /\  i  <_  N ) ) )
496490, 492, 495mpbir2and 920 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  ( 0 ... N
) )
497496, 57syldan 470 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
( X `  i
) `  S )  e.  RR )
498472, 497remulcld 9624 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
499498adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( ( L  -  1 ) ... N ) )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
500471, 499fsumrecl 13532 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( ( L  -  1 ) ... N ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  RR )
501285, 466fsumrecl 13532 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  RR )
502 fzfid 12059 . . . . . . . . 9  |-  ( ph  ->  ( ( L  - 
1 ) ... N
)  e.  Fin )
503182adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  E  e.  CC )
504503mul01d 9779 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  x.  0 )  =  0 )
505496, 106syldan 470 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) )
506313adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  e.  RR  /\  0  <  E ) )
507 lemul2 10398 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  ( ( X `  i ) `  S
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( 0  <_  ( ( X `
 i ) `  S )  <->  ( E  x.  0 )  <_  ( E  x.  ( ( X `  i ) `  S ) ) ) )
508473, 497, 506, 507syl3anc 1227 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
0  <_  ( ( X `  i ) `  S )  <->  ( E  x.  0 )  <_  ( E  x.  ( ( X `  i ) `  S ) ) ) )
509505, 508mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  x.  0 )  <_  ( E  x.  ( ( X `  i ) `  S
) ) )
510504, 509eqbrtrrd 4456 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  ( E  x.  (
( X `  i
) `  S )
) )
511502, 498, 510fsumge0 13585 . . . . . . . 8  |-  ( ph  ->  0  <_  sum_ i  e.  ( ( L  - 
1 ) ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
512511adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  <_  sum_ i  e.  ( ( L  - 
1 ) ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
513470, 500, 501, 512leadd2dd 10170 . . . . . 6  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  (
( X `  i
) `  S )
)  +  0 )  <_  ( sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  ( ( X `  i ) `  S
) )  +  sum_ i  e.  ( ( L  -  1 ) ... N ) ( E  x.  ( ( X `  i ) `
 S ) ) ) )
514469, 513eqbrtrrd 4456 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( E  x.  ( ( X `  i ) `
 S ) )  <_  ( sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  ( ( X `  i ) `  S
) )  +  sum_ i  e.  ( ( L  -  1 ) ... N ) ( E  x.  ( ( X `  i ) `
 S ) ) ) )
515157recnd 9622 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( X `  i
) `  S )  e.  CC )
516130, 182, 515fsummulc2 13575 . . . . . 6  |-  ( ph  ->  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  =  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  ( ( X `  i ) `  S
) ) )
517516adantr 465 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  =  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  ( ( X `  i ) `  S
) ) )
518 stoweidlem26.2 . . . . . . . . 9  |-  F/ j
ph
519 elfzelz 11694 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( L  -  2 ) )  ->  j  e.  ZZ )
520519adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  e.  ZZ )
521520zred 10971 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  e.  RR )
522318adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  RR )
523126adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  1 )  e.  RR )
524 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  e.  ( 0 ... ( L  -  2 ) ) )
525 0zd 10879 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  0  e.  ZZ )
526134adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  ZZ )
527 elfz 11684 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ )  -> 
( j  e.  ( 0 ... ( L  -  2 ) )  <-> 
( 0  <_  j  /\  j  <_  ( L  -  2 ) ) ) )
528520, 525, 526, 527syl3anc 1227 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
j  e.  ( 0 ... ( L  - 
2 ) )  <->  ( 0  <_  j  /\  j  <_  ( L  -  2 ) ) ) )
529524, 528mpbid 210 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
0  <_  j  /\  j  <_  ( L  - 
2 ) ) )
530529simprd 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  <_  ( L  -  2 ) )
531122, 138, 114ltsub2d 10165 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  <  2  <->  ( L  -  2 )  <  ( L  - 
1 ) ) )
532355, 531mpbii 211 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  2 )  <  ( L  -  1 ) )
533532adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  <  ( L  - 
1 ) )
534521, 522, 523, 530, 533lelttrd 9740 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  <  ( L  -  1 ) )
535521, 523ltnled 9732 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
j  <  ( L  -  1 )  <->  -.  ( L  -  1 )  <_  j ) )
536534, 535mpbid 210 . . . . . . . . . . . 12  |-  (