Metamath Proof Explorer


Theorem stoweidlem26

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)

Ref Expression
Hypotheses 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 stoweidlem26
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) )

Proof

Step Hyp Ref Expression
1 stoweidlem26.1
 |-  F/_ t F
2 stoweidlem26.2
 |-  F/ j ph
3 stoweidlem26.3
 |-  F/ t ph
4 stoweidlem26.4
 |-  D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
5 stoweidlem26.5
 |-  B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
6 stoweidlem26.6
 |-  ( ph -> N e. NN )
7 stoweidlem26.7
 |-  ( ph -> T e. _V )
8 stoweidlem26.8
 |-  ( ph -> L e. ( 1 ... N ) )
9 stoweidlem26.9
 |-  ( ph -> S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) )
10 stoweidlem26.10
 |-  ( ph -> F : T --> RR )
11 stoweidlem26.11
 |-  ( ph -> E e. RR+ )
12 stoweidlem26.12
 |-  ( ph -> E < ( 1 / 3 ) )
13 stoweidlem26.13
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
14 stoweidlem26.14
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
15 stoweidlem26.15
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
16 1re
 |-  1 e. RR
17 eleq1
 |-  ( L = 1 -> ( L e. RR <-> 1 e. RR ) )
18 16 17 mpbiri
 |-  ( L = 1 -> L e. RR )
19 18 adantl
 |-  ( ( ph /\ L = 1 ) -> L e. RR )
20 4re
 |-  4 e. RR
21 20 a1i
 |-  ( ( ph /\ L = 1 ) -> 4 e. RR )
22 3re
 |-  3 e. RR
23 22 a1i
 |-  ( ( ph /\ L = 1 ) -> 3 e. RR )
24 3ne0
 |-  3 =/= 0
25 24 a1i
 |-  ( ( ph /\ L = 1 ) -> 3 =/= 0 )
26 21 23 25 redivcld
 |-  ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
27 19 26 resubcld
 |-  ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
28 11 rpred
 |-  ( ph -> E e. RR )
29 28 adantr
 |-  ( ( ph /\ L = 1 ) -> E e. RR )
30 27 29 remulcld
 |-  ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
31 0red
 |-  ( ( ph /\ L = 1 ) -> 0 e. RR )
32 fzfid
 |-  ( ph -> ( 0 ... N ) e. Fin )
33 28 adantr
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> E e. RR )
34 eldif
 |-  ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
35 9 34 sylib
 |-  ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
36 35 simpld
 |-  ( ph -> S e. ( D ` L ) )
37 oveq1
 |-  ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) )
38 37 oveq1d
 |-  ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) )
39 38 breq2d
 |-  ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
40 39 rabbidv
 |-  ( j = L -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
41 fz1ssfz0
 |-  ( 1 ... N ) C_ ( 0 ... N )
42 41 8 sseldi
 |-  ( ph -> L e. ( 0 ... N ) )
43 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
44 7 43 syl
 |-  ( ph -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
45 4 40 42 44 fvmptd3
 |-  ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
46 36 45 eleqtrd
 |-  ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
47 nfcv
 |-  F/_ t S
48 nfcv
 |-  F/_ t T
49 1 47 nffv
 |-  F/_ t ( F ` S )
50 nfcv
 |-  F/_ t <_
51 nfcv
 |-  F/_ t ( ( L - ( 1 / 3 ) ) x. E )
52 49 50 51 nfbr
 |-  F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E )
53 fveq2
 |-  ( t = S -> ( F ` t ) = ( F ` S ) )
54 53 breq1d
 |-  ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
55 47 48 52 54 elrabf
 |-  ( S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
56 46 55 sylib
 |-  ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
57 56 simpld
 |-  ( ph -> S e. T )
58 57 adantr
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T )
59 13 58 ffvelrnd
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
60 33 59 remulcld
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
61 32 60 fsumrecl
 |-  ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
62 61 adantr
 |-  ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
63 20 22 24 redivcli
 |-  ( 4 / 3 ) e. RR
64 63 a1i
 |-  ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
65 19 64 resubcld
 |-  ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
