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

Theorem stoweidlem26 27877
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
Dummy variable  A is distinct from all other variables.
StepHypRef Expression
1 1re 8853 . . . . . . . . . . . . 13  |-  1  e.  RR
21a1i 10 . . . . . . . . . . . 12  |-  ( L  =  1  ->  1  e.  RR )
3 eleq1 2356 . . . . . . . . . . . 12  |-  ( L  =  1  ->  ( L  e.  RR  <->  1  e.  RR ) )
42, 3mpbird 223 . . . . . . . . . . 11  |-  ( L  =  1  ->  L  e.  RR )
54adantl 452 . . . . . . . . . 10  |-  ( (
ph  /\  L  = 
1 )  ->  L  e.  RR )
6 4re 9835 . . . . . . . . . . . . 13  |-  4  e.  RR
7 3re 9833 . . . . . . . . . . . . 13  |-  3  e.  RR
8 3ne0 9847 . . . . . . . . . . . . 13  |-  3  =/=  0
96, 7, 83pm3.2i 1130 . . . . . . . . . . . 12  |-  ( 4  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
10 redivcl 9495 . . . . . . . . . . . 12  |-  ( ( 4  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
4  /  3 )  e.  RR )
119, 10ax-mp 8 . . . . . . . . . . 11  |-  ( 4  /  3 )  e.  RR
1211a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  /  3 )  e.  RR )
135, 12jca 518 . . . . . . . . 9  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  e.  RR  /\  (
4  /  3 )  e.  RR ) )
14 resubcl 9127 . . . . . . . . 9  |-  ( ( L  e.  RR  /\  ( 4  /  3
)  e.  RR )  ->  ( L  -  ( 4  /  3
) )  e.  RR )
1513, 14syl 15 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  e.  RR )
16 3cn 9834 . . . . . . . . . . . . . . 15  |-  3  e.  CC
1716, 8pm3.2i 441 . . . . . . . . . . . . . 14  |-  ( 3  e.  CC  /\  3  =/=  0 )
18 divid 9467 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  CC  /\  3  =/=  0 )  -> 
( 3  /  3
)  =  1 )
1917, 18ax-mp 8 . . . . . . . . . . . . 13  |-  ( 3  /  3 )  =  1
20 3lt4 9905 . . . . . . . . . . . . . 14  |-  3  <  4
21 3pos 9846 . . . . . . . . . . . . . . . . 17  |-  0  <  3
227, 21pm3.2i 441 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  RR  /\  0  <  3 )
237, 6, 223pm3.2i 1130 . . . . . . . . . . . . . . 15  |-  ( 3  e.  RR  /\  4  e.  RR  /\  ( 3  e.  RR  /\  0  <  3 ) )
24 ltdiv1 9636 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  RR  /\  4  e.  RR  /\  (
3  e.  RR  /\  0  <  3 ) )  ->  ( 3  <  4  <->  ( 3  / 
3 )  <  (
4  /  3 ) ) )
2523, 24ax-mp 8 . . . . . . . . . . . . . 14  |-  ( 3  <  4  <->  ( 3  /  3 )  < 
( 4  /  3
) )
2620, 25mpbi 199 . . . . . . . . . . . . 13  |-  ( 3  /  3 )  < 
( 4  /  3
)
2719, 26eqbrtrri 4060 . . . . . . . . . . . 12  |-  1  <  ( 4  /  3
)
2827a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  L  = 
1 )  ->  1  <  ( 4  /  3
) )
29 breq1 4042 . . . . . . . . . . . 12  |-  ( L  =  1  ->  ( L  <  ( 4  / 
3 )  <->  1  <  ( 4  /  3 ) ) )
3029adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  <  ( 4  / 
3 )  <->  1  <  ( 4  /  3 ) ) )
3128, 30mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  L  = 
1 )  ->  L  <  ( 4  /  3
) )
32 recn 8843 . . . . . . . . . . . . 13  |-  ( L  e.  RR  ->  L  e.  CC )
335, 32syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  L  = 
1 )  ->  L  e.  CC )
34 subid1 9084 . . . . . . . . . . . 12  |-  ( L  e.  CC  ->  ( L  -  0 )  =  L )
3533, 34syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  0 )  =  L )
3635breq1d 4049 . . . . . . . . . 10  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  0 )  <  ( 4  /  3 )  <->  L  <  ( 4  /  3 ) ) )
3731, 36mpbird 223 . . . . . . . . 9  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  0 )  <  ( 4  / 
3 ) )
38 0re 8854 . . . . . . . . . . . 12  |-  0  e.  RR
3938a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  L  = 
1 )  ->  0  e.  RR )
405, 12, 393jca 1132 . . . . . . . . . 10  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  e.  RR  /\  (
4  /  3 )  e.  RR  /\  0  e.  RR ) )
41 ltsub23 9270 . . . . . . . . . 10  |-  ( ( L  e.  RR  /\  ( 4  /  3
)  e.  RR  /\  0  e.  RR )  ->  ( ( L  -  ( 4  /  3
) )  <  0  <->  ( L  -  0 )  <  ( 4  / 
3 ) ) )
4240, 41syl 15 . . . . . . . . 9  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  <  0  <->  ( L  -  0 )  <  ( 4  / 
3 ) ) )
4337, 42mpbird 223 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  <  0 )
4415, 43jca 518 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  e.  RR  /\  ( L  -  (
4  /  3 ) )  <  0 ) )
45 stoweidlem26.11 . . . . . . . . . 10  |-  ( ph  ->  E  e.  RR+ )
46 rpre 10376 . . . . . . . . . 10  |-  ( E  e.  RR+  ->  E  e.  RR )
4745, 46syl 15 . . . . . . . . 9  |-  ( ph  ->  E  e.  RR )
4847adantr 451 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  E  e.  RR )
49 rpgt0 10381 . . . . . . . . . 10  |-  ( E  e.  RR+  ->  0  < 
E )
5045, 49syl 15 . . . . . . . . 9  |-  ( ph  ->  0  <  E )
5150adantr 451 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  0  <  E )
5248, 51jca 518 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  ( E  e.  RR  /\  0  <  E ) )
5344, 52jca 518 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  (
( ( L  -  ( 4  /  3
) )  e.  RR  /\  ( L  -  (
4  /  3 ) )  <  0 )  /\  ( E  e.  RR  /\  0  < 
E ) ) )
54 mulltgt0 27795 . . . . . 6  |-  ( ( ( ( L  -  ( 4  /  3
) )  e.  RR  /\  ( L  -  (
4  /  3 ) )  <  0 )  /\  ( E  e.  RR  /\  0  < 
E ) )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  0 )
5553, 54syl 15 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  0 )
56 fzfi 11050 . . . . . . . . 9  |-  ( 0 ... N )  e. 
Fin
5756a1i 10 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
5838a1i 10 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  e.  RR )
5947adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  E  e.  RR )
60 stoweidlem26.13 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
61 stoweidlem26.9 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  S  e.  ( ( D `  L ) 
\  ( D `  ( L  -  1
) ) ) )
62 eldif 3175 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  ( ( D `
 L )  \ 
( D `  ( L  -  1 ) ) )  <->  ( S  e.  ( D `  L
)  /\  -.  S  e.  ( D `  ( L  -  1 ) ) ) )
6361, 62sylib 188 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  e.  ( D `  L )  /\  -.  S  e.  ( D `  ( L  -  1 ) ) ) )
6463simpld 445 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  S  e.  ( D `
 L ) )
65 stoweidlem26.8 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  L  e.  ( 1 ... N ) )
66 1e0p1 10168 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =  ( 0  +  1 )
6766oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1 ... N )  =  ( ( 0  +  1 ) ... N
)
68 0z 10051 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  ZZ
69 fzp1ss 10853 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  e.  ZZ  ->  (
( 0  +  1 ) ... N ) 
C_  ( 0 ... N ) )
7068, 69ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  +  1 ) ... N )  C_  ( 0 ... N
)
7167, 70eqsstri 3221 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1 ... N )  C_  ( 0 ... N
)
7271a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 1 ... N
)  C_  ( 0 ... N ) )
7372sselda 3193 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  L  e.  ( 1 ... N
) )  ->  L  e.  ( 0 ... N
) )
7465, 73mpdan 649 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  L  e.  ( 0 ... N ) )
75 stoweidlem26.7 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  e.  _V )
7675idi 2 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  _V )
77 rabexg 4180 . . . . . . . . . . . . . . . . . . . 20  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
7876, 77syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
7974, 78jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  ( 0 ... N )  /\  { t  e.  T  |  ( F `
 t )  <_ 
