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 112 syl 
 |-  ( 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 112 syl 
 |-  ( ( 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 193 simpld 
 |-  ( ph -> 1 <_ L )
367 139 122 readdcld 
 |-  ( ph -> ( N + 1 ) e. RR )
368 139 lep1d 
 |-  ( ph -> N <_ ( N + 1 ) )
369 114 139 367 194 368 letrd 
 |-  ( ph -> L <_ ( N + 1 ) )
370 134 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
371 elfz 
 |-  ( ( L e. ZZ /\ 1 e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
372 130 190 370 371 syl3anc 
 |-  ( ph -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
373 366 369 372 mpbir2and 
 |-  ( ph -> L e. ( 1 ... ( N + 1 ) ) )
374 144 179 npcand 
 |-  ( ph -> ( ( L - 1 ) + 1 ) = L )
375 0p1e1 
 |-  ( 0 + 1 ) = 1
376 375 a1i 
 |-  ( ph -> ( 0 + 1 ) = 1 )
377 376 oveq1d 
 |-  ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
378 373 374 377 3eltr4d 
 |-  ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
379 0zd 
 |-  ( ph -> 0 e. ZZ )
380 130 190 zsubcld 
 |-  ( ph -> ( L - 1 ) e. ZZ )
381 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 ) ) ) )
382 379 134 380 190 381 syl22anc 
 |-  ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
383 378 382 mpbird 
 |-  ( ph -> ( L - 1 ) e. ( 0 ... N ) )
384 rabexg 
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
385 7 384 syl 
 |-  ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
386 4 365 383 385 fvmptd3 
 |-  ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
387 361 386 neleqtrd 
 |-  ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
388 nfcv 
 |-  F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
389 49 50 388 nfbr 
 |-  F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
390 53 breq1d 
 |-  ( t = S -> ( ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
391 47 48 389 390 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 ) ) )
392 387 391 sylnib 
 |-  ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
393 ianor 
 |-  ( -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
394 392 393 sylib 
 |-  ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
395 olc 
 |-  ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
396 395 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 ) ) ) )
397 57 394 396 syl2anc 
 |-  ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) )
398 orcom 
 |-  ( ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) )
399 398 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 ) ) )
400 397 399 sylib 
 |-  ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) )
401 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 ) ) )
402 400 401 sylibr 
 |-  ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
403 320 318 ltnled 
 |-  ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
404 402 403 mpbird 
 |-  ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
405 317 320 318 360 404 lttrd 
 |-  ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
406 317 318 405 ltled 
 |-  ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
407 406 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
408 297 302 306 314 407 letrd 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
409 nfcv 
 |-  F/_ t ( ( i + ( 1 / 3 ) ) x. E )
410 409 50 49 nfbr 
 |-  F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
411 53 breq2d 
 |-  ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