66 19 recnd
 |-  ( ( ph /\ L = 1 ) -> L e. CC )
67 66 subid1d
 |-  ( ( ph /\ L = 1 ) -> ( L - 0 ) = L )
68 3cn
 |-  3 e. CC
69 68 24 dividi
 |-  ( 3 / 3 ) = 1
70 3lt4
 |-  3 < 4
71 3pos
 |-  0 < 3
72 22 20 22 71 ltdiv1ii
 |-  ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) )
73 70 72 mpbi
 |-  ( 3 / 3 ) < ( 4 / 3 )
74 69 73 eqbrtrri
 |-  1 < ( 4 / 3 )
75 breq1
 |-  ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
76 75 adantl
 |-  ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
77 74 76 mpbiri
 |-  ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) )
78 67 77 eqbrtrd
 |-  ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) )
79 19 31 64 78 ltsub23d
 |-  ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 )
80 11 rpgt0d
 |-  ( ph -> 0 < E )
81 80 adantr
 |-  ( ( ph /\ L = 1 ) -> 0 < E )
82 mulltgt0
 |-  ( ( ( ( L - ( 4 / 3 ) ) e. RR /\ ( L - ( 4 / 3 ) ) < 0 ) /\ ( E e. RR /\ 0 < E ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
83 65 79 29 81 82 syl22anc
 |-  ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
84 0cn
 |-  0 e. CC
85 fsumconst
 |-  ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
86 32 84 85 sylancl
 |-  ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
87 hashcl
 |-  ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 )
88 nn0cn
 |-  ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC )
89 32 87 88 3syl
 |-  ( ph -> ( # ` ( 0 ... N ) ) e. CC )
90 89 mul01d
 |-  ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 )
91 86 90 eqtrd
 |-  ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 )
92 91 adantr
 |-  ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 )
93 0red
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR )
94 11 rpge0d
 |-  ( ph -> 0 <_ E )
95 94 adantr
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E )
96 nfv
 |-  F/ t i e. ( 0 ... N )
97 3 96 nfan
 |-  F/ t ( ph /\ i e. ( 0 ... N ) )
98 nfv
 |-  F/ t 0 <_ ( ( X ` i ) ` S )
99 97 98 nfim
 |-  F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
100 fveq2
 |-  ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) )
101 100 breq2d
 |-  ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) )
102 101 imbi2d
 |-  ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) ) )
103 14 3expia
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) )
104 103 com12
 |-  ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) )
105 47 99 102 104 vtoclgaf
 |-  ( S e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) )
106 58 105 mpcom
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
107 33 59 95 106 mulge0d
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
108 32 93 60 107 fsumle
 |-  ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
109 108 adantr
 |-  ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
110 92 109 eqbrtrrd
 |-  ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
111 30 31 62 83 110 ltletrd
 |-  ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
112 elfzelz
 |-  ( L e. ( 1 ... N ) -> L e. ZZ )
113 zre
 |-  ( L e. ZZ -> L e. RR )
114 8 112 113 3syl
 |-  ( ph -> L e. RR )
115 20 a1i
 |-  ( ph -> 4 e. RR )
116 22 a1i
 |-  ( ph -> 3 e. RR )
117 24 a1i
 |-  ( ph -> 3 =/= 0 )
118 115 116 117 redivcld
 |-  ( ph -> ( 4 / 3 ) e. RR )
119 114 118 resubcld
 |-  ( ph -> ( L - ( 4 / 3 ) ) e. RR )
120 119 28 remulcld
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
121 120 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
122 16 a1i
 |-  ( ph -> 1 e. RR )
123 28 6 nndivred
 |-  ( ph -> ( E / N ) e. RR )
124 122 123 resubcld
 |-  ( ph -> ( 1 - ( E / N ) ) e. RR )
125 114 122 resubcld
 |-  ( ph -> ( L - 1 ) e. RR )
126 124 125 remulcld
 |-  ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
127 28 126 remulcld
 |-  ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
128 127 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
129 fzfid
 |-  ( ph -> ( 0 ... ( L - 2 ) ) e. Fin )
130 8 elfzelzd
 |-  ( ph -> L e. ZZ )
131 2z
 |-  2 e. ZZ