( ( L  -  ( 1  /  3
) )  x.  E
) }  e.  _V ) )
80 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j L
81 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) }
82 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  L  ->  (
j  -  ( 1  /  3 ) )  =  ( L  -  ( 1  /  3
) ) )
8382oveq1d 5889 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  L  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( L  -  ( 1  / 
3 ) )  x.  E ) )
8483breq2d 4051 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  L  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) ) )
8584rabbidv 2793 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  L  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) } )
86 stoweidlem26.4 . . . . . . . . . . . . . . . . . . 19  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
8780, 81, 85, 86fvmptf 5632 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) } )
8879, 87syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  L
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
8988eleq2d 2363 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  e.  ( D `  L )  <-> 
S  e.  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } ) )
9064, 89mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ph  ->  S  e.  { t  e.  T  |  ( F `  t )  <_  ( ( L  -  ( 1  / 
3 ) )  x.  E ) } )
91 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ t S
92 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ t T
93 stoweidlem26.1 . . . . . . . . . . . . . . . . . 18  |-  F/_ t F
9493, 91nffv 5548 . . . . . . . . . . . . . . . . 17  |-  F/_ t
( F `  S
)
95 nfcv 2432 . . . . . . . . . . . . . . . . 17  |-  F/_ t  <_
96 nfcv 2432 . . . . . . . . . . . . . . . . 17  |-  F/_ t
( ( L  -  ( 1  /  3
) )  x.  E
)
9794, 95, 96nfbr 4083 . . . . . . . . . . . . . . . 16  |-  F/ t ( F `  S
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E )
98 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( t  =  S  ->  ( F `  t )  =  ( F `  S ) )
9998breq1d 4049 . . . . . . . . . . . . . . . 16  |-  ( t  =  S  ->  (
( F `  t
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  S )  <_  (
( L  -  (
1  /  3 ) )  x.  E ) ) )
10091, 92, 97, 99elrabf 2935 . . . . . . . . . . . . . . 15  |-  ( S  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( L  -  ( 1  /  3
) )  x.  E
) }  <->  ( S  e.  T  /\  ( F `  S )  <_  ( ( L  -  ( 1  /  3
) )  x.  E
) ) )
10190, 100sylib 188 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S  e.  T  /\  ( F `  S
)  <_  ( ( L  -  ( 1  /  3 ) )  x.  E ) ) )
102101simpld 445 . . . . . . . . . . . . 13  |-  ( ph  ->  S  e.  T )
103102adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  S  e.  T )
10460, 103jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) : T --> RR  /\  S  e.  T )
)
105 ffvelrn 5679 . . . . . . . . . . 11  |-  ( ( ( X `  i
) : T --> RR  /\  S  e.  T )  ->  ( ( X `  i ) `  S
)  e.  RR )
106104, 105syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  S )  e.  RR )
10759, 106jca 518 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  e.  RR  /\  (
( X `  i
) `  S )  e.  RR ) )
108 remulcl 8838 . . . . . . . . 9  |-  ( ( E  e.  RR  /\  ( ( X `  i ) `  S
)  e.  RR )  ->  ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
109107, 108syl 15 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  x.  ( ( X `  i ) `  S ) )  e.  RR )
11038a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  RR )
111110, 47jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  e.  RR  /\  E  e.  RR ) )
112 ltle 8926 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  E  e.  RR )  ->  ( 0  <  E  ->  0  <_  E )
)
113111, 112syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  <  E  ->  0  <_  E )
)
11450, 113mpd 14 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  E )
115114adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  E )
11659, 115jca 518 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  e.  RR  /\  0  <_  E ) )
117 stoweidlem26.3 . . . . . . . . . . . . . . . 16  |-  F/ t
ph
118 nfv 1609 . . . . . . . . . . . . . . . 16  |-  F/ t  i  e.  ( 0 ... N )
119117, 118nfan 1783 . . . . . . . . . . . . . . 15  |-  F/ t ( ph  /\  i  e.  ( 0 ... N
) )
120 nfv 1609 . . . . . . . . . . . . . . 15  |-  F/ t 0  <_  ( ( X `  i ) `  S )
121119, 120nfim 1781 . . . . . . . . . . . . . 14  |-  F/ t ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  S )
)
122 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( t  =  S  ->  (
( X `  i
) `  t )  =  ( ( X `
 i ) `  S ) )
123122breq2d 4051 . . . . . . . . . . . . . . 15  |-  ( t  =  S  ->  (
0  <_  ( ( X `  i ) `  t )  <->  0  <_  ( ( X `  i
) `  S )
) )
124123imbi2d 307 . . . . . . . . . . . . . 14  |-  ( t  =  S  ->  (
( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  t )
)  <->  ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  0  <_  (
( X `  i
) `  S )
) ) )
125 stoweidlem26.14 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )  ->  0  <_  ( ( X `  i ) `  t
) )
1261253expia 1153 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
t  e.  T  -> 
0  <_  ( ( X `  i ) `  t ) ) )
127126com12 27 . . . . . . . . . . . . . . 15  |-  ( t  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  t
) ) )
128127idi 2 . . . . . . . . . . . . . 14  |-  ( t  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  t
) ) )
12991, 121, 124, 128vtoclgaf 2861 . . . . . . . . . . . . 13  |-  ( S  e.  T  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) ) )
130103, 129syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) ) )
131130pm2.43i 43 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( ( X `  i ) `  S
) )
132106, 131jca 518 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( ( X `  i ) `  S
)  e.  RR  /\  0  <_  ( ( X `
 i ) `  S ) ) )
133116, 132jca 518 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( E  e.  RR  /\  0  <_  E )  /\  ( ( ( X `
 i ) `  S )  e.  RR  /\  0  <_  ( ( X `  i ) `  S ) ) ) )
