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 represent 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 sselid 
 |-  ( 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 ffvelcdmd 
 |-  ( ( 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 mulridd 
 |-  ( 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 mullidd 
 |-  ( 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 ffvelcdm 
 |-  ( ( 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 ffvelcdmd 
 |-  ( 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 addrid 
 |-  ( 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 addridd 
 |-  ( ( 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 ) )