132 131 a1i
 |-  ( ph -> 2 e. ZZ )
133 130 132 zsubcld
 |-  ( ph -> ( L - 2 ) e. ZZ )
134 6 nnzd
 |-  ( ph -> N e. ZZ )
135 130 zred
 |-  ( ph -> L e. RR )
136 2re
 |-  2 e. RR
137 136 a1i
 |-  ( ph -> 2 e. RR )
138 135 137 resubcld
 |-  ( ph -> ( L - 2 ) e. RR )
139 6 nnred
 |-  ( ph -> N e. RR )
140 0le2
 |-  0 <_ 2
141 0red
 |-  ( ph -> 0 e. RR )
142 141 137 135 lesub2d
 |-  ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) )
143 140 142 mpbii
 |-  ( ph -> ( L - 2 ) <_ ( L - 0 ) )
144 130 zcnd
 |-  ( ph -> L e. CC )
145 144 subid1d
 |-  ( ph -> ( L - 0 ) = L )
146 143 145 breqtrd
 |-  ( ph -> ( L - 2 ) <_ L )
147 elfzle2
 |-  ( L e. ( 1 ... N ) -> L <_ N )
148 8 147 syl
 |-  ( ph -> L <_ N )
149 138 135 139 146 148 letrd
 |-  ( ph -> ( L - 2 ) <_ N )
150 133 134 149 3jca
 |-  ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
151 eluz2
 |-  ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
152 150 151 sylibr
 |-  ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) )