134 mulge0 9307 . . . . . . . . 9  |-  ( ( ( E  e.  RR  /\  0  <_  E )  /\  ( ( ( X `
 i ) `  S )  e.  RR  /\  0  <_  ( ( X `  i ) `  S ) ) )  ->  0  <_  ( E  x.  ( ( X `  i ) `  S ) ) )
135133, 134syl 15 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  0  <_  ( E  x.  (
( X `  i
) `  S )
) )
13657, 58, 109, 135fsumle 12273 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
137136adantr 451 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) 0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )
138 0cn 8847 . . . . . . . . . . . 12  |-  0  e.  CC
139138a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  CC )
14057, 139jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0 ... N )  e.  Fin  /\  0  e.  CC ) )
141 fsumconst 12268 . . . . . . . . . 10  |-  ( ( ( 0 ... N
)  e.  Fin  /\  0  e.  CC )  -> 
sum_ i  e.  ( 0 ... N ) 0  =  ( (
# `  ( 0 ... N ) )  x.  0 ) )
142140, 141syl 15 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  =  ( (
# `  ( 0 ... N ) )  x.  0 ) )
143 hashcl 11366 . . . . . . . . . . 11  |-  ( ( 0 ... N )  e.  Fin  ->  ( # `
 ( 0 ... N ) )  e. 
NN0 )
144 nn0cn 9991 . . . . . . . . . . 11  |-  ( (
# `  ( 0 ... N ) )  e. 
NN0  ->  ( # `  (
0 ... N ) )  e.  CC )
14557, 143, 1443syl 18 . . . . . . . . . 10  |-  ( ph  ->  ( # `  (
0 ... N ) )  e.  CC )
146 mul01 9007 . . . . . . . . . 10  |-  ( (
# `  ( 0 ... N ) )  e.  CC  ->  ( ( # `
 ( 0 ... N ) )  x.  0 )  =  0 )
147145, 146syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  x.  0 )  =  0 )
148142, 147eqtrd 2328 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) 0  =  0 )
149148adantr 451 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) 0  =  0 )
150149breq1d 4049 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  ( sum_ i  e.  ( 0 ... N ) 0  <_  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
)  <->  0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) ) )
151137, 150mpbid 201 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  0  <_ 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) )
15255, 151jca 518 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  (
( ( L  -  ( 4  /  3
) )  x.  E
)  <  0  /\  0  <_  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) ) )
1536a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  L  = 
1 )  ->  4  e.  RR )
1547a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  L  = 
1 )  ->  3  e.  RR )
1558a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  L  = 
1 )  ->  3  =/=  0 )
156153, 154, 1553jca 1132 . . . . . . . . . . 11  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  e.  RR  /\  3  e.  RR  /\  3  =/=  0 ) )
157156, 10syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  L  = 
1 )  ->  (
4  /  3 )  e.  RR )
1585, 157jca 518 . . . . . . . . 9  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  e.  RR  /\  (
4  /  3 )  e.  RR ) )
159158, 14syl 15 . . . . . . . 8  |-  ( (
ph  /\  L  = 
1 )  ->  ( L  -  ( 4  /  3 ) )  e.  RR )
160159, 48jca 518 . . . . . . 7  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  e.  RR  /\  E  e.  RR )
)
161 remulcl 8838 . . . . . . 7  |-  ( ( ( L  -  (
4  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR )
162160, 161syl 15 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  e.  RR )
163 fzfid 11051 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
164163, 109fsumrecl 12223 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
)  e.  RR )
165164adantr 451 . . . . . 6  |-  ( (
ph  /\  L  = 
1 )  ->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) )  e.  RR )
166162, 39, 1653jca 1132 . . . . 5  |-  ( (
ph  /\  L  = 
1 )  ->  (
( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR  /\  0  e.  RR  /\  sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  RR ) )
167 ltletr 8929 . . . . 5  |-  ( ( ( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR  /\  0  e.  RR  /\  sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 S ) )  e.  RR )  -> 
( ( ( ( L  -  ( 4  /  3 ) )  x.  E )  <  0  /\  0  <_  sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 S ) ) )  ->  ( ( L  -  ( 4  /  3 ) )  x.  E )  <  sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 S ) ) ) )
168166, 167syl 15 . . . 4  |-  ( (
ph  /\  L  = 
1 )  ->  (
( ( ( L  -  ( 4  / 
3 ) )  x.  E )  <  0  /\  0  <_  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  S
) ) ) )
169152, 168mpd 14 . . 3  |-  ( (
ph  /\  L  = 
1 )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  S )
) )
170 stoweidlem26.12 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E  <  ( 1  /  3 ) )
1711, 7, 83pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
172 redivcl 9495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  RR )
173171, 172ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  3 )  e.  RR
174173a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
1751a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  1  e.  RR )
17647, 174, 1753jca 1132 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E  e.  RR  /\  ( 1  /  3
)  e.  RR  /\  1  e.  RR )
)
177 ltadd2 8940 . . . . . . . . . . . . . . . . . 18  |-  ( ( E  e.  RR  /\  ( 1  /  3
)  e.  RR  /\  1  e.  RR )  ->  ( E  <  (
1  /  3 )  <-> 
( 1  +  E
)  <  ( 1  +  ( 1  / 
3 ) ) ) )
178176, 177syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E  <  (
1  /  3 )  <-> 
( 1  +  E
)  <  ( 1  +  ( 1  / 
3 ) ) ) )
179170, 178mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  +  E
)  <  ( 1  +  ( 1  / 
3 ) ) )
180 ax-1cn 8811 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
18116, 180, 173pm3.2i 1130 . . . . . . . . . . . . . . . . . 18  |-  ( 3  e.  CC  /\  1  e.  CC  /\  ( 3  e.  CC  /\  3  =/=  0 ) )
182 divdir 9463 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  e.  CC  /\  1  e.  CC  /\  (
3  e.  CC  /\  3  =/=  0 ) )  ->  ( ( 3  +  1 )  / 
3 )  =  ( ( 3  /  3
)  +  ( 1  /  3 ) ) )
183181, 182ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  +  1 )  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
184 3p1e4 9864 . . . . . . . . . . . . . . . . . 18  |-  ( 3  +  1 )  =  4
185184oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  +  1 )  /  3 )  =  ( 4  /  3
)
18619oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  /  3 )  +  ( 1  / 
3 ) )  =  ( 1  +  ( 1  /  3 ) )
187183, 185, 1863eqtr3ri 2325 . . . . . . . . . . . . . . . 16  |-  ( 1  +  ( 1  / 
3 ) )  =  ( 4  /  3
)
188179, 187syl6breq 4078 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  +  E
)  <  ( 4  /  3 ) )
189175, 47jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  e.  RR  /\  E  e.  RR ) )
190 readdcl 8836 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  RR  /\  E  e.  RR )  ->  ( 1  +  E
)  e.  RR )
191189, 190syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1  +  E
)  e.  RR )
1926a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  4  e.  RR )
1937a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  3  e.  RR )
1948a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  3  =/=  0 )
195192, 193, 1943jca 1132 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 4  e.  RR  /\  3  e.  RR  /\  3  =/=  0 ) )
196195, 10syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 4  /  3
)  e.  RR )
197 elfzelz 10814 . . . . . . . . . . . . . . . . . 18  |-  ( L  e.  ( 1 ... N )  ->  L  e.  ZZ )
198 zre 10044 . . . . . . . . . . . . . . . . . 18  |-  ( L  e.  ZZ  ->  L  e.  RR )
19965, 197, 1983syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  L  e.  RR )
200191, 196, 1993jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1  +  E )  e.  RR  /\  ( 4  /  3
)  e.  RR  /\  L  e.  RR )
)
201 ltsub2 9287 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  +  E
)  e.  RR  /\  ( 4  /  3
)  e.  RR  /\  L  e.  RR )  ->  ( ( 1  +  E )  <  (
4  /  3 )  <-> 
( L  -  (
4  /  3 ) )  <  ( L  -  ( 1  +  E ) ) ) )
202200, 201syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1  +  E )  <  (
4  /  3 )  <-> 
( L  -  (
4  /  3 ) )  <  ( L  -  ( 1  +  E ) ) ) )
203188, 202mpbid 201 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  <  ( L  -  ( 1  +  E ) ) )
20465, 197syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  L  e.  ZZ )
205 zcn 10045 . . . . . . . . . . . . . . . . 17  |-  ( L  e.  ZZ  ->  L  e.  CC )
206204, 205syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  L  e.  CC )
207180a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  CC )
208 recn 8843 . . . . . . . . . . . . . . . . 17  |-  ( E  e.  RR  ->  E  e.  CC )
20947, 208syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  CC )
210206, 207, 2093jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  e.  CC  /\  1  e.  CC  /\  E  e.  CC )
)
211 subsub4 9096 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  CC  /\  1  e.  CC  /\  E  e.  CC )  ->  (
( L  -  1 )  -  E )  =  ( L  -  ( 1  +  E
) ) )
212210, 211syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  =  ( L  -  ( 1  +  E ) ) )
213203, 212breqtrrd 4065 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  <  ( ( L  -  1 )  -  E ) )
214199, 196jca 518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( L  e.  RR  /\  ( 4  /  3
)  e.  RR ) )
215214, 14syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  -  (
4  /  3 ) )  e.  RR )
216199, 175jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  RR  /\  1  e.  RR ) )
217 resubcl 9127 . . . . . . . . . . . . . . . . . 18  |-  ( ( L  e.  RR  /\  1  e.  RR )  ->  ( L  -  1 )  e.  RR )
218216, 217syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  1 )  e.  RR )
219218, 47jca 518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
1 )  e.  RR  /\  E  e.  RR ) )
220 resubcl 9127 . . . . . . . . . . . . . . . 16  |-  ( ( ( L  -  1 )  e.  RR  /\  E  e.  RR )  ->  ( ( L  - 
1 )  -  E
)  e.  RR )
221219, 220syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  e.  RR )
22247, 50jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
223215, 221, 2223jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  e.  RR  /\  ( ( L  - 
1 )  -  E
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
224 ltmul1 9622 . . . . . . . . . . . . . 14  |-  ( ( ( L  -  (
4  /  3 ) )  e.  RR  /\  ( ( L  - 
1 )  -  E
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( ( L  -  ( 4  /  3 ) )  <  ( ( L  -  1 )  -  E )  <->  ( ( L  -  ( 4  /  3 ) )  x.  E )  < 
( ( ( L  -  1 )  -  E )  x.  E
) ) )
225223, 224syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  <  (
( L  -  1 )  -  E )  <-> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( (
( L  -  1 )  -  E )  x.  E ) ) )
226213, 225mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( (
( L  -  1 )  -  E )  x.  E ) )
227206, 207jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  CC  /\  1  e.  CC ) )
228 subcl 9067 . . . . . . . . . . . . . . . . . 18  |-  ( ( L  e.  CC  /\  1  e.  CC )  ->  ( L  -  1 )  e.  CC )
229227, 228syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  1 )  e.  CC )
230229, 209jca 518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
1 )  e.  CC  /\  E  e.  CC ) )
231 subcl 9067 . . . . . . . . . . . . . . . 16  |-  ( ( ( L  -  1 )  e.  CC  /\  E  e.  CC )  ->  ( ( L  - 
1 )  -  E
)  e.  CC )
232230, 231syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  - 
1 )  -  E
)  e.  CC )
233209, 232jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  e.  CC  /\  ( ( L  - 
1 )  -  E
)  e.  CC ) )
234 mulcom 8839 . . . . . . . . . . . . . 14  |-  ( ( E  e.  CC  /\  ( ( L  - 
1 )  -  E
)  e.  CC )  ->  ( E  x.  ( ( L  - 
1 )  -  E
) )  =  ( ( ( L  - 
1 )  -  E
)  x.  E ) )
235233, 234syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( ( L  -  1 )  -  E )  x.  E ) )
236209, 229, 2093jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  e.  CC  /\  ( L  -  1 )  e.  CC  /\  E  e.  CC )
)
237 subdi 9229 . . . . . . . . . . . . . 14  |-  ( ( E  e.  CC  /\  ( L  -  1
)  e.  CC  /\  E  e.  CC )  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
238236, 237syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  E ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
239235, 238eqtr3d 2330 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( L  -  1 )  -  E )  x.  E
)  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
240226, 239breqtrd 4063 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) ) )
241 1z 10069 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  ZZ
242241a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  ZZ )
243 stoweidlem26.6 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  N  e.  NN )
244 nnz 10061 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN  ->  N  e.  ZZ )
245243, 244syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  ZZ )
246204, 242, 2453jca 1132 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )
)
247 elfz 10804 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )  ->  ( L  e.  ( 1 ... N )  <->  ( 1  <_  L  /\  L  <_  N ) ) )
248246, 247syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( L  e.  ( 1 ... N )  <-> 
( 1  <_  L  /\  L  <_  N ) ) )
24965, 248mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  <_  L  /\  L  <_  N ) )
250249simprd 449 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  L  <_  N )
251204, 245jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  ZZ  /\  N  e.  ZZ ) )
252 zlem1lt 10085 . . . . . . . . . . . . . . . . . 18  |-  ( ( L  e.  ZZ  /\  N  e.  ZZ )  ->  ( L  <_  N  <->  ( L  -  1 )  <  N ) )
253251, 252syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  <_  N  <->  ( L  -  1 )  <  N ) )
254250, 253mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( L  -  1 )  <  N )
255 nnre 9769 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  ->  N  e.  RR )
256243, 255syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  RR )
257 nngt0 9791 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  ->  0  <  N )
258243, 257syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  N )
259256, 258jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N  e.  RR  /\  0  <  N ) )
260218, 256, 2593jca 1132 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( L  - 
1 )  e.  RR  /\  N  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) ) )
261 ltdiv1 9636 . . . . . . . . . . . . . . . . 17  |-  ( ( ( L  -  1 )  e.  RR  /\  N  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) )  -> 
( ( L  - 
1 )  <  N  <->  ( ( L  -  1 )  /  N )  <  ( N  /  N ) ) )
262260, 261syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
1 )  <  N  <->  ( ( L  -  1 )  /  N )  <  ( N  /  N ) ) )
263254, 262mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  <  ( N  /  N ) )
264 nncn 9770 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  N  e.  CC )
265243, 264syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  CC )
266 nnne0 9794 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  N  =/=  0 )
267243, 266syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  =/=  0 )
268265, 267jca 518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  e.  CC  /\  N  =/=  0 ) )
269 divid 9467 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  CC  /\  N  =/=  0 )  -> 
( N  /  N
)  =  1 )
270268, 269syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  /  N
)  =  1 )
271263, 270breqtrd 4063 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  <  1 )
272218, 256, 2673jca 1132 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( L  - 
1 )  e.  RR  /\  N  e.  RR  /\  N  =/=  0 ) )
273 redivcl 9495 . . . . . . . . . . . . . . . . 17  |-  ( ( ( L  -  1 )  e.  RR  /\  N  e.  RR  /\  N  =/=  0 )  ->  (
( L  -  1 )  /  N )  e.  RR )
274272, 273syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  e.  RR )
27547, 47jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( E  e.  RR  /\  E  e.  RR ) )
276 remulcl 8838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E  e.  RR  /\  E  e.  RR )  ->  ( E  x.  E
)  e.  RR )
277275, 276syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( E  x.  E
)  e.  RR )
278222, 222jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( E  e.  RR  /\  0  < 
E )  /\  ( E  e.  RR  /\  0  <  E ) ) )
279 mulgt0 8916 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( E  e.  RR  /\  0  <  E )  /\  ( E  e.  RR  /\  0  < 
E ) )  -> 
0  <  ( E  x.  E ) )
280278, 279syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  ( E  x.  E ) )
281277, 280jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( E  x.  E )  e.  RR  /\  0  <  ( E  x.  E ) ) )
282281idi 2 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( E  x.  E )  e.  RR  /\  0  <  ( E  x.  E ) ) )
283282idi 2 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E  x.  E )  e.  RR  /\  0  <  ( E  x.  E ) ) )
284274, 175, 2833jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( L  -  1 )  /  N )  e.  RR  /\  1  e.  RR  /\  ( ( E  x.  E )  e.  RR  /\  0  <  ( E  x.  E ) ) ) )
285 ltmul2 9623 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) )
286284, 285syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( L  -  1 )  /  N )  <  1  <->  ( ( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) )  <  ( ( E  x.  E )  x.  1 ) ) )
287271, 286mpbid 201 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  <  ( ( E  x.  E )  x.  1 ) )
288209, 209jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  e.  CC  /\  E  e.  CC ) )
289 mulcl 8837 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  CC  /\  E  e.  CC )  ->  ( E  x.  E
)  e.  CC )
290288, 289syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  x.  E
)  e.  CC )
291 mulid1 8851 . . . . . . . . . . . . . 14  |-  ( ( E  x.  E )  e.  CC  ->  (
( E  x.  E
)  x.  1 )  =  ( E  x.  E ) )
292290, 291syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  x.  E )  x.  1 )  =  ( E  x.  E ) )
293287, 292breqtrd 4063 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  <  ( E  x.  E ) )
294277, 274jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E  x.  E )  e.  RR  /\  ( ( L  - 
1 )  /  N
)  e.  RR ) )
295 remulcl 8838 . . . . . . . . . . . . . . 15  |-  ( ( ( E  x.  E
)  e.  RR  /\  ( ( L  - 
1 )  /  N
)  e.  RR )  ->  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) )  e.  RR )
296294, 295syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  e.  RR )
29747, 218jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  e.  RR  /\  ( L  -  1 )  e.  RR ) )
298 remulcl 8838 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  RR  /\  ( L  -  1
)  e.  RR )  ->  ( E  x.  ( L  -  1
) )  e.  RR )
299297, 298syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  x.  ( L  -  1 ) )  e.  RR )
300296, 277, 2993jca 1132 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) )  e.  RR  /\  ( E  x.  E
)  e.  RR  /\  ( E  x.  ( L  -  1 ) )  e.  RR ) )
301 ltsub2 9287 . . . . . . . . . . . . 13  |-  ( ( ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  e.  RR  /\  ( E  x.  E
)  e.  RR  /\  ( E  x.  ( L  -  1 ) )  e.  RR )  ->  ( ( ( E  x.  E )  x.  ( ( L  -  1 )  /  N ) )  < 
( E  x.  E
)  <->  ( ( E  x.  ( L  - 
1 ) )  -  ( E  x.  E
) )  <  (
( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  -  1 )  /  N ) ) ) ) )
302300, 301syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) )  <  ( E  x.  E )  <->  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) )  <  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) ) )
303293, 302mpbid 201 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) )
304240, 303jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  -  ( 4  / 
3 ) )  x.  E )  <  (
( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) )  /\  ( ( E  x.  ( L  - 
1 ) )  -  ( E  x.  E
) )  <  (
( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  -  1 )  /  N ) ) ) ) )
305215, 47jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  e.  RR  /\  E  e.  RR ) )
306305, 161syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR )
307299, 277jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  e.  RR  /\  ( E  x.  E
)  e.  RR ) )
308 resubcl 9127 . . . . . . . . . . . . 13  |-  ( ( ( E  x.  ( L  -  1 ) )  e.  RR  /\  ( E  x.  E
)  e.  RR )  ->  ( ( E  x.  ( L  - 
1 ) )  -  ( E  x.  E
) )  e.  RR )
309307, 308syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  e.  RR )
310299, 296jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  e.  RR  /\  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  e.  RR ) )
311 resubcl 9127 . . . . . . . . . . . . 13  |-  ( ( ( E  x.  ( L  -  1 ) )  e.  RR  /\  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  e.  RR )  ->  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) )  e.  RR )
312310, 311syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  (
( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) ) )  e.  RR )
313306, 309, 3123jca 1132 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  -  ( 4  / 
3 ) )  x.  E )  e.  RR  /\  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  e.  RR  /\  ( ( E  x.  ( L  -  1
) )  -  (
( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) ) )  e.  RR ) )
314 lttr 8915 . . . . . . . . . . 11  |-  ( ( ( ( L  -  ( 4  /  3
) )  x.  E
)  e.  RR  /\  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  e.  RR  /\  ( ( E  x.  ( L  -  1
) )  -  (
( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) ) )  e.  RR )  ->  ( ( ( ( L  -  (
4  /  3 ) )  x.  E )  <  ( ( E  x.  ( L  - 
1 ) )  -  ( E  x.  E
) )  /\  (
( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) )  <  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) ) )
315313, 314syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( L  -  ( 4  /  3 ) )  x.  E )  < 
( ( E  x.  ( L  -  1
) )  -  ( E  x.  E )
)  /\  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  E ) )  < 
( ( E  x.  ( L  -  1
) )  -  (
( E  x.  E
)  x.  ( ( L  -  1 )  /  N ) ) ) )  ->  (
( L  -  (
4  /  3 ) )  x.  E )  <  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) ) )
316304, 315mpd 14 . . . . . . . . 9  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( ( E  x.  ( L  -  1 ) )  -  ( ( E  x.  E )  x.  ( ( L  - 
1 )  /  N
) ) ) )
317209, 265, 2673jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  e.  CC  /\  N  e.  CC  /\  N  =/=  0 ) )
318 divcl 9446 . . . . . . . . . . . . . . . 16  |-  ( ( E  e.  CC  /\  N  e.  CC  /\  N  =/=  0 )  ->  ( E  /  N )  e.  CC )
319317, 318syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  /  N
)  e.  CC )
320207, 319, 2293jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  e.  CC  /\  ( E  /  N
)  e.  CC  /\  ( L  -  1
)  e.  CC ) )
321 subdir 9230 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  ( E  /  N
)  e.  CC  /\  ( L  -  1
)  e.  CC )  ->  ( ( 1  -  ( E  /  N ) )  x.  ( L  -  1 ) )  =  ( ( 1  x.  ( L  -  1 ) )  -  ( ( E  /  N )  x.  ( L  - 
1 ) ) ) )
322320, 321syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  =  ( ( 1  x.  ( L  -  1 ) )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
323 mulid2 8852 . . . . . . . . . . . . . . 15  |-  ( ( L  -  1 )  e.  CC  ->  (
1  x.  ( L  -  1 ) )  =  ( L  - 
1 ) )
324229, 323syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  x.  ( L  -  1 ) )  =  ( L  -  1 ) )
325324oveq1d 5889 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1  x.  ( L  -  1 ) )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( ( L  -  1 )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
326322, 325eqtrd 2328 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) )  =  ( ( L  -  1 )  -  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )
327326oveq2d 5890 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( E  x.  ( ( L  - 
1 )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) ) ) )
328319, 229jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E  /  N )  e.  CC  /\  ( L  -  1 )  e.  CC ) )
329 mulcl 8837 . . . . . . . . . . . . . 14  |-  ( ( ( E  /  N
)  e.  CC  /\  ( L  -  1
)  e.  CC )  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  e.  CC )
330328, 329syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  e.  CC )
331209, 229, 3303jca 1132 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  e.  CC  /\  ( L  -  1 )  e.  CC  /\  ( ( E  /  N )  x.  ( L  -  1 ) )  e.  CC ) )
332 subdi 9229 . . . . . . . . . . . 12  |-  ( ( E  e.  CC  /\  ( L  -  1
)  e.  CC  /\  ( ( E  /  N )  x.  ( L  -  1 ) )  e.  CC )  ->  ( E  x.  ( ( L  - 
1 )  -  (
( E  /  N
)  x.  ( L  -  1 ) ) ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) ) )
333331, 332syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( L  -  1 )  -  ( ( E  /  N )  x.  ( L  - 
1 ) ) ) )  =  ( ( E  x.  ( L  -  1 ) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) ) )
334327, 333eqtrd 2328 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) ) ) )
335209, 268, 2293jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  e.  CC  /\  ( N  e.  CC  /\  N  =/=  0 )  /\  ( L  - 
1 )  e.  CC ) )
336 div32 9460 . . . . . . . . . . . . . 14  |-  ( ( E  e.  CC  /\  ( N  e.  CC  /\  N  =/=  0 )  /\  ( L  - 
1 )  e.  CC )  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  =  ( E  x.  ( ( L  -  1 )  /  N ) ) )
337335, 336syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  /  N )  x.  ( L  -  1 ) )  =  ( E  x.  ( ( L  -  1 )  /  N ) ) )
338337oveq2d 5890 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
339229, 265, 2673jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  - 
1 )  e.  CC  /\  N  e.  CC  /\  N  =/=  0 ) )
340 divcl 9446 . . . . . . . . . . . . . . 15  |-  ( ( ( L  -  1 )  e.  CC  /\  N  e.  CC  /\  N  =/=  0 )  ->  (
( L  -  1 )  /  N )  e.  CC )
341339, 340syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  - 
1 )  /  N
)  e.  CC )
342209, 209, 3413jca 1132 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  e.  CC  /\  E  e.  CC  /\  ( ( L  - 
1 )  /  N
)  e.  CC ) )
343 mulass 8841 . . . . . . . . . . . . 13  |-  ( ( E  e.  CC  /\  E  e.  CC  /\  (
( L  -  1 )  /  N )  e.  CC )  -> 
( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
344342, 343syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) )  =  ( E  x.  ( E  x.  ( ( L  - 
1 )  /  N
) ) ) )
345338, 344eqtr4d 2331 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( E  /  N
)  x.  ( L  -  1 ) ) )  =  ( ( E  x.  E )  x.  ( ( L  -  1 )  /  N ) ) )
346345oveq2d 5890 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  ( L  -  1
) )  -  ( E  x.  ( ( E  /  N )  x.  ( L  -  1 ) ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )
347334, 346eqtrd 2328 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  (
( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )  =  ( ( E  x.  ( L  - 
1 ) )  -  ( ( E  x.  E )  x.  (
( L  -  1 )  /  N ) ) ) )
348316, 347breqtrrd 4065 . . . . . . . 8  |-  ( ph  ->  ( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) ) )
349348adantr 451 . . . . . . 7  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  -  ( 4  /  3
) )  x.  E
)  <  ( E  x.  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) ) )
350 fzfid 11051 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 ... ( L  -  2 ) )  e.  Fin )
351207, 319jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  e.  CC  /\  ( E  /  N
)  e.  CC ) )
352 subcl 9067 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  ( E  /  N
)  e.  CC )  ->  ( 1  -  ( E  /  N
) )  e.  CC )
353351, 352syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  -  ( E  /  N ) )  e.  CC )
354350, 353jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0 ... ( L  -  2 ) )  e.  Fin  /\  ( 1  -  ( E  /  N ) )  e.  CC ) )
355 fsumconst 12268 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
356354, 355syl 15 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( L  -  2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
357356adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( # `  ( 0 ... ( L  -  2 ) ) )  x.  (
1  -  ( E  /  N ) ) ) )
35868a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  e.  ZZ )
35965adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( 1 ... N ) )
360359, 197syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ZZ )
361 2z 10070 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  ZZ
362361a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  e.  ZZ )
363360, 362jca 518 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  e.  ZZ  /\  2  e.  ZZ ) )
364 zsubcl 10077 . . . . . . . . . . . . . . . . 17  |-  ( ( L  e.  ZZ  /\  2  e.  ZZ )  ->  ( L  -  2 )  e.  ZZ )
365363, 364syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  -  2 )  e.  ZZ )
366 elnnuz 10280 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN  <->  N  e.  ( ZZ>= `  1 )
)
367243, 366sylib 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
368 elfzp12 10877 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( L  e.  ( 1 ... N
)  <->  ( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N
) ) ) )
369367, 368syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  e.  ( 1 ... N )  <-> 
( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N ) ) ) )
37065, 369mpbid 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  =  1  \/  L  e.  ( ( 1  +  1 ) ... N ) ) )
371370orcanai 879 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( (
1  +  1 ) ... N ) )
372 1p1e2 9856 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  +  1 )  =  2
373372a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 1  +  1 )  =  2 )
374373oveq1d 5889 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( 1  +  1 ) ... N
)  =  ( 2 ... N ) )
375371, 374eleqtrd 2372 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  ( 2 ... N ) )
376 elfzle1 10815 . . . . . . . . . . . . . . . . . 18  |-  ( L  e.  ( 2 ... N )  ->  2  <_  L )
377375, 376syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  <_  L )
378199adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  L  =  1 )  ->  L  e.  RR )
379 2re 9831 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
380379a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  L  =  1 )  -> 
2  e.  RR )
381378, 380jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  e.  RR  /\  2  e.  RR ) )
382 subge0 9303 . . . . . . . . . . . . . . . . . 18  |-  ( ( L  e.  RR  /\  2  e.  RR )  ->  ( 0  <_  ( L  -  2 )  <->  2  <_  L )
)
383381, 382syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0  <_  ( L  -  2 )  <->  2  <_  L )
)
384377, 383mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  L  =  1 )  -> 
0  <_  ( L  -  2 ) )
385358, 365, 3843jca 1132 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ  /\  0  <_  ( L  - 
2 ) ) )
386 eluz2 10252 . . . . . . . . . . . . . . 15  |-  ( ( L  -  2 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( L  -  2 )  e.  ZZ  /\  0  <_ 
( L  -  2 ) ) )
387385, 386sylibr 203 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( L  -  2 )  e.  ( ZZ>= ` 
0 ) )
388 hashfz 11397 . . . . . . . . . . . . . 14  |-  ( ( L  -  2 )  e.  ( ZZ>= `  0
)  ->  ( # `  (
0 ... ( L  - 
2 ) ) )  =  ( ( ( L  -  2 )  -  0 )  +  1 ) )
389387, 388syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( # `  ( 0 ... ( L  - 
2 ) ) )  =  ( ( ( L  -  2 )  -  0 )  +  1 ) )
390 2cn 9832 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  CC
391390a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  2  e.  CC )
392206, 391jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  CC  /\  2  e.  CC ) )
393 subcl 9067 . . . . . . . . . . . . . . . . . 18  |-  ( ( L  e.  CC  /\  2  e.  CC )  ->  ( L  -  2 )  e.  CC )
394392, 393syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  2 )  e.  CC )
395 subid1 9084 . . . . . . . . . . . . . . . . 17  |-  ( ( L  -  2 )  e.  CC  ->  (
( L  -  2 )  -  0 )  =  ( L  - 
2 ) )
396394, 395syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
2 )  -  0 )  =  ( L  -  2 ) )
397396oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( ( L  -  2 )  +  1 ) )
398206, 391, 2073jca 1132 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  e.  CC  /\  2  e.  CC  /\  1  e.  CC )
)
399 subadd23 9079 . . . . . . . . . . . . . . . . 17  |-  ( ( L  e.  CC  /\  2  e.  CC  /\  1  e.  CC )  ->  (
( L  -  2 )  +  1 )  =  ( L  +  ( 1  -  2 ) ) )
400398, 399syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
2 )  +  1 )  =  ( L  +  ( 1  -  2 ) ) )
401390, 180pm3.2i 441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  e.  CC  /\  1  e.  CC )
402 negsubdi2 9122 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  CC  /\  1  e.  CC )  -> 
-u ( 2  -  1 )  =  ( 1  -  2 ) )
403401, 402ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  -u (
2  -  1 )  =  ( 1  -  2 )
404390, 180, 1803pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  e.  CC  /\  1  e.  CC  /\  1  e.  CC )
405 subadd 9070 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
( 2  -  1 )  =  1  <->  (
1  +  1 )  =  2 ) )
406404, 405ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  -  1 )  =  1  <->  ( 1  +  1 )  =  2 )
407372, 406mpbir 200 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  -  1 )  =  1
408407negeqi 9061 . . . . . . . . . . . . . . . . . . . 20  |-  -u (
2  -  1 )  =  -u 1
409403, 408eqtr3i 2318 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  -  2 )  = 
-u 1
410409a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  -  2 )  =  -u 1
)
411410oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  +  ( 1  -  2 ) )  =  ( L  +  -u 1 ) )
412 negsub 9111 . . . . . . . . . . . . . . . . . 18  |-  ( ( L  e.  CC  /\  1  e.  CC )  ->  ( L  +  -u
1 )  =  ( L  -  1 ) )
413227, 412syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  +  -u
1 )  =  ( L  -  1 ) )
414411, 413eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( L  +  ( 1  -  2 ) )  =  ( L  -  1 ) )
415400, 414eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  - 
2 )  +  1 )  =  ( L  -  1 ) )
416397, 415eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( L  -  1 ) )
417416adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( ( L  -  2 )  - 
0 )  +  1 )  =  ( L  -  1 ) )
418389, 417eqtrd 2328 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( # `  ( 0 ... ( L  - 
2 ) ) )  =  ( L  - 
1 ) )
419418oveq1d 5889 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( # `  (
0 ... ( L  - 
2 ) ) )  x.  ( 1  -  ( E  /  N
) ) )  =  ( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) ) )
420229, 353jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( L  - 
1 )  e.  CC  /\  ( 1  -  ( E  /  N ) )  e.  CC ) )
421 mulcom 8839 . . . . . . . . . . . . 13  |-  ( ( ( L  -  1 )  e.  CC  /\  ( 1  -  ( E  /  N ) )  e.  CC )  -> 
( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
422420, 421syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
423422adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( L  - 
1 )  x.  (
1  -  ( E  /  N ) ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  - 
1 ) ) )
424419, 423eqtrd 2328 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( ( # `  (
0 ... ( L  - 
2 ) ) )  x.  ( 1  -  ( E  /  N
) ) )  =  ( ( 1  -  ( E  /  N
) )  x.  ( L  -  1 ) ) )
425357, 424eqtrd 2328 . . . . . . . . 9  |-  ( (
ph  /\  -.  L  =  1 )  ->  sum_ i  e.  ( 0 ... ( L  - 
2 ) ) ( 1  -  ( E  /  N ) )  =  ( ( 1  -  ( E  /  N ) )  x.  ( L  -  1 ) ) )
426 fzfid 11051 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0 ... ( L  -  2 ) )  e.  Fin )
427 fzn0 10825 . . . . . . . . . . 11  |-  ( ( 0 ... ( L  -  2 ) )  =/=  (/)  <->  ( L  - 
2 )  e.  (
ZZ>= `  0 ) )
428387, 427sylibr 203 . . . . . . . . . 10  |-  ( (
ph  /\  -.  L  =  1 )  -> 
( 0 ... ( L  -  2 ) )  =/=  (/) )
42947, 256, 2673jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  e.  RR  /\  N  e.  RR  /\  N  =/=  0 ) )
430 redivcl 9495 . . . . . . . . . . . . . 14  |-  ( ( E  e.  RR  /\  N  e.  RR  /\  N  =/=  0 )  ->  ( E  /  N )  e.  RR )
431429, 430syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  /  N
)  e.  RR )
432175, 431jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  e.  RR  /\  ( E  /  N
)  e.  RR ) )
433 resubcl 9127 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  ( E  /  N
)  e.  RR )  ->  ( 1  -  ( E  /  N
) )  e.  RR )
434432, 433syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  -  ( E  /  N ) )  e.  RR )
435434ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( 1  -  ( E  /  N ) )  e.  RR )
436 simpll 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ph )
437361a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  2  e.  ZZ )
438204, 437jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( L  e.  ZZ  /\  2  e.  ZZ ) )
439438, 364syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  2 )  e.  ZZ )
440 2pos 9844 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  2
44138, 379pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  e.  RR  /\  2  e.  RR )
442 ltle 8926 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR  /\  2  e.  RR )  ->  ( 0  <  2  ->  0  <_  2 ) )
443441, 442ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <  2  ->  0  <_  2 )
444440, 443ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  2
445379a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  2  e.  RR )
446204, 198syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  L  e.  RR )
447110, 445, 4463jca 1132 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 0  e.  RR  /\  2  e.  RR  /\  L  e.  RR )
)
448 lesub2 9285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  RR  /\  2  e.  RR  /\  L  e.  RR )  ->  (
0  <_  2  <->  ( L  -  2 )  <_ 
( L  -  0 ) ) )
449447, 448syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 0  <_  2  <->  ( L  -  2 )  <_  ( L  - 
0 ) ) )
450444, 449mpbii 202 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  -  2 )  <_  ( L  -  0 ) )
451446, 32syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  L  e.  CC )
452451, 34syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  -  0 )  =  L )
453450, 452breqtrd 4063 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( L  -  2 )  <_  L )
454 elfzle2 10816 . . . . . . . . . . . . . . . . . . . 20  |-  ( L  e.  ( 1 ... N )  ->  L  <_  N )
45565, 454syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  L  <_  N )
456453, 455jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( L  - 
2 )  <_  L  /\  L  <_  N ) )
457446idi 2 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  L  e.  RR )
458457, 445jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  e.  RR  /\  2  e.  RR ) )
459 resubcl 9127 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( L  e.  RR  /\  2  e.  RR )  ->  ( L  -  2 )  e.  RR )
460458, 459syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  -  2 )  e.  RR )
461 zre 10044 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ZZ  ->  N  e.  RR )
462245, 461syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  RR )
463460, 446, 4623jca 1132 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( L  - 
2 )  e.  RR  /\  L  e.  RR  /\  N  e.  RR )
)
464 letr 8930 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( L  -  2 )  e.  RR  /\  L  e.  RR  /\  N  e.  RR )  ->  (
( ( L  - 
2 )  <_  L  /\  L  <_  N )  ->  ( L  - 
2 )  <_  N
) )
465463, 464syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( L  -  2 )  <_  L  /\  L  <_  N
)  ->  ( L  -  2 )  <_  N ) )
466456, 465mpd 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  -  2 )  <_  N )
467439, 245, 4663jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( L  - 
2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2
)  <_  N )
)
468 eluz2 10252 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  ( L  -  2 ) )  <->  ( ( L  -  2 )  e.  ZZ  /\  N  e.  ZZ  /\  ( L  -  2 )  <_  N ) )
469467, 468sylibr 203 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  ( ZZ>= `  ( L  -  2
) ) )
470 fzss2 10847 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  ( L  -  2 ) )  ->  ( 0 ... ( L  - 
2 ) )  C_  ( 0 ... N
) )
471469, 470syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0 ... ( L  -  2 ) )  C_  ( 0 ... N ) )
472 ssel2 3188 . . . . . . . . . . . . . 14  |-  ( ( ( 0 ... ( L  -  2 ) )  C_  ( 0 ... N )  /\  i  e.  ( 0 ... ( L  - 
2 ) ) )  ->  i  e.  ( 0 ... N ) )
473471, 472sylan 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  ( 0 ... N
) )
474473adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  ( 0 ... N
) )
475436, 474jca 518 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( ph  /\  i  e.  ( 0 ... N ) ) )
476475, 106syl 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  -.  L  =  1 )  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( ( X `  i ) `  S )  e.  RR )
477102adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  S  e.  T )
478 elfzle2 10816 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  <_  ( L  -  2 ) )
479478adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  <_  ( L  -  2 ) )
480 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  e.  ZZ )
481 zre 10044 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ZZ  ->  i  e.  RR )
482480, 481syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... ( L  -  2 ) )  ->  i  e.  RR )
483482adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  i  e.  RR )
484199adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  L  e.  RR )
485379a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  2  e.  RR )
486484, 485jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  e.  RR  /\  2  e.  RR ) )
487486, 459syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( L  -  2 )  e.  RR )
488173a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
1  /  3 )  e.  RR )
489483, 487, 4883jca 1132 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  e.  RR  /\  ( L  -  2
)  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
490 leadd1 9258 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  RR  /\  ( L  -  2
)  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( i  <_ 
( L  -  2 )  <->  ( i  +  ( 1  /  3
) )  <_  (
( L  -  2 )  +  ( 1  /  3 ) ) ) )
491489, 490syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  <_  ( L  -  2 )  <->  ( i  +  ( 1  / 
3 ) )  <_ 
( ( L  - 
2 )  +  ( 1  /  3 ) ) ) )
492479, 491mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  +  ( 1  /  3 ) )  <_  ( ( L  -  2 )  +  ( 1  /  3
) ) )
493483, 488jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
494 readdcl 8836 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( i  +  ( 1  /  3
) )  e.  RR )
495493, 494syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
i  +  ( 1  /  3 ) )  e.  RR )
496487, 488jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( L  -  2 )  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
497 readdcl 8836 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( L  -  2 )  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( ( L  -  2 )  +  ( 1  /  3
) )  e.  RR )
498496, 497syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( L  -  2 )  +  ( 1  /  3 ) )  e.  RR )
499222adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  ( E  e.  RR  /\  0  <  E ) )
500495, 498, 4993jca 1132 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  e.  RR  /\  ( ( L  - 
2 )  +  ( 1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
501 lemul1 9624 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) )
502500, 501syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  <_  ( ( L  -  2 )  +  ( 1  / 
3 ) )  <->  ( (
i  +  ( 1  /  3 ) )  x.  E )  <_ 
( ( ( L  -  2 )  +  ( 1  /  3
) )  x.  E
) ) )
503492, 502mpbid 201 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... ( L  -  2 ) ) )  ->  (
( i  +  ( 1  /  3 ) )  x.  E )  <_  ( ( ( L  -  2 )  +  ( 1  / 
3 ) )  x.  E ) )
504 1lt2 9902 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  <  2
505504a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  1  <  2 )
5061, 379, 223pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1  e.  RR  /\  2  e.  RR  /\  ( 3  e.  RR  /\  0  <  3 ) )
507506a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( 1  e.  RR  /\  2  e.  RR  /\  ( 3  e.  RR  /\  0  <  3 ) ) )
508 ltdiv1 9636 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  (
3  e.  RR  /\  0  <  3 ) )  ->  ( 1  <  2  <->  ( 1  / 
3 )  <  (
2  /  3 ) ) )
509507, 508syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1  <  2  <->  ( 1  /  3 )  <  ( 2  / 
3 ) ) )
510505, 509mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1  /  3
)  <  ( 2  /  3 ) )
511379, 7, 83pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 2  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
512 redivcl 9495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
2  /  3 )  e.  RR )
513511, 512ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 2  /  3 )  e.  RR
514513a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( 2  /  3
)  e.  RR )
515174, 514, 2183jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( 1  / 
3 )  e.  RR  /\  ( 2  /  3
)  e.  RR  /\  ( L  -  1
)  e.  RR ) )
516 ltsub2 9287 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 1  /  3
)  e.  RR  /\  ( 2  /  3
)  e.  RR  /\  ( L  -  1
)  e.  RR )  ->  ( ( 1  /  3 )  < 
( 2  /  3
)  <->  ( ( L  -  1 )  -  ( 2  /  3
) )  <  (
( L  -  1 )  -  ( 1  /  3 ) ) ) )
517515, 516syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 1  / 
3 )  <  (
2  /  3 )  <-> 
( ( L  - 
1 )  -  (
2  /  3 ) )  <  ( ( L  -  1 )  -  ( 1  / 
3 ) ) ) )
518510, 517mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  <  ( ( L  -  1 )  -  ( 1  / 
3 ) ) )
519 addid1 9008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 1  e.  CC  ->  (
1  +  0 )  =  1 )
520519eqcomd 2301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 1  e.  CC  ->  1  =  ( 1  +  0 ) )
521207, 520syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  1  =  ( 1  +  0 ) )
522 subid 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 1  e.  CC  ->  (
1  -  1 )  =  0 )
523207, 522syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( 1  -  1 )  =  0 )
524523eqcomd 2301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  0  =  ( 1  -  1 ) )
525524oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( 1  +  0 )  =  ( 1  +  ( 1  -  1 ) ) )
526207, 207, 2073jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )
)
527 addsubass 9077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
( 1  +  1 )  -  1 )  =  ( 1  +  ( 1  -  1 ) ) )
528527eqcomd 2301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
1  +  ( 1  -  1 ) )  =  ( ( 1  +  1 )  - 
1 ) )
529526, 528syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( 1  +  ( 1  -  1 ) )  =  ( ( 1  +  1 )  -  1 ) )
530525, 529eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( 1  +  0 )  =  ( ( 1  +  1 )  -  1 ) )
531521, 530eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  1  =  ( ( 1  +  1 )  -  1 ) )
532531oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( L  -  1 )  =  ( L  -  ( ( 1  +  1 )  - 
1 ) ) )
533372a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( 1  +  1 )  =  2 )
534533oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( ( 1  +  1 )  -  1 )  =  ( 2  -  1 ) )
535534oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( L  -  (
( 1  +  1 )  -  1 ) )  =  ( L  -  ( 2  -  1 ) ) )
536 subsub 9093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( L  e.  CC  /\  2  e.  CC  /\  1  e.  CC )  ->  ( L  -  ( 2  -  1 ) )  =  ( ( L  -  2 )  +  1 ) )
537398, 536syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( L  -  (
2  -  1 ) )  =  ( ( L  -  2 )  +  1 ) )
538535, 537eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( L  -  (
( 1  +  1 )  -  1 ) )  =  ( ( L  -  2 )  +  1 ) )
539532, 538eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( L  -  1 )  =  ( ( L  -  2 )  +  1 ) )
540539oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  =  ( ( ( L  -  2 )  +  1 )  -  ( 2  / 
3 ) ) )
541390, 16, 83pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )
542 divcl 9446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )  ->  (
2  /  3 )  e.  CC )
543541, 542ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2  /  3 )  e.  CC
544543a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 2  /  3
)  e.  CC )
545394, 207, 5443jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( L  - 
2 )  e.  CC  /\  1  e.  CC  /\  ( 2  /  3
)  e.  CC ) )
546 addsubass 9077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( L  -  2 )  e.  CC  /\  1  e.  CC  /\  (
2  /  3 )  e.  CC )  -> 
( ( ( L  -  2 )  +  1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  -  ( 2  /  3
) ) ) )
547545, 546syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( ( L  -  2 )  +  1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  -  ( 2  /  3
) ) ) )
548540, 547eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( L  - 
1 )  -  (
2  /  3 ) )  =  ( ( L  -  2 )  +  ( 1  -  ( 2  /  3
) ) ) )
549 df-3 9821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  3  =  ( 2  +  1 )
550549oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 3  /  3 )  =  ( ( 2  +  1 )  /  3
)
551390, 180, 173pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 2  e.  CC  /\  1  e.  CC  /\  ( 3  e.  CC  /\  3  =/=  0 ) )
552 divdir 9463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 2  e.  CC  /\  1  e.  CC  /\  (
3  e.  CC  /\  3  =/=  0 ) )  ->  ( ( 2  +  1 )  / 
3 )  =  ( ( 2  /  3
)  +  ( 1  /  3 ) ) )
553551, 552ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 2  +  1 )  /  3 )  =  ( ( 2  / 
3 )  +  ( 1  /  3 ) )
554550, 553eqtri 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 3  /  3 )  =  ( ( 2  / 
3 )  +  ( 1  /  3 ) )
555554eqcomi 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2  /  3 )  +  ( 1  / 
3 ) )  =  ( 3  /  3
)
556555, 19eqtri 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2  /  3 )  +  ( 1  / 
3 ) )  =  1
557180, 16, 83pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 1  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )
558 divcl 9446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 1  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  CC )
559557, 558ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 1  /  3 )  e.  CC
560180, 543, 5593pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 1  e.  CC  /\  (
2  /  3 )  e.  CC  /\