412 47 48 410 411 elrabf 
 |-  ( S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } <-> ( S e. T /\ ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
413 290 408 412 sylanbrc 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
414 oveq1 
 |-  ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
415 414 oveq1d 
 |-  ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
416 415 breq1d 
 |-  ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
417 416 rabbidv 
 |-  ( j = i -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
418 rabexg 
 |-  ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
419 7 418 syl 
 |-  ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
420 419 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
421 5 417 155 420 fvmptd3 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
422 413 421 eleqtrrd 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
423 150 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
424 423 151 sylibr 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) )
425 424 153 syl 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
426 simp2 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
427 425 426 sseldd 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
428 elex 
 |-  ( S e. ( B ` i ) -> S e. _V )
429 428 3ad2ant3 
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
430 nfcv 
 |-  F/_ t ( 0 ... N )
431 nfrab1 
 |-  F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
432 430 431 nfmpt 
 |-  F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
433 5 432 nfcxfr 
 |-  F/_ t B
434 nfcv 
 |-  F/_ t i
435 433 434 nffv 
 |-  F/_ t ( B ` i )
436 435 nfel2 
 |-  F/ t S e. ( B ` i )
437 3 96 436 nf3an 
 |-  F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
438 nfv 
 |-  F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
439 437 438 nfim 
 |-  F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
440 eleq1 
 |-  ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
441 440 3anbi3d 
 |-  ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
442 100 breq2d 
 |-  ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
443 441 442 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 ) ) ) )
444 439 443 15 vtoclg1f 
 |-  ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
445 429 444 mpcom 
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
446 427 445 syld3an2 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
447 422 446 mpd3an3 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
448 447 adantlr 
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
449 283 285 286 289 448 fsumlt 
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
450 282 449 eqbrtrrd 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
451 126 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
452 157 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
453 310 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
454 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 ) ) ) )
455 451 452 453 454 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 ) ) ) )
456 450 455 mpbid 
 |-  ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
457 121 128 159 231 456 lttrd 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
458 155 60 syldan 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
459 458 adantlr 
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
460 459 recnd 
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
461 283 460 fsumcl 
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
462 461 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 ) ) )
463 0red 
 |-  ( ( ph /\ -. L = 1 ) -> 0 e. RR )
464 fzfid 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
465 28 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
466 0red 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
467 125 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
468 elfzelz 
 |-  ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
469 468 zred 
 |-  ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
470 469 adantl 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
471 1m1e0 
 |-  ( 1 - 1 ) = 0
472 122 114 122 366 lesub1dd 
 |-  ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
473 471 472 eqbrtrrid 
 |-  ( ph -> 0 <_ ( L - 1 ) )
474 473 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
475 simpr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
476 468 adantl 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
477 380 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
478 134 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
479 elfz 
 |-  ( ( i e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
480 476 477 478 479 syl3anc 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
481 475 480 mpbid 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
482 481 simpld 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
483 466 467 470 474 482 letrd 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
484 elfzle2 
 |-  ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
485 484 adantl 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
486 0zd 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
487 elfz 
 |-  ( ( i e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
488 476 486 478 487 syl3anc 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
489 483 485 488 mpbir2and 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
490 489 59 syldan 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
491 465 490 remulcld 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
492 491 adantlr 
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
493 464 492 fsumrecl 
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
494 283 459 fsumrecl 
 |-  ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
495 fzfid 
 |-  ( ph -> ( ( L - 1 ) ... N ) e. Fin )
496 180 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
497 496 mul01d 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
498 489 106 syldan 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
499 310 adantr 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
500 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 ) ) ) )
501 466 490 499 500 syl3anc 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
502 498 501 mpbid 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
503 497 502 eqbrtrrd 
 |-  ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
504 495 491 503 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
505 504 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
506 463 493 494 505 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 ) ) ) )
507 462 506 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 ) ) ) )
508 156 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
509 129 180 508 fsummulc2 
 |-  ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) )
510 509 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 ) ) )
511 elfzelz 
 |-  ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
512 511 adantl 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
513 512 zred 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
514 315 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
515 125 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
516 simpr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
517 0zd 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
518 133 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
519 elfz 
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ ( L - 2 ) e. ZZ ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
520 512 517 518 519 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
521 516 520 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
522 521 simprd 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
523 122 137 114 ltsub2d 
 |-  ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
524 352 523 mpbii 
 |-  ( ph -> ( L - 2 ) < ( L - 1 ) )
525 524 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
526 513 514 515 522 525 lelttrd 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
527 513 515 ltnled 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) )
528 526 527 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( L - 1 ) <_ j )
529 528 intnanrd 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( ( L - 1 ) <_ j /\ j <_ N ) )
530 380 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. ZZ )
531 134 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> N e. ZZ )
532 elfz 
 |-  ( ( j e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) )
533 512 530 531 532 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) )
534 529 533 mtbird 
 |-  ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. j e. ( ( L - 1 ) ... N ) )
535 534 ex 
 |-  ( ph -> ( j e. ( 0 ... ( L - 2 ) ) -> -. j e. ( ( L - 1 ) ... N ) ) )
536 2 535 ralrimi 
 |-  ( ph -> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) )
537 disj 
 |-  ( ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) <-> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) )
538 536 537 sylibr 
 |-  ( ph -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) )
539 538 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) )
540 149 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> ( L - 2 ) <_ N )
541 133 379 134 3jca 
 |-  ( ph -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) )
542 541 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) )
543 elfz 
 |-  ( ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) )
544 542 543 syl 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) )
545 256 540 544 mpbir2and 
 |-  ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( 0 ... N ) )
546 fzsplit 
 |-  ( ( L - 2 ) e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) )
547 545 546 syl 
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) )
548 267 273 274 3eqtrd 
 |-  ( ph -> ( ( L - 2 ) + 1 ) = ( L - 1 ) )
549 548 oveq1d 
 |-  ( ph -> ( ( ( L - 2 ) + 1 ) ... N ) = ( ( L - 1 ) ... N ) )
550 549 uneq2d 
 |-  ( ph -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
551 550 adantr 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
552 547 551 eqtrd 
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
553 fzfid 
 |-  ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) e. Fin )
554 180 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> E e. CC )
555 59 recnd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. CC )
556 554 555 mulcld 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
557 556 adantlr 
 |-  ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
558 539 552 553 557 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 ) ) ) )
559 507 510 558 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 ) ) )
560 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 ) )
561 560 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 ) )
562 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 ) ) ) )
563 561 562 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 ) ) ) )
564 457 559 563 mp2and 
 |-  ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
565 111 564 pm2.61dan 
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
566 sumex 
 |-  sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V
567 100 oveq2d 
 |-  ( t = S -> ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` i ) ` S ) ) )
568 567 sumeq2sdv 
 |-  ( t = S -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
569 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 ) ) )
570 568 569 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 ) ) )
571 57 566 570 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 ) ) )
572 565 571 breqtrrd 
 |-  ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) )