153 fzss2
 |-  ( N e. ( ZZ>= ` ( L - 2 ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
154 152 153 syl
 |-  ( ph -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
155 154 sselda
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
156 155 59 syldan
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
157 129 156 fsumrecl
 |-  ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
158 28 157 remulcld
 |-  ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
159 158 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
160 28 125 remulcld
 |-  ( ph -> ( E x. ( L - 1 ) ) e. RR )
161 28 28 remulcld
 |-  ( ph -> ( E x. E ) e. RR )
162 160 161 resubcld
 |-  ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR )
163 125 6 nndivred
 |-  ( ph -> ( ( L - 1 ) / N ) e. RR )
164 161 163 remulcld
 |-  ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR )
165 160 164 resubcld
 |-  ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR )
166 125 28 resubcld
 |-  ( ph -> ( ( L - 1 ) - E ) e. RR )
167 122 28 readdcld
 |-  ( ph -> ( 1 + E ) e. RR )
168 16 22 24 redivcli
 |-  ( 1 / 3 ) e. RR
169 168 a1i
 |-  ( ph -> ( 1 / 3 ) e. RR )
170 28 169 122 12 ltadd2dd
 |-  ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) )
171 ax-1cn
 |-  1 e. CC
172 68 171 68 24 divdiri
 |-  ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
173 3p1e4
 |-  ( 3 + 1 ) = 4
174 173 oveq1i
 |-  ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
175 69 oveq1i
 |-  ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
176 172 174 175 3eqtr3ri
 |-  ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
177 170 176 breqtrdi
 |-  ( ph -> ( 1 + E ) < ( 4 / 3 ) )
178 167 118 114 177 ltsub2dd
 |-  ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) )
179 171 a1i
 |-  ( ph -> 1 e. CC )
180 11 rpcnd
 |-  ( ph -> E e. CC )
181 144 179 180 subsub4d
 |-  ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) )
182 178 181 breqtrrd
 |-  ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) )
183 119 166 11 182 ltmul1dd
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) )
184 144 179 subcld
 |-  ( ph -> ( L - 1 ) e. CC )
185 184 180 subcld
 |-  ( ph -> ( ( L - 1 ) - E ) e. CC )
186 180 185 mulcomd
 |-  ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) )
187 180 184 180 subdid
 |-  ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
188 186 187 eqtr3d
 |-  ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
189 183 188 breqtrd
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
190 1zzd
 |-  ( ph -> 1 e. ZZ )
191 elfz
 |-  ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
192 130 190 134 191 syl3anc
 |-  ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
193 8 192 mpbid
 |-  ( ph -> ( 1 <_ L /\ L <_ N ) )
194 193 simprd
 |-  ( ph -> L <_ N )
195 zlem1lt
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
196 130 134 195 syl2anc
 |-  ( ph -> ( L <_ N <-> ( L - 1 ) < N ) )
197 194 196 mpbid
 |-  ( ph -> ( L - 1 ) < N )
198 6 nngt0d
 |-  ( ph -> 0 < N )
199 ltdiv1
 |-  ( ( ( L - 1 ) e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
200 125 139 139 198 199 syl112anc
 |-  ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
201 197 200 mpbid
 |-  ( ph -> ( ( L - 1 ) / N ) < ( N / N ) )
202 6 nncnd
 |-  ( ph -> N e. CC )
203 6 nnne0d
 |-  ( ph -> N =/= 0 )
204 202 203 dividd
 |-  ( ph -> ( N / N ) = 1 )
205 201 204 breqtrd
 |-  ( ph -> ( ( L - 1 ) / N ) < 1 )
206 28 28 80 80 mulgt0d
 |-  ( ph -> 0 < ( E x. E ) )
207 ltmul2
 |-  ( ( ( ( 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 ) ) )
208 163 122 161 206 207 syl112anc
 |-  ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
209 205 208 mpbid
 |-  ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) )
210 180 180 mulcld
 |-  ( ph -> ( E x. E ) e. CC )
211 210 mulid1d
 |-  ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) )
212 209 211 breqtrd
 |-  ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) )
213 164 161 160 212 ltsub2dd
 |-  ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
214 120 162 165 189 213 lttrd
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
215 180 202 203 divcld
 |-  ( ph -> ( E / N ) e. CC )
216 179 215 184 subdird
 |-  ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) )
217 184 mulid2d
 |-  ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) )
218 217 oveq1d
 |-  ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
219 216 218 eqtrd
 |-  ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
220 219 oveq2d
 |-  ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) )
221 215 184 mulcld
 |-  ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC )
222 180 184 221 subdid
 |-  ( ph -> ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) )
223 180 202 184 203 div32d
 |-  ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) )
224 223 oveq2d
 |-  ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
225 184 202 203 divcld
 |-  ( ph -> ( ( L - 1 ) / N ) e. CC )
226 180 180 225 mulassd
 |-  ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
227 224 226 eqtr4d
 |-  ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) )
228 227 oveq2d
 |-  ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
229 220 222 228 3eqtrd
 |-  ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
230 214 229 breqtrrd
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
231 230 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
232 179 215 subcld
 |-  ( ph -> ( 1 - ( E / N ) ) e. CC )
233 fsumconst
 |-  ( ( ( 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 ) ) ) )
234 129 232 233 syl2anc
 |-  ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
235 234 adantr
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
236 0zd
 |-  ( ( ph /\ -. L = 1 ) -> 0 e. ZZ )
237 8 adantr
 |-  ( ( ph /\ -. L = 1 ) -> L e. ( 1 ... N ) )
238 237 elfzelzd
 |-  ( ( ph /\ -. L = 1 ) -> L e. ZZ )
239 131 a1i
 |-  ( ( ph /\ -. L = 1 ) -> 2 e. ZZ )
240 238 239 zsubcld
 |-  ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ )
241 elnnuz
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
242 6 241 sylib
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
243 elfzp12
 |-  ( N e. ( ZZ>= ` 1 ) -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
244 242 243 syl
 |-  ( ph -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
245 8 244 mpbid
 |-  ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) )
246 245 orcanai
 |-  ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) )
247 1p1e2
 |-  ( 1 + 1 ) = 2
248 247 a1i
 |-  ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 )
249 248 oveq1d
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
250 246 249 eleqtrd
 |-  ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) )
251 elfzle1
 |-  ( L e. ( 2 ... N ) -> 2 <_ L )
252 250 251 syl
 |-  ( ( ph /\ -. L = 1 ) -> 2 <_ L )
253 114 adantr
 |-  ( ( ph /\ -. L = 1 ) -> L e. RR )
254 136 a1i
 |-  ( ( ph /\ -. L = 1 ) -> 2 e. RR )
255 253 254 subge0d
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) )
256 252 255 mpbird
 |-  ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) )
