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

Theorem stoweidlem26 27642
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 9046 . . . . . . . 8  |-  1  e.  RR
2 eleq1 2464 . . . . . . . 8  |-  ( L  =  1  ->  ( L  e.  RR  <->  1  e.  RR ) )
31, 2mpbiri 225 . . . . . . 7  |-  ( L  =  1  ->  L  e.  RR )
43adantl 453 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  L  e.  RR )
5 4re 10029 . . . . . . . 8  |-  4  e.  RR
65a1i 11 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  4  e.  RR )
7 3re 10027 . . . . . . . 8  |-  3  e.  RR
87a1i 11 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  3  e.  RR )
9 3ne0 10041 . . . . . . . 8  |-  3  =/=  0
109a1i 11 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  3  =/=  0 )
116, 8, 10redivcld 9798 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  /  3 )  e.  RR )
124, 11resubcld 9421 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  e.  RR )
13 stoweidlem26.11 . . . . . . 7  |-  ( ph  ->  E  e.  RR+ )
1413rpred 10604 . . . . . 6  |-  ( ph  ->  E  e.  RR )
1514adantr 452 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  E  e.  RR )
1612, 15remulcld 9072 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  e.  RR )
17 0re 9047 . . . . 5  |-  0  e.  RR
1817a1i 11 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  0  e.  RR )
19 fzfid 11267 . . . . . 6  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
2014adantr 452 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  E  e.  RR )
21 stoweidlem26.13 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
22 stoweidlem26.9 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  ( ( D `  L ) 
\  ( D `  ( L  -  1
) ) ) )
23 eldif 3290 . . . . . . . . . . . . . 14  |-  ( S  e.  ( ( D `
 L )  \ 
( D `  ( L  -  1 ) ) )  <->  ( S  e.  ( D `  L
)  /\  -.  S  e.  ( D `  ( L  -  1 ) ) ) )
2422, 23sylib 189 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  ( D `  L )  /\  -.  S  e.  ( D `  ( L  -  1 ) ) ) )
2524simpld 446 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  ( D `
 L ) )
26 1e0p1 10366 . . . . . . . . . . . . . . . 16  |-  1  =  ( 0  +  1 )
2726oveq1i 6050 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  =  ( ( 0  +  1 ) ... N
)
28 0z 10249 . . . . . . . . . . . . . . . 16  |-  0  e.  ZZ
29 fzp1ss 11054 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  ZZ  ->  (
( 0  +  1 ) ... N ) 
C_  ( 0 ... N ) )
3028, 29ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( ( 0  +  1 ) ... N )  C_  ( 0 ... N
)
3127, 30eqsstri 3338 . . . . . . . . . . . . . 14  |-  ( 1 ... N )  C_  ( 0 ... N
)
32 stoweidlem26.8 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  e.  ( 1 ... N ) )
3331, 32sseldi 3306 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  ( 0 ... N ) )
34 stoweidlem26.7 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  e.  _V )
35 rabexg 4313 . . . . . . . . . . . . . 14  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
3634, 35syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
37 oveq1 6047 . . . . . . . . . . . . . . . . 17  |-  ( j  =  L  ->  (
j  -  ( 1  /  3 ) )  =  ( L  -  ( 1  /  3
) ) )
3837oveq1d 6055 . . . . . . . . . . . . . . . 16  |-  ( j  =  L  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( L  -  ( 1  / 
3 ) )  x.  E ) )
3938breq2d 4184 . . . . . . . . . . . . . . 15  |-  ( j  =  L  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) ) )
4039rabbidv 2908 . . . . . . . . . . . . . 14  |-  ( j  =  L  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) } )
41 stoweidlem26.4 . . . . . . . . . . . . . 14  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
4240, 41fvmptg 5763 . . . . . . . . . . . . 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 ) } )
4333, 36, 42syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( D `  L
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
4425, 43eleqtrd 2480 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
45 nfcv 2540 . . . . . . . . . . . 12  |-  F/_ t S
46 nfcv 2540 . . . . . . . . . . . 12  |-  F/_ t T
47 stoweidlem26.1 . . . . . . . . . . . . . 14  |-  F/_ t F
4847, 45nffv 5694 . . . . . . . . . . . . 13  |-  F/_ t
( F `  S
)
49 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ t  <_
50 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ t
( ( L  -  ( 1  /  3
) )  x.  E
)
5148, 49, 50nfbr 4216 . . . . . . . . . . . 12  |-  F/ t ( F `  S
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E )
52 fveq2 5687 . . . . . . . . . . . . 13  |-  ( t  =  S  ->  ( F `  t )  =  ( F `  S ) )
5352breq1d 4182 . . . . . . . . . . . 12  |-  ( t  =  S  ->  (
( F `  t
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  S )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) ) )
5445, 46, 51, 53elrabf 3051 . . . . . . . . . . 11  |-  ( S  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( L  -  ( 1  /  3
) )  x.  E
) }  <->  ( S  e.  T  /\  ( F `  S )  <_  ( ( L  -  ( 1  /  3
) )  x.  E
) ) )
5544, 54sylib 189 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  T  /\  ( F `  S
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E ) ) )
5655simpld 446 . . . . . . . . 9  |-  ( ph  ->  S  e.  T )
5756adantr 452 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  S  e.  T )
5821, 57ffvelrnd 5830 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  S )  e.  RR )
5920, 58remulcld 9072 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
6019, 59fsumrecl 12483 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
)  e.  RR )
6160adantr 452 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
625, 7, 9redivcli 9737 . . . . . . 7  |-  ( 4  /  3 )  e.  RR
6362a1i 11 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  /  3 )  e.  RR )
644, 63resubcld 9421 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  e.  RR )
654recnd 9070 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  L  e.  CC )
6665subid1d 9356 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  0 )  =  L )
67 3cn 10028 . . . . . . . . . 10  |-  3  e.  CC
6867, 9dividi 9703 . . . . . . . . 9  |-  ( 3  /  3 )  =  1
69 3lt4 10101 . . . . . . . . . 10  |-  3  <  4
70 3pos 10040 . . . . . . . . . . 11  |-  0  <  3
717, 5, 7, 70ltdiv1ii 9896 . . . . . . . . . 10  |-  ( 3  <  4  <->  ( 3  /  3 )  < 
( 4  /  3
) )
7269, 71mpbi 200 . . . . . . . . 9  |-  ( 3  /  3 )  < 
( 4  /  3
)
7368, 72eqbrtrri 4193 . . . . . . . 8  |-  1  <  ( 4  /  3
)
74 breq1 4175 . . . . . . . . 9  |-  ( L  =  1  ->  ( L  <  ( 4  / 
3 )  <->  1  <  ( 4  /  3 ) ) )
7574adantl 453 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  <  ( 4  / 
3 )  <->  1  <  ( 4  /  3 ) ) )
7673, 75mpbiri 225 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  L  <  ( 4  /  3
) )
7766, 76eqbrtrd 4192 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  0 )  <  ( 4  / 
3 ) )
784, 18, 63, 77ltsub23d 9587 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  <  0 )
7913rpgt0d 10607 . . . . . 6  |-  ( ph  ->  0  <  E )
8079adantr 452 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  0  <  E )
81 mulltgt0 27560 . . . . 5  |-  ( ( ( ( L  -  ( 4  /  3
) )  e.  RR  /\  ( L  -  (
4  /  3 ) )  <  0 )  /\  ( E  e.  RR  /\  0  < 
E ) )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  0 )
8264, 78, 15, 80, 81syl22anc 1185 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  0 )
83 0cn 9040 . . . . . . . 8  |-  0  e.  CC
84 fsumconst 12528 . . . . . . . 8  |-  ( ( ( 0 ... N
)  e.  Fin  /\  0  e.  CC )  -> 
sum_ i  e.  ( 0 ... N ) 0  =  ( (
# `  ( 0 ... N ) )  x.  0 ) )
8519, 83, 84sylancl 644 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  =  ( (
# `  ( 0 ... N ) )  x.  0 ) )
86 hashcl 11594 . . . . . . . . 9  |-  ( ( 0 ... N )  e.  Fin  ->  ( # `
 ( 0 ... N ) )  e. 
NN0 )
87 nn0cn 10187 . . . . . . . . 9  |-  ( (
# `  ( 0 ... N ) )  e. 
NN0  ->  ( # `  (
0 ... N ) )  e.  CC )
8819, 86, 873syl 19 . . . . . . . 8  |-  ( ph  ->  ( # `  (
0 ... N ) )  e.  CC )
8988mul01d 9221 . . . . . . 7  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  x.  0 )  =  0 )
9085, 89eqtrd 2436 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  =  0 )
9190adantr 452 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) 0  =  0 )
9217a1i 11 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  e.  RR )
9313rpge0d 10608 . . . . . . . . 9  |-  ( ph  ->  0  <_  E )
9493adantr 452 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  E )
95 stoweidlem26.3 . . . . . . . . . . . 12  |-  F/ t
ph
96 nfv 1626 . . . . . . . . . . . 12  |-  F/ t  i  e.  ( 0 ... N )
9795, 96nfan 1842 . . . . . . . . . . 11  |-  F/ t ( ph  /\  i  e.  ( 0 ... N
) )
98 nfv 1626 . . . . . . . . . . 11  |-  F/ t 0  <_  ( ( X `  i ) `  S )
9997, 98nfim 1828 . . . . . . . . . 10  |-  F/ t ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  S )
)
100 fveq2 5687 . . . . . . . . . . . 12  |-  ( t  =  S  ->  (
( X `  i
) `  t )  =  ( ( X `
 i ) `  S ) )
101100breq2d 4184 . . . . . . . . . . 11  |-  ( t  =  S  ->  (
0  <_  ( ( X `  i ) `  t )  <->  0  <_  ( ( X `  i
) `  S )
) )
102101imbi2d 308 . . . . . . . . . 10  |-  ( t  =  S  ->  (
( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  t )
)  <->  ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  S )
) ) )
103 stoweidlem26.14 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )  ->  0  <_  ( ( X `  i ) `  t
) )
1041033expia 1155 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
t  e.  T  -> 
0  <_  ( ( X `  i ) `  t ) ) )
105104com12 29 . . . . . . . . . 10  |-  ( t  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  t
) ) )
10645, 99, 102, 105vtoclgaf 2976 . . . . . . . . 9  |-  ( S  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) ) )
10757, 106mpcom 34 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) )
10820, 58, 94, 107mulge0d 9559 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( E  x.  (
( X `  i
) `  S )
) )
10919, 92, 59, 108fsumle 12533 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
110109adantr 452 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) 0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
11191, 110eqbrtrrd 4194 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  0  <_ 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) )
11216, 18, 61, 82, 111ltletrd 9186 . . 3  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) )
113 elfzelz 11015 . . . . . . . . 9  |-  ( L  e.  ( 1 ... N )  ->  L  e.  ZZ )
114 zre 10242 . . . . . . . . 9  |-  ( L  e.  ZZ  ->  L  e.  RR )
11532, 113, 1143syl 19 . . . . . . . 8  |-  ( ph  ->  L  e.  RR )
1165a1i 11 . . . . . . . . 9  |-  ( ph  ->  4  e.  RR )
1177a1i 11 . . . . . . . . 9  |-  ( ph  ->  3  e.  RR )
1189a1i 11 . . . . . . . . 9  |-  ( ph  ->  3  =/=  0 )
119116, 117, 118redivcld 9798 . . . . . . . 8  |-  ( ph  ->  ( 4  /  3
)  e.  RR )
120115, 119resubcld 9421 . . . . . . 7  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  e.  RR )
121120, 14remulcld 9072 . . . . . 6  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR )
122121adantr 452 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR )
1231a1i 11 . . . . . . . . 9  |-  ( ph  ->  1  e.  RR )
124 stoweidlem26.6 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
12514, 124nndivred 10004 . . . . . . . . 9  |-  ( ph  ->  ( E  /  N
)  e.  RR )
126123, 125resubcld 9421 . . . . . . . 8  |-  ( ph  ->  ( 1  -  ( E  /  N ) )  e.  RR )
127115, 123resubcld 9421 . . . . . . . 8  |-  ( ph  ->  ( L  -  1 )  e.  RR )
128126, 127remulcld 9072 . . . . . . 7  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  e.  RR )
12914, 128remulcld 9072 . . . . . 6  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  e.  RR )
130129adantr 452 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  e.  RR )
131 fzfid 11267 . . . . . . . 8  |-  ( ph  ->  ( 0 ... ( L  -  2 ) )  e.  Fin )
13232, 113syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  e.  ZZ )
133 2z 10268 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
134133a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  2  e.  ZZ )
135132, 134zsubcld 10336 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  2 )  e.  ZZ )
136124nnzd 10330 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
137132zred 10331 . . . . . . . . . . . . . . 15  |-  ( ph  ->  L  e.  RR )
138 2re 10025 . . . . . . . . . . . . . . . 16  |-  2  e.  RR
139138a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  e.  RR )
140137, 139resubcld 9421 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  2 )  e.  RR )
141124nnred 9971 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  RR )
142 2pos 10038 . . . . . . . . . . . . . . . . 17  |-  0  <  2
14317, 138, 142ltleii 9152 . . . . . . . . . . . . . . . 16  |-  0  <_  2
14417a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  e.  RR )
145144, 139, 137lesub2d 9590 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  <_  2  <->  ( L  -  2 )  <_  ( L  - 
0 ) ) )
146143, 145mpbii 203 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  2 )  <_  ( L  -  0 ) )
147132zcnd 10332 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  L  e.  CC )
148147subid1d 9356 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  0 )  =  L )
149146, 148breqtrd 4196 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  2 )  <_  L )
150 elfzle2 11017 . . . . . . . . . . . . . . 15  |-  ( L  e.  ( 1 ... N )  ->  L  <_  N )
15132, 150syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  <_  N )
152140, 137, 141, 149, 151letrd 9183 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  2 )  <_  N )
153135, 136, 1523jca 1134 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2
)  <_  N )
)
154 eluz2 10450 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  ( L  -  2 ) )  <->  ( ( L  -  2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2 )  <_  N ) )
155153, 154sylibr 204 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  ( L  -  2
) ) )
156 fzss2 11048 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  ( L  -  2 ) )  ->  ( 0 ... ( L  - 
2 ) )  C_  ( 0 ... N
) )
157155, 156syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ... ( L  -  2 ) )  C_  ( 0 ... N ) )
158157sselda 3308 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  ( 0 ... N
) )
159158, 58syldan 457 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( X `  i
) `  S )  e.  RR )
160131, 159fsumrecl 12483 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `  i ) `  S
)  e.  RR )
16114, 160remulcld 9072 . . . . . 6  |-  ( ph  ->  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  e.  RR )
162161adantr 452 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  e.  RR )
16314, 127remulcld 9072 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  ( L  -  1 ) )  e.  RR )
16414, 14remulcld 9072 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  E
)  e.  RR )
165163, 164resubcld 9421 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  e.  RR )
166127, 124nndivred 10004 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  e.  RR )
167164, 166remulcld 9072 . . . . . . . . 9  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  e.  RR )
168163, 167resubcld 9421 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  (
( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) ) )  e.  RR )
169127, 14resubcld 9421 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  e.  RR )
170123, 14readdcld 9071 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
1711, 7, 9redivcli 9737 . . . . . . . . . . . . . . 15  |-  ( 1  /  3 )  e.  RR
172171a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
173 stoweidlem26.12 . . . . . . . . . . . . . 14  |-  ( ph  ->  E  <  ( 1  /  3 ) )
17414, 172, 123, 173ltadd2dd 9185 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  +  E
)  <  ( 1  +  ( 1  / 
3 ) ) )
175 ax-1cn 9004 . . . . . . . . . . . . . . 15  |-  1  e.  CC
17667, 175, 67, 9divdiri 9727 . . . . . . . . . . . . . 14  |-  ( ( 3  +  1 )  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
177 3p1e4 10060 . . . . . . . . . . . . . . 15  |-  ( 3  +  1 )  =  4
178177oveq1i 6050 . . . . . . . . . . . . . 14  |-  ( ( 3  +  1 )  /  3 )  =  ( 4  /  3
)
17968oveq1i 6050 . . . . . . . . . . . . . 14  |-  ( ( 3  /  3 )  +  ( 1  / 
3 ) )  =  ( 1  +  ( 1  /  3 ) )
180176, 178, 1793eqtr3ri 2433 . . . . . . . . . . . . 13  |-  ( 1  +  ( 1  / 
3 ) )  =  ( 4  /  3
)
181174, 180syl6breq 4211 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  E
)  <  ( 4  /  3 ) )
182170, 119, 115, 181ltsub2dd 9595 . . . . . . . . . . 11  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  <  ( L  -  ( 1  +  E ) ) )
183175a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  CC )
18413rpcnd 10606 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  CC )
185147, 183, 184subsub4d 9398 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  =  ( L  -  ( 1  +  E ) ) )
186182, 185breqtrrd 4198 . . . . . . . . . 10  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  <  ( ( L  -  1 )  -  E ) )
187120, 169, 13, 186ltmul1dd 10655 . . . . . . . . 9  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( (
( L  -  1 )  -  E )  x.  E ) )
188147, 183subcld 9367 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  -  1 )  e.  CC )
189188, 184subcld 9367 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  e.  CC )
190184, 189mulcomd 9065 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( ( L  -  1 )  -  E )  x.  E ) )
191184, 188, 184subdid 9445 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
192190, 191eqtr3d 2438 . . . . . . . . 9  |-  ( ph  ->  ( ( ( L  -  1 )  -  E )  x.  E
)  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
193187, 192breqtrd 4196 . . . . . . . 8  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
194 1z 10267 . . . . . . . . . . . . . . . . . 18  |-  1  e.  ZZ
195194a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
196 elfz 11005 . . . . . . . . . . . . . . . . 17  |-  ( ( L  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )  ->  ( L  e.  ( 1 ... N )  <->  ( 1  <_  L  /\  L  <_  N ) ) )
197132, 195, 136, 196syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( L  e.  ( 1 ... N )  <-> 
( 1  <_  L  /\  L  <_  N ) ) )
19832, 197mpbid 202 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  <_  L  /\  L  <_  N ) )
199198simprd 450 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  <_  N )
200 zlem1lt 10283 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  ZZ  /\  N  e.  ZZ )  ->  ( L  <_  N  <->  ( L  -  1 )  <  N ) )
201132, 136, 200syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  <_  N  <->  ( L  -  1 )  <  N ) )
202199, 201mpbid 202 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  1 )  <  N )
203124nngt0d 9999 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  N )
204 ltdiv1 9830 . . . . . . . . . . . . . 14  |-  ( ( ( L  -  1 )  e.  RR  /\  N  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) )  -> 
( ( L  - 
1 )  <  N  <->  ( ( L  -  1 )  /  N )  <  ( N  /  N ) ) )
205127, 141, 141, 203, 204syl112anc 1188 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  - 
1 )  <  N  <->  ( ( L  -  1 )  /  N )  <  ( N  /  N ) ) )
206202, 205mpbid 202 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  <  ( N  /  N ) )
207124nncnd 9972 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
208124nnne0d 10000 . . . . . . . . . . . . 13  |-  ( ph  ->  N  =/=  0 )
209207, 208dividd 9744 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  /  N
)  =  1 )
210206, 209breqtrd 4196 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  <  1 )
21114, 14, 79, 79mulgt0d 9181 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  ( E  x.  E ) )
212 ltmul2 9817 . . . . . . . . . . . 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 ) ) )
213166, 123, 164, 211, 212syl112anc 1188 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  -  1 )  /  N )  <  1  <->  ( ( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) )  <  ( ( E  x.  E )  x.  1 ) ) )
214210, 213mpbid 202 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  <  ( ( E  x.  E )  x.  1 ) )
215184, 184mulcld 9064 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  E
)  e.  CC )
216215mulid1d 9061 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  E )  x.  1 )  =  ( E  x.  E ) )
217214, 216breqtrd 4196 . . . . . . . . 9  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  <  ( E  x.  E ) )
218167, 164, 163, 217ltsub2dd 9595 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) )
219121, 165, 168, 193, 218lttrd 9187 . . . . . . 7  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) )
220184, 207, 208divcld 9746 . . . . . . . . . . 11  |-  ( ph  ->  ( E  /  N
)  e.  CC )
221183, 220, 188subdird 9446 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  =  ( ( 1  x.  ( L  -  1 ) )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
222188mulid2d 9062 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  x.  ( L  -  1 ) )  =  ( L  -  1 ) )
223222oveq1d 6055 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  x.  ( L  -  1 ) )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( ( L  -  1 )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
224221, 223eqtrd 2436 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  =  ( ( L  -  1 )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
225224oveq2d 6056 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( E  x.  ( ( L  - 
1 )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) ) ) )
226220, 188mulcld 9064 . . . . . . . . 9  |-  ( ph  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  e.  CC )
227184, 188, 226subdid 9445 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  ( ( E  /  N )  x.  ( L  - 
1 ) ) ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) ) )
228184, 207, 188, 208div32d 9769 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  =  ( E  x.  ( ( L  -  1 )  /  N ) ) )
229228oveq2d 6056 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
230188, 207, 208divcld 9746 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  e.  CC )
231184, 184, 230mulassd 9067 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
232229, 231eqtr4d 2439 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( ( E  x.  E )  x.  ( ( L  -  1 )  /  N ) ) )
233232oveq2d 6056 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )
234225, 227, 2333eqtrd 2440 . . . . . . 7  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )
235219, 234breqtrrd 4198 . . . . . 6  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) ) )
236235adantr 452 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) ) )
237183, 220subcld 9367 . . . . . . . . . 10  |-  ( ph  ->  ( 1  -  ( E  /  N ) )  e.  CC )
238 fsumconst 12528 . . . . . . . . . 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 ) ) ) )
239131, 237, 238syl2anc 643 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
240239adantr 452 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
24128a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  e.  ZZ )
24232adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( 1 ... N ) )
243242, 113syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ZZ )
244133a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  e.  ZZ )
245243, 244zsubcld 10336 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  -  2 )  e.  ZZ )
246 elnnuz 10478 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  <->  N  e.  ( ZZ>= `  1 )
)
247124, 246sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
248 elfzp12 11081 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( L  e.  ( 1 ... N
)  <->  ( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N
) ) ) )
249247, 248syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  ( 1 ... N )  <-> 
( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N ) ) ) )
25032, 249mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N ) ) )
251250orcanai 880 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( (
1  +  1 ) ... N ) )
252 1p1e2 10050 . . . . . . . . . . . . . . . . . 18  |-  ( 1  +  1 )  =  2
253252a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 1  +  1 )  =  2 )
254253oveq1d 6055 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  +  1 ) ... N
)  =  ( 2 ... N ) )
255251, 254eleqtrd 2480 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( 2 ... N ) )
256 elfzle1 11016 . . . . . . . . . . . . . . 15  |-  ( L  e.  ( 2 ... N )  ->  2  <_  L )
257255, 256syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  <_  L )
258115adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  RR )
259138a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  e.  RR )
260258, 259subge0d 9572 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0  <_  ( L  -  2 )  <->  2  <_  L )
)
261257, 260mpbird 224 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  <_  ( L  -  2 ) )
262241, 245, 2613jca 1134 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ  /\  0  <_  ( L  - 
2 ) ) )
263 eluz2 10450 . . . . . . . . . . . 12  |-  ( ( L  -  2 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ  /\  0  <_ 
( L  -  2 ) ) )
264262, 263sylibr 204 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  -  2 )  e.  ( ZZ>= ` 
0 ) )
265 hashfz 11647 . . . . . . . . . . 11  |-  ( ( L  -  2 )  e.  ( ZZ>= `  0
)  ->  ( # `  (
0 ... ( L  - 
2 ) ) )  =  ( ( ( L  -  2 )  -  0 )  +  1 ) )
266264, 265syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( # `  ( 0 ... ( L  - 
2 ) ) )  =  ( ( ( L  -  2 )  -  0 )  +  1 ) )
267 2cn 10026 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
268267a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  e.  CC )
269147, 268subcld 9367 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  2 )  e.  CC )
270269subid1d 9356 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  - 
2 )  -  0 )  =  ( L  -  2 ) )
271270oveq1d 6055 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( ( L  -  2 )  +  1 ) )
272147, 268, 183subadd23d 9389 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
2 )  +  1 )  =  ( L  +  ( 1  -  2 ) ) )
273267, 175negsubdi2i 9342 . . . . . . . . . . . . . . . 16  |-  -u (
2  -  1 )  =  ( 1  -  2 )
274 2m1e1 10051 . . . . . . . . . . . . . . . . 17  |-  ( 2  -  1 )  =  1
275274negeqi 9255 . . . . . . . . . . . . . . . 16  |-  -u (
2  -  1 )  =  -u 1
276273, 275eqtr3i 2426 . . . . . . . . . . . . . . 15  |-  ( 1  -  2 )  = 
-u 1
277276a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  -  2 )  =  -u 1
)
278277oveq2d 6056 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  +  ( 1  -  2 ) )  =  ( L  +  -u 1 ) )
279147, 183negsubd 9373 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  +  -u
1 )  =  ( L  -  1 ) )
280278, 279eqtrd 2436 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  +  ( 1  -  2 ) )  =  ( L  -  1 ) )
281271, 272, 2803eqtrd 2440 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( L  -  1 ) )
282281adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( L  -  1 ) )
283266, 282eqtrd 2436 . . . . . . . . 9  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( # `  ( 0 ... ( L  - 
2 ) ) )  =  ( L  - 
1 ) )
284283oveq1d 6055 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( # `  (
0 ... ( L  - 
2 ) ) )  x.  ( 1  -  ( E  /  N
) ) )  =  ( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) ) )
285188, 237mulcomd 9065 . . . . . . . . 9  |-  ( ph  ->  ( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
286285adantr 452 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
287240, 284, 2863eqtrd 2440 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  -  1 ) ) )
288 fzfid 11267 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0 ... ( L  -  2 ) )  e.  Fin )
289 fzn0 11026 . . . . . . . . 9  |-  ( ( 0 ... ( L  -  2 ) )  =/=  (/)  <->  ( L  - 
2 )  e.  (
ZZ>= `  0 ) )
290264, 289sylibr 204 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0 ... ( L  -  2 ) )  =/=  (/) )
291126ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( 1  -  ( E  /  N ) )  e.  RR )
292 simpll 731 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ph )
293158adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  ( 0 ... N
) )
294292, 293, 58syl2anc 643 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( ( X `  i ) `  S )  e.  RR )
29556adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  T )
296 elfzelz 11015 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  e.  ZZ )
297296zred 10331 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  e.  RR )
298297adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  RR )
299171a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
1  /  3 )  e.  RR )
300298, 299readdcld 9071 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  +  ( 1  /  3 ) )  e.  RR )
30114adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  E  e.  RR )
302300, 301remulcld 9072 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  e.  RR )
303115adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  L  e.  RR )
304138a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  2  e.  RR )
305303, 304resubcld 9421 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  RR )
306305, 299readdcld 9071 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( L  -  2 )  +  ( 1  /  3 ) )  e.  RR )
307306, 301remulcld 9072 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( ( L  - 
2 )  +  ( 1  /  3 ) )  x.  E )  e.  RR )
308 stoweidlem26.10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : T --> RR )
309308, 56jca 519 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F : T --> RR  /\  S  e.  T
) )
310309adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( F : T --> RR  /\  S  e.  T )
)
311 ffvelrn 5827 . . . . . . . . . . . . . 14  |-  ( ( F : T --> RR  /\  S  e.  T )  ->  ( F `  S
)  e.  RR )
312310, 311syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( F `  S )  e.  RR )
313 elfzle2 11017 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  <_  ( L  -  2 ) )
314313adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  <_  ( L  -  2 ) )
315298, 305, 299, 314leadd1dd 9596 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  +  ( 1  /  3 ) )  <_  ( ( L  -  2 )  +  ( 1  /  3
) ) )
31614, 79jca 519 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
317316adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  e.  RR  /\  0  <  E ) )
318 lemul1 9818 . . . . . . . . . . . . . . 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
) ) )
319300, 306, 317, 318syl3anc 1184 . . . . . . . . . . . . . 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
) ) )
320315, 319mpbid 202 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( ( ( L  -  2 )  +  ( 1  / 
3 ) )  x.  E ) )
321115, 139resubcld 9421 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  2 )  e.  RR )
322321, 172readdcld 9071 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
2 )  +  ( 1  /  3 ) )  e.  RR )
323322, 14remulcld 9072 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  e.  RR )
324308, 56ffvelrnd 5830 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  S
)  e.  RR )
325127, 172resubcld 9421 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( L  - 
1 )  -  (
1  /  3 ) )  e.  RR )
326325, 14remulcld 9072 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  e.  RR )
327 addid1 9202 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  CC  ->  (
1  +  0 )  =  1 )
328327eqcomd 2409 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  e.  CC  ->  1  =  ( 1  +  0 ) )
329175, 328mp1i 12 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  1  =  ( 1  +  0 ) )
330183subidd 9355 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1  -  1 )  =  0 )
331330eqcomd 2409 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  0  =  ( 1  -  1 ) )
332331oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  +  0 )  =  ( 1  +  ( 1  -  1 ) ) )
333 addsubass 9271 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
( 1  +  1 )  -  1 )  =  ( 1  +  ( 1  -  1 ) ) )
334333eqcomd 2409 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
1  +  ( 1  -  1 ) )  =  ( ( 1  +  1 )  - 
1 ) )
335183, 183, 183, 334syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  +  ( 1  -  1 ) )  =  ( ( 1  +  1 )  -  1 ) )
336329, 332, 3353eqtrd 2440 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  1  =  ( ( 1  +  1 )  -  1 ) )
337336oveq2d 6056 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  -  1 )  =  ( L  -  ( ( 1  +  1 )  - 
1 ) ) )
338252a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  +  1 )  =  2 )
339338oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1  +  1 )  -  1 )  =  ( 2  -  1 ) )
340339oveq2d 6056 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  -  (
( 1  +  1 )  -  1 ) )  =  ( L  -  ( 2  -  1 ) ) )
341147, 268, 183subsubd 9395 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  -  (
2  -  1 ) )  =  ( ( L  -  2 )  +  1 ) )
342337, 340, 3413eqtrd 2440 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  -  1 )  =  ( ( L  -  2 )  +  1 ) )
343342oveq1d 6055 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  =  ( ( ( L  -  2 )  +  1 )  -  ( 2  / 
3 ) ) )
344267, 67, 9divcli 9712 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  /  3 )  e.  CC
345344a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 2  /  3
)  e.  CC )
346269, 183, 345addsubassd 9387 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( L  -  2 )  +  1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  -  ( 2  /  3
) ) ) )
347175, 67, 9divcli 9712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  /  3 )  e.  CC
348 df-3 10015 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  3  =  ( 2  +  1 )
349348oveq1i 6050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 3  /  3 )  =  ( ( 2  +  1 )  /  3
)
350267, 175, 67, 9divdiri 9727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  +  1 )  /  3 )  =  ( ( 2  / 
3 )  +  ( 1  /  3 ) )
351349, 68, 3503eqtr3ri 2433 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  /  3 )  +  ( 1  / 
3 ) )  =  1
352175, 344, 347, 351subaddrii 9345 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  -  ( 2  / 
3 ) )  =  ( 1  /  3
)
353352a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  -  (
2  /  3 ) )  =  ( 1  /  3 ) )
354353oveq2d 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( L  - 
2 )  +  ( 1  -  ( 2  /  3 ) ) )  =  ( ( L  -  2 )  +  ( 1  / 
3 ) ) )
355343, 346, 3543eqtrd 2440 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  / 
3 ) ) )
356138, 7, 9redivcli 9737 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  /  3 )  e.  RR
357356a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 2  /  3
)  e.  RR )
358 1lt2 10098 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
3597, 70pm3.2i 442 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 3  e.  RR  /\  0  <  3 )
3601, 138, 3593pm3.2i 1132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  RR  /\  2  e.  RR  /\  ( 3  e.  RR  /\  0  <  3 ) )
361 ltdiv1 9830 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  (
3  e.  RR  /\  0  <  3 ) )  ->  ( 1  <  2  <->  ( 1  / 
3 )  <  (
2  /  3 ) ) )
362360, 361mp1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  <  2  <->  ( 1  /  3 )  <  ( 2  / 
3 ) ) )
363358, 362mpbii 203 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1  /  3
)  <  ( 2  /  3 ) )
364172, 357, 127, 363ltsub2dd 9595 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  <  ( ( L  -  1 )  -  ( 1  / 
3 ) ) )
365355, 364eqbrtrrd 4194 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( L  - 
2 )  +  ( 1  /  3 ) )  <  ( ( L  -  1 )  -  ( 1  / 
3 ) ) )
366322, 325, 13, 365ltmul1dd 10655 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  <  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) )
36724simprd 450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  -.  S  e.  ( D `  ( L  -  1 ) ) )
368198simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  1  <_  L )
369141, 123readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( N  +  1 )  e.  RR )
370141lep1d 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  N  <_  ( N  +  1 ) )
371115, 141, 369, 199, 370letrd 9183 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  L  <_  ( N  +  1 ) )
372136peano2zd 10334 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
373 elfz 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( L  e.  ZZ  /\  1  e.  ZZ  /\  ( N  +  1 )  e.  ZZ )  -> 
( L  e.  ( 1 ... ( N  +  1 ) )  <-> 
( 1  <_  L  /\  L  <_  ( N  +  1 ) ) ) )
374132, 195, 372, 373syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( L  e.  ( 1 ... ( N  +  1 ) )  <-> 
( 1  <_  L  /\  L  <_  ( N  +  1 ) ) ) )
375368, 371, 374mpbir2and 889 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  L  e.  ( 1 ... ( N  + 
1 ) ) )
376147, 183npcand 9371 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( L  - 
1 )  +  1 )  =  L )
37726eqcomi 2408 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  +  1 )  =  1
378377a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( 0  +  1 )  =  1 )
379378oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( 0  +  1 ) ... ( N  +  1 ) )  =  ( 1 ... ( N  + 
1 ) ) )
380375, 376, 3793eltr4d 2485 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( L  - 
1 )  +  1 )  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) ) )
38128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  0  e.  ZZ )
382132, 195zsubcld 10336 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( L  -  1 )  e.  ZZ )
383 fzaddel 11043 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
384381, 136, 382, 195, 383syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( L  - 
1 )  e.  ( 0 ... N )  <-> 
( ( L  - 
1 )  +  1 )  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) ) ) )
385380, 384mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( L  -  1 )  e.  ( 0 ... N ) )
386 rabexg 4313 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
38734, 386syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
388 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  ( L  - 
1 )  ->  (
j  -  ( 1  /  3 ) )  =  ( ( L  -  1 )  -  ( 1  /  3
) ) )
389388oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  ( L  - 
1 )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) )
390389breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  ( L  - 
1 )  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
391390rabbidv 2908 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) } )
392391, 41fvmptg 5763 . . . . . . . . . . . . . . . . . . . . . . . 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 ) } )
393385, 387, 392syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( D `  ( L  -  1 ) )  =  { t  e.  T  |  ( F `  t )  <_  ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } )
394367, 393neleqtrd 2499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  S  e.  {
t  e.  T  | 
( F `  t
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) } )
395 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t
( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)
39648, 49, 395nfbr 4216 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ t ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )
39752breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  S  ->  (
( F `  t
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
39845, 46, 396, 397elrabf 3051 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
399394, 398sylnib 296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  ( S  e.  T  /\  ( F `
 S )  <_ 
( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
400 ianor 475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( S  e.  T  /\  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) )  <-> 
( -.  S  e.  T  \/  -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
401399, 400sylib 189 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
402 olc 374 . . . . . . . . . . . . . . . . . . . . 21  |-  ( S  e.  T  ->  ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  \/  S  e.  T ) )
403402anim1i 552 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
40456, 401, 403syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  S  e.  T )  /\  ( -.  S  e.  T  \/  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) ) )
405 orcom 377 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  S  e.  T  \/  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) )  <->  ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  -.  S  e.  T ) )
406405anbi2i 676 . . . . . . . . . . . . . . . . . . 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 ) ) )
407404, 406sylib 189 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( -.  ( F `  S )  <_  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  \/  S  e.  T )  /\  ( -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E )  \/ 
-.  S  e.  T
) ) )
408 pm4.43 894 . . . . . . . . . . . . . . . . . 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 ) ) )
409407, 408sylibr 204 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  ( F `  S )  <_  (
( ( L  - 
1 )  -  (
1  /  3 ) )  x.  E ) )
410326, 324ltnled 9176 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( ( L  -  1 )  -  ( 1  / 
3 ) )  x.  E )  <  ( F `  S )  <->  -.  ( F `  S
)  <_  ( (
( L  -  1 )  -  ( 1  /  3 ) )  x.  E ) ) )
411409, 410mpbird 224 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( L  -  1 )  -  ( 1  /  3
) )  x.  E
)  <  ( F `  S ) )
412323, 326, 324, 366, 411lttrd 9187 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  <  ( F `  S ) )
413323, 324, 412ltled 9177 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  S ) )
414413adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( ( L  - 
2 )  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  S ) )
415302, 307, 312, 320, 414letrd 9183 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  S ) )
416 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ t
( ( i  +  ( 1  /  3
) )  x.  E
)
417416, 49, 48nfbr 4216 . . . . . . . . . . . . 13  |-  F/ t ( ( i  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  S )
41852breq2d 4184 . . . . . . . . . . . . 13  |-  ( t  =  S  ->  (
( ( i  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  S
) ) )
41945, 46, 417, 418elrabf 3051 . . . . . . . . . . . 12  |-  ( S  e.  { t  e.  T  |  ( ( i  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) }  <->  ( S  e.  T  /\  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  S ) ) )
420295, 415, 419sylanbrc 646 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
421 rabexg 4313 . . . . . . . . . . . . . 14  |-  ( T  e.  _V  ->  { t  e.  T  |  ( ( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
42234, 421syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
423422adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  { t  e.  T  |  ( ( i  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
424 oveq1 6047 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  (
j  +  ( 1  /  3 ) )  =  ( i  +  ( 1  /  3
) ) )
425424oveq1d 6055 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  =  ( ( i  +  ( 1  / 
3 ) )  x.  E ) )
426425breq1d 4182 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) ) )
427426rabbidv 2908 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  =  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
428 stoweidlem26.5 . . . . . . . . . . . . 13  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
429427, 428fvmptg 5763 . . . . . . . . . . . 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 ) } )
430158, 423, 429syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( B `  i )  =  { t  e.  T  |  ( ( i  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
431420, 430eleqtrrd 2481 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  ( B `  i
) )
4321533ad2ant1 978 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  (
( L  -  2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2 )  <_  N ) )
433432, 154sylibr 204 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  N  e.  ( ZZ>= `  ( L  -  2 ) ) )
434433, 156syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  (
0 ... ( L  - 
2 ) )  C_  ( 0 ... N
) )
435 simp2 958 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  i  e.  ( 0 ... ( L  -  2 ) ) )
436434, 435sseldd 3309 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  i  e.  ( 0 ... N
) )
437 elex 2924 . . . . . . . . . . . . 13  |-  ( S  e.  ( B `  i )  ->  S  e.  _V )
4384373ad2ant3 980 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )  ->  S  e.  _V )
439 nfcv 2540 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t
( 0 ... N
)
440 nfrab1 2848 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
441439, 440nfmpt 4257 . . . . . . . . . . . . . . . . . 18  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
442428, 441nfcxfr 2537 . . . . . . . . . . . . . . . . 17  |-  F/_ t B
443 nfcv 2540 . . . . . . . . . . . . . . . . 17  |-  F/_ t
i
444442, 443nffv 5694 . . . . . . . . . . . . . . . 16  |-  F/_ t
( B `  i
)
445444nfel2 2552 . . . . . . . . . . . . . . 15  |-  F/ t  S  e.  ( B `
 i )
44695, 96, 445nf3an 1845 . . . . . . . . . . . . . 14  |-  F/ t ( ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )
447 nfv 1626 . . . . . . . . . . . . . 14  |-  F/ t ( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S )
448446, 447nfim 1828 . . . . . . . . . . . . 13  |-  F/ t ( ( ph  /\  i  e.  ( 0 ... N )  /\  S  e.  ( B `  i ) )  -> 
( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S ) )
449 eleq1 2464 . . . . . . . . . . . . . . 15  |-  ( t  =  S  ->  (
t  e.  ( B `
 i )  <->  S  e.  ( B `  i ) ) )