257 236 240 256 3jca
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
258 eluz2
 |-  ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
259 257 258 sylibr
 |-  ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) )
260 hashfz
 |-  ( ( L - 2 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
261 259 260 syl
 |-  ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
262 2cn
 |-  2 e. CC
263 262 a1i
 |-  ( ph -> 2 e. CC )
264 144 263 subcld
 |-  ( ph -> ( L - 2 ) e. CC )
265 264 subid1d
 |-  ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) )
266 265 oveq1d
 |-  ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) )
267 144 263 179 subadd23d
 |-  ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) )
268 262 171 negsubdi2i
 |-  -u ( 2 - 1 ) = ( 1 - 2 )
269 2m1e1
 |-  ( 2 - 1 ) = 1
270 269 negeqi
 |-  -u ( 2 - 1 ) = -u 1
271 268 270 eqtr3i
 |-  ( 1 - 2 ) = -u 1
272 271 a1i
 |-  ( ph -> ( 1 - 2 ) = -u 1 )
273 272 oveq2d
 |-  ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) )
274 144 179 negsubd
 |-  ( ph -> ( L + -u 1 ) = ( L - 1 ) )
275 273 274 eqtrd
 |-  ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) )
276 266 267 275 3eqtrd
 |-  ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
277 276 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
278 261 277 eqtrd
 |-  ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) )
279 278 oveq1d
 |-  ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) )
280 184 232 mulcomd
 |-  ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
281 280 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
282 235 279 281 3eqtrd
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
283 fzfid
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin )
284 fzn0
 |-  ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) )
285 259 284 sylibr
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) )
286 124 ad2antrr
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR )
287 simpll
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph )
288 155 adantlr
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
289 287 288 59 syl2anc
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
290 57 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T )
291 elfzelz
 |-  ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ )
292 291 zred
 |-  ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR )
293 292 adantl
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. RR )
294 168 a1i
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 / 3 ) e. RR )
295 293 294 readdcld
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR )
296 28 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR )
297 295 296 remulcld
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR )
298 114 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> L e. RR )
299 136 a1i
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> 2 e. RR )
300 298 299 resubcld
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
301 300 294 readdcld
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
302 301 296 remulcld
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
303 10 57 jca
 |-  ( ph -> ( F : T --> RR /\ S e. T ) )
304 303 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) )
305 ffvelrn
 |-  ( ( F : T --> RR /\ S e. T ) -> ( F ` S ) e. RR )
306 304 305 syl
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F ` S ) e. RR )
307 elfzle2
 |-  ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) )
308 307 adantl
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) )
309 293 300 294 308 leadd1dd
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) )
310 28 80 jca
 |-  ( ph -> ( E e. RR /\ 0 < E ) )
311 310 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) )
312 lemul1
 |-  ( ( ( 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 ) ) )
313 295 301 311 312 syl3anc
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) ) )
314 309 313 mpbid
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) )
315 114 137 resubcld
 |-  ( ph -> ( L - 2 ) e. RR )
316 315 169 readdcld
 |-  ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
317 316 28 remulcld
 |-  ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
318 10 57 ffvelrnd
 |-  ( ph -> ( F ` S ) e. RR )
319 125 169 resubcld
 |-  ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR )
320 319 28 remulcld
 |-  ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR )
321 addid1
 |-  ( 1 e. CC -> ( 1 + 0 ) = 1 )
322 321 eqcomd
 |-  ( 1 e. CC -> 1 = ( 1 + 0 ) )
323 171 322 mp1i
 |-  ( ph -> 1 = ( 1 + 0 ) )
324 179 subidd
 |-  ( ph -> ( 1 - 1 ) = 0 )
325 324 eqcomd
 |-  ( ph -> 0 = ( 1 - 1 ) )
326 325 oveq2d
 |-  ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) )
327 addsubass
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) )
328 327 eqcomd
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
329 179 179 179 328 syl3anc
 |-  ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
330 323 326 329 3eqtrd
 |-  ( ph -> 1 = ( ( 1 + 1 ) - 1 ) )
331 330 oveq2d
 |-  ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) )
332 247 a1i
 |-  ( ph -> ( 1 + 1 ) = 2 )
333 332 oveq1d
 |-  ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) )
334 333 oveq2d
 |-  ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) )
335 144 263 179 subsubd
 |-  ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) )
336 331 334 335 3eqtrd
 |-  ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) )
337 336 oveq1d
 |-  ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) )
338 262 68 24 divcli
 |-  ( 2 / 3 ) e. CC
339 338 a1i
 |-  ( ph -> ( 2 / 3 ) e. CC )
340 264 179 339 addsubassd
 |-  ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) )
341 171 68 24 divcli
 |-  ( 1 / 3 ) e. CC
342 df-3
 |-  3 = ( 2 + 1 )
343 342 oveq1i
 |-  ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
344 262 171 68 24 divdiri
 |-  ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
345 343 69 344 3eqtr3ri
 |-  ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
346 171 338 341 345 subaddrii
 |-  ( 1 - ( 2 / 3 ) ) = ( 1 / 3 )
347 346 a1i
 |-  ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) )
348 347 oveq2d
 |-  ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
349 337 340 348 3eqtrd
 |-  ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
350 136 22 24 redivcli
 |-  ( 2 / 3 ) e. RR
351 350 a1i
 |-  ( ph -> ( 2 / 3 ) e. RR )
352 1lt2
 |-  1 < 2
353 22 71 pm3.2i
 |-  ( 3 e. RR /\ 0 < 3 )
354 16 136 353 3pm3.2i
 |-  ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) )
355 ltdiv1
 |-  ( ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
356 354 355 mp1i
 |-  ( ph -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
357 352 356 mpbii
 |-  ( ph -> ( 1 / 3 ) < ( 2 / 3 ) )
358 169 351 125 357 ltsub2dd
 |-  ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
359 349 358 eqbrtrrd
 |-  ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
360 316 319 11 359 ltmul1dd
 |-  ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
361 35 simprd
 |-  ( ph -> -. S e. ( D ` ( L - 1 ) ) )
362 oveq1
 |-  ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) )
363 362 oveq1d
 |-  ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
364 363 breq2d
 |-  ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
365 364 rabbidv
 |-  ( j = ( L - 1 ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
366 134 peano2zd
 |-  ( ph -> ( N + 1 ) e. ZZ )
367 193 simpld
 |-  ( ph -> 1 <_ L )
368 139 122 readdcld
 |-  ( ph -> ( N + 1 ) e. RR )
369 139 lep1d
 |-  ( ph -> N <_ ( N + 1 ) )
370 114 139 368 194 369 letrd
 |-  ( ph -> L <_ ( N + 1 ) )
371 190 366 130 367 370 elfzd
 |-  ( ph -> L e. ( 1 ... ( N + 1 ) ) )
372 144 179 npcand
 |-  ( ph -> ( ( L - 1 ) + 1 ) = L )
373 0p1e1
 |-  ( 0 + 1 ) = 1
374 373 a1i
 |-  ( ph -> ( 0 + 1 ) = 1 )
375 374 oveq1d
 |-  ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
376 371 372 375 3eltr4d
 |-  ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
377 0zd
 |-  ( ph -> 0 e. ZZ )
378 130 190 zsubcld
 |-  ( ph -> ( L - 1 ) e. ZZ )
379 fzaddel
 |-  ( ( ( 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 ) ) ) )
380 377 134 378 190 379 syl22anc
 |-  ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
381 376 380 mpbird
 |-  ( ph -> ( L - 1 ) e. ( 0 ... N ) )
382 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
383 7 382 syl
 |-  ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
384 4 365 381 383 fvmptd3
 |-  ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
385 361 384 neleqtrd
 |-  ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
386 nfcv
 |-  F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
387 49 50 386 nfbr
 |-  F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
388 53 breq1d
 |-  ( t = S -> ( ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
389 47 48 387 388 elrabf
 |-  ( S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
390 385 389 sylnib
 |-  ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
391 ianor
 |-  ( -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
392 390 391 sylib
 |-  ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
393 olc
 |-  ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
394 393 anim1i
 |-  ( ( 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 ) ) ) )
395 57 392 394 syl2anc
 |-  ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) )
396 orcom
 |-  ( ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) )