4504493anbi3d 1260 . . . . . . . . . . . . . 14  |-  ( t  =  S  ->  (
( ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  ( B `  i ) )  <->  ( ph  /\  i  e.  ( 0 ... N )  /\  S  e.  ( B `  i ) ) ) )
451100breq2d 4184 . . . . . . . . . . . . . 14  |-  ( t  =  S  ->  (
( 1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) ) )
452450, 451imbi12d 312 . . . . . . . . . . . . 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
) ) ) )
453 stoweidlem26.15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  t
) )
45445, 448, 452, 453vtoclgf 2970 . . . . . . . . . . . 12  |-  ( S  e.  _V  ->  (
( ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) ) )
455438, 454mpcom 34 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  S  e.  ( B `  i ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) )
456436, 455syld3an2 1231 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) )  /\  S  e.  ( B `  i
) )  ->  (
1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S ) )
457431, 456mpd3an3 1280 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
1  -  ( E  /  N ) )  <  ( ( X `
 i ) `  S ) )
458457adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  i ) `  S
) )
459288, 290, 291, 294, 458fsumlt 12534 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  <  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `  i ) `  S
) )
460287, 459eqbrtrrd 4194 . . . . . 6  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  <  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `
 i ) `  S ) )
461128adantr 452 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  e.  RR )
462160adantr 452 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )  e.  RR )
463316adantr 452 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  e.  RR  /\  0  <  E ) )
464 ltmul2 9817 . . . . . . 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 )
) ) )
465461, 462, 463, 464syl3anc 1184 . . . . . 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 )
) ) )
466460, 465mpbid 202 . . . . 5  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  <  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
) )
467122, 130, 162, 236, 466lttrd 9187 . . . 4  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( ( X `  i ) `  S
) ) )
468158, 59syldan 457 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
469468adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
470469recnd 9070 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  CC )
471288, 470fsumcl 12482 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  CC )
472471addid1d 9222 . . . . . 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 )
) )
47317a1i 11 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  e.  RR )
474 fzfid 11267 . . . . . . . 8  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  - 
1 ) ... N
)  e.  Fin )
47514adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  E  e.  RR )
47617a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  e.  RR )
477127adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( L  -  1 )  e.  RR )
478 elfzelz 11015 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( ( L  -  1 ) ... N )  ->  i  e.  ZZ )
479478zred 10331 . . . . . . . . . . . . . 14  |-  ( i  e.  ( ( L  -  1 ) ... N )  ->  i  e.  RR )
480479adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  RR )
481 1m1e0 10024 . . . . . . . . . . . . . . 15  |-  ( 1  -  1 )  =  0
482123, 115, 123, 368lesub1dd 9598 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  -  1 )  <_  ( L  -  1 ) )
483481, 482syl5eqbrr 4206 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <_  ( L  -  1 ) )
484483adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  ( L  -  1 ) )
485 simpr 448 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  ( ( L  - 
1 ) ... N
) )
486478adantl 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  ZZ )
487382adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( L  -  1 )  e.  ZZ )
488136adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  N  e.  ZZ )
489 elfz 11005 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ZZ  /\  ( L  -  1
)  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  e.  ( ( L  -  1 ) ... N )  <-> 
( ( L  - 
1 )  <_  i  /\  i  <_  N ) ) )
490486, 487, 488, 489syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
i  e.  ( ( L  -  1 ) ... N )  <->  ( ( L  -  1 )  <_  i  /\  i  <_  N ) ) )
491485, 490mpbid 202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
( L  -  1 )  <_  i  /\  i  <_  N ) )
492491simpld 446 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( L  -  1 )  <_  i )
493476, 477, 480, 484, 492letrd 9183 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  i )
494 elfzle2 11017 . . . . . . . . . . . . 13  |-  ( i  e.  ( ( L  -  1 ) ... N )  ->  i  <_  N )
495494adantl 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  <_  N )
49628a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  e.  ZZ )
497 elfz 11005 . . . . . . . . . . . . 13  |-  ( ( i  e.  ZZ  /\  0  e.  ZZ  /\  N  e.  ZZ )  ->  (
i  e.  ( 0 ... N )  <->  ( 0  <_  i  /\  i  <_  N ) ) )
498486, 496, 488, 497syl3anc 1184 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
i  e.  ( 0 ... N )  <->  ( 0  <_  i  /\  i  <_  N ) ) )
499493, 495, 498mpbir2and 889 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  i  e.  ( 0 ... N
) )
500499, 58syldan 457 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
( X `  i
) `  S )  e.  RR )
501475, 500remulcld 9072 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
502501adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( ( L  -  1 ) ... N ) )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
503474, 502fsumrecl 12483 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( ( L  -  1 ) ... N ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  RR )
504288, 469fsumrecl 12483 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  RR )
505 fzfid 11267 . . . . . . . . 9  |-  ( ph  ->  ( ( L  - 
1 ) ... N
)  e.  Fin )
506184adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  E  e.  CC )
507506mul01d 9221 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  x.  0 )  =  0 )
508499, 107syldan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) )
509316adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  e.  RR  /\  0  <  E ) )
510 lemul2 9819 . . . . . . . . . . . 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 ) ) ) )
511476, 500, 509, 510syl3anc 1184 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  (
0  <_  ( ( X `  i ) `  S )  <->  ( E  x.  0 )  <_  ( E  x.  ( ( X `  i ) `  S ) ) ) )
512508, 511mpbid 202 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  ( E  x.  0 )  <_  ( E  x.  ( ( X `  i ) `  S
) ) )
513507, 512eqbrtrrd 4194 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( L  - 
1 ) ... N
) )  ->  0  <_  ( E  x.  (
( X `  i
) `  S )
) )
514505, 501, 513fsumge0 12529 . . . . . . . 8  |-  ( ph  ->  0  <_  sum_ i  e.  ( ( L  - 
1 ) ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
515514adantr 452 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  <_  sum_ i  e.  ( ( L  - 
1 ) ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
516473, 503, 504, 515leadd2dd 9597 . . . . . 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 ) ) ) )
517472, 516eqbrtrrd 4194 . . . . 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 ) ) ) )
518159recnd 9070 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( X `  i
) `  S )  e.  CC )
519131, 184, 518fsummulc2 12522 . . . . . 6  |-  ( ph  ->  ( E  x.  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( ( X `  i
) `  S )
)  =  sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( E  x.  ( ( X `  i ) `  S
) ) )
520519adantr 452 . . . . 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
) ) )
521 stoweidlem26.2 . . . . . . . . 9  |-  F/ j
ph
522 elfzelz 11015 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( L  -  2 ) )  ->  j  e.  ZZ )
523522adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  e.  ZZ )
524523zred 10331 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  e.  RR )
525321adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  RR )
526127adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  1 )  e.  RR )
527 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  e.  ( 0 ... ( L  -  2 ) ) )
52828a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  0  e.  ZZ )
529135adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  ZZ )
530 elfz 11005 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ )  -> 
( j  e.  ( 0 ... ( L  -  2 ) )  <-> 
( 0  <_  j  /\  j  <_  ( L  -  2 ) ) ) )
531523, 528, 529, 530syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
j  e.  ( 0 ... ( L  - 
2 ) )  <->  ( 0  <_  j  /\  j  <_  ( L  -  2 ) ) ) )
532527, 531mpbid 202 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
0  <_  j  /\  j  <_  ( L  - 
2 ) ) )
533532simprd 450 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  <_  ( L  -  2 ) )
534123, 139, 115ltsub2d 9592 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  <  2  <->  ( L  -  2 )  <  ( L  - 
1 ) ) )
535358, 534mpbii 203 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  2 )  <  ( L  -  1 ) )
536535adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  <  ( L  - 
1 ) )
537524, 525, 526, 533, 536lelttrd 9184 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->  j  <  ( L  -  1 ) )
538524, 526ltnled 9176 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... ( L  -  2 ) ) )  ->