397 396 anbi2i
 |-  ( ( ( -. ( 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 ) ) )
398 395 397 sylib
 |-  ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) )
399 pm4.43
 |-  ( -. ( 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 ) ) )
400 398 399 sylibr
 |-  ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
401 320 318 ltnled
 |-  ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
402 400 401 mpbird
 |-  ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
403 317 320 318 360 402 lttrd
 |-  ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
404 317 318 403 ltled
 |-  ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
405 404 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
406 297 302 306 314 405 letrd
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
407 nfcv
 |-  F/_ t ( ( i + ( 1 / 3 ) ) x. E )
408 407 50 49 nfbr
 |-  F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
409 53 breq2d
 |-  ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
410 47 48 408 409 elrabf
 |-  ( S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } <-> ( S e. T /\ ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
411 290 406 410 sylanbrc
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
412 oveq1
 |-  ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
413 412 oveq1d
 |-  ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
414 413 breq1d
 |-  ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
415 414 rabbidv
 |-  ( j = i -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
416 rabexg
 |-  ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
417 7 416 syl
 |-  ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
418 417 adantr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
419 5 415 155 418 fvmptd3
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
420 411 419 eleqtrrd
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
421 150 3ad2ant1
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
422 421 151 sylibr
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) )
423 422 153 syl
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
424 simp2
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
425 423 424 sseldd
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
426 elex
 |-  ( S e. ( B ` i ) -> S e. _V )
427 426 3ad2ant3
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
428 nfcv
 |-  F/_ t ( 0 ... N )
429 nfrab1
 |-  F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
430 428 429 nfmpt
 |-  F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
431 5 430 nfcxfr
 |-  F/_ t B
432 nfcv
 |-  F/_ t i
433 431 432 nffv
 |-  F/_ t ( B ` i )
434 433 nfel2
 |-  F/ t S e. ( B ` i )
435 3 96 434 nf3an
 |-  F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
436 nfv
 |-  F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
437 435 436 nfim
 |-  F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
438 eleq1
 |-  ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
439 438 3anbi3d
 |-  ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
440 100 breq2d
 |-  ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
441 439 440 imbi12d
 |-  ( 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 ) ) ) )
442 437 441 15 vtoclg1f
 |-  ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
443 427 442 mpcom
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
444 425 443 syld3an2
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
445 420 444 mpd3an3
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
446 445 adantlr
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
447 283 285 286 289 446 fsumlt
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
448 282 447 eqbrtrrd
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
449 126 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
450 157 adantr
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
451 310 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
452 ltmul2
 |-  ( ( ( ( 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 ) ) ) )
453 449 450 451 452 syl3anc
 |-  ( ( 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 ) ) ) )
454 448 453 mpbid
 |-  ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
455 121 128 159 231 454 lttrd
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
456 155 60 syldan
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
457 456 adantlr
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
458 457 recnd
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
459 283 458 fsumcl
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
460 459 addid1d
 |-  ( ( 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 ) ) )
461 0red
 |-  ( ( ph /\ -. L = 1 ) -> 0 e. RR )
462 fzfid
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
463 28 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
464 0zd
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
465 134 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
466 elfzelz
 |-  ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
467 466 adantl
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
468 0red
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
469 125 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
470 466 zred
 |-  ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
471 470 adantl
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
472 1m1e0
 |-  ( 1 - 1 ) = 0
473 122 114 122 367 lesub1dd
 |-  ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
474 472 473 eqbrtrrid
 |-  ( ph -> 0 <_ ( L - 1 ) )
475 474 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
476 simpr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
477 378 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
478 elfz
 |-  ( ( i e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
479 467 477 465 478 syl3anc
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
480 476 479 mpbid
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
481 480 simpld
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
482 468 469 471 475 481 letrd
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
483 elfzle2
 |-  ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
484 483 adantl
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
485 464 465 467 482 484 elfzd
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
486 485 59 syldan
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
487 463 486 remulcld
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
488 487 adantlr
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
489 462 488 fsumrecl
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
490 283 457 fsumrecl
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
491 fzfid
 |-  ( ph -> ( ( L - 1 ) ... N ) e. Fin )
492 180 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
493 492 mul01d
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
494 485 106 syldan
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
495 310 adantr
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
496 lemul2
 |-  ( ( 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 ) ) ) )
497 468 486 495 496 syl3anc
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
498 494 497 mpbid
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
499 493 498 eqbrtrrd
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
500 491 487 499 fsumge0
 |-  ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
501 500 adantr
 |-  ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
502 461 489 490 501 leadd2dd
 |-  ( ( 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 ) ) ) )
503 460 502 eqbrtrrd
 |-  ( ( 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 ) ) ) )
504 156 recnd
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
505 129 180 504 fsummulc2
 |-  ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) )
506 505 adantr
 |-  ( ( 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 ) ) )
507 elfzelz
 |-  ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
508 507 adantl
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
509 508 zred
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
510 315 adantr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
511 125 adantr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
512 simpr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
513 0zd
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
514 133 adantr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
515 elfz
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ ( L - 2 ) e. ZZ ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
516 508 513 514 515 syl3anc
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
517 512 516 mpbid
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
518 517 simprd
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
519 122 137 114 ltsub2d
 |-  ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
520 352 519 mpbii
 |-  ( ph -> ( L - 2 ) < ( L - 1 ) )
521 520 adantr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
522 509 510 511 518 521 lelttrd
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
523 509 511 ltnled
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) )
524 522 523 mpbid
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( L - 1 ) <_ j )
525 524 intnanrd
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( ( L - 1 ) <_ j /\ j <_ N ) )
526 378 adantr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. ZZ )
527 134 adantr
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> N e. ZZ )
528 elfz
 |-  ( ( j e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) )
529 508 526 527 528 syl3anc
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) )
530 525 529 mtbird
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. j e. ( ( L - 1 ) ... N ) )
531 530 ex
 |-  ( ph -> ( j e. ( 0 ... ( L - 2 ) ) -> -. j e. ( ( L - 1 ) ... N ) ) )
532 2 531 ralrimi
 |-  ( ph -> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) )
533 disj
 |-  ( ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) <-> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) )
534 532 533 sylibr
 |-  ( ph -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) )
535 534 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) )
536 149 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( L - 2 ) <_ N )
537 133 377 134 3jca
 |-  ( ph -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) )
538 537 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) )
539 elfz
 |-  ( ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) )
540 538 539 syl
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) )
541 256 536 540 mpbir2and
 |-  ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( 0 ... N ) )
542 fzsplit
 |-  ( ( L - 2 ) e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) )
543 541 542 syl
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) )
544 267 273 274 3eqtrd
 |-  ( ph -> ( ( L - 2 ) + 1 ) = ( L - 1 ) )
545 544 oveq1d
 |-  ( ph -> ( ( ( L - 2 ) + 1 ) ... N ) = ( ( L - 1 ) ... N ) )
546 545 uneq2d
 |-  ( ph -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
547 546 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
548 543 547 eqtrd
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
549 fzfid
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) e. Fin )
550 180 adantr
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> E e. CC )
551 59 recnd
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. CC )
552 550 551 mulcld
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
553 552 adantlr
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
554 535 548 549 553 fsumsplit
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... N ) ( 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 ) ) ) )
555 503 506 554 3brtr4d
 |-  ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
556 120 158 61 3jca
 |-  ( ph -> ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) )
557 556 adantr
 |-  ( ( ph /\ -. L = 1 ) -> ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) )
558 ltletr
 |-  ( ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) -> ( ( ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ 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 ) ) ) )
559 557 558 syl
 |-  ( ( ph /\ -. L = 1 ) -> ( ( ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ 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 ) ) ) )
560 455 555 559 mp2and
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
561 111 560 pm2.61dan
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
562 sumex
 |-  sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V
563 100 oveq2d
 |-  ( t = S -> ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` i ) ` S ) ) )
564 563 sumeq2sdv
 |-  ( t = S -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
565 eqid
 |-  ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) )
566 564 565 fvmptg
 |-  ( ( S e. T /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V ) -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
567 57 562 566 sylancl
 |-  ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
568 561 567 breqtrrd
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) )