Metamath Proof Explorer

Theorem stoweidlem11

Description: This lemma is used to prove that there is a function g as in the proof of BrosowskiDeutsh p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem11.1 
|- ( ph -> N e. NN )
stoweidlem11.2 
|- ( ph -> t e. T )
stoweidlem11.3 
|- ( ph -> j e. ( 1 ... N ) )
stoweidlem11.4 
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
stoweidlem11.5 
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) <_ 1 )
stoweidlem11.6 
|- ( ( ph /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
stoweidlem11.7 
|- ( ph -> E e. RR+ )
stoweidlem11.8 
|- ( ph -> E < ( 1 / 3 ) )
Assertion stoweidlem11 
|- ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) )

Proof

Step Hyp Ref Expression
1 stoweidlem11.1 
 |-  ( ph -> N e. NN )
2 stoweidlem11.2 
 |-  ( ph -> t e. T )
3 stoweidlem11.3 
 |-  ( ph -> j e. ( 1 ... N ) )
4 stoweidlem11.4 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
5 stoweidlem11.5 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) <_ 1 )
6 stoweidlem11.6 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
7 stoweidlem11.7 
 |-  ( ph -> E e. RR+ )
8 stoweidlem11.8 
 |-  ( ph -> E < ( 1 / 3 ) )
9 sumex 
 |-  sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) e. _V
10 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 ) ) )
11 10 fvmpt2 
 |-  ( ( t e. T /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) e. _V ) -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) )
12 2 9 11 sylancl 
 |-  ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) )
13 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
14 7 rpred 
 |-  ( ph -> E e. RR )
15 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> E e. RR )
16 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> t e. T )
17 4 16 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) e. RR )
18 15 17 remulcld 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
19 13 18 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) e. RR )
20 3 elfzelzd 
 |-  ( ph -> j e. ZZ )
21 20 zred 
 |-  ( ph -> j e. RR )
22 14 21 remulcld 
 |-  ( ph -> ( E x. j ) e. RR )
23 1 nnred 
 |-  ( ph -> N e. RR )
24 23 21 resubcld 
 |-  ( ph -> ( N - j ) e. RR )
25 1red 
 |-  ( ph -> 1 e. RR )
26 24 25 readdcld 
 |-  ( ph -> ( ( N - j ) + 1 ) e. RR )
27 14 1 nndivred 
 |-  ( ph -> ( E / N ) e. RR )
28 14 27 remulcld 
 |-  ( ph -> ( E x. ( E / N ) ) e. RR )
29 26 28 remulcld 
 |-  ( ph -> ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) e. RR )
30 22 29 readdcld 
 |-  ( ph -> ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) e. RR )
31 3re 
 |-  3 e. RR
32 31 a1i 
 |-  ( ph -> 3 e. RR )
33 3ne0 
 |-  3 =/= 0
34 33 a1i 
 |-  ( ph -> 3 =/= 0 )
35 32 34 rereccld 
 |-  ( ph -> ( 1 / 3 ) e. RR )
36 21 35 readdcld 
 |-  ( ph -> ( j + ( 1 / 3 ) ) e. RR )
37 36 14 remulcld 
 |-  ( ph -> ( ( j + ( 1 / 3 ) ) x. E ) e. RR )
38 fzfid 
 |-  ( ph -> ( 0 ... ( j - 1 ) ) e. Fin )
39 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> E e. RR )
40 elfzelz 
 |-  ( j e. ( 1 ... N ) -> j e. ZZ )
41 peano2zm 
 |-  ( j e. ZZ -> ( j - 1 ) e. ZZ )
42 3 40 41 3syl 
 |-  ( ph -> ( j - 1 ) e. ZZ )
43 1 nnzd 
 |-  ( ph -> N e. ZZ )
44 21 25 resubcld 
 |-  ( ph -> ( j - 1 ) e. RR )
45 21 lem1d 
 |-  ( ph -> ( j - 1 ) <_ j )
46 elfzuz3 
 |-  ( j e. ( 1 ... N ) -> N e. ( ZZ>= ` j ) )
47 eluzle 
 |-  ( N e. ( ZZ>= ` j ) -> j <_ N )
48 3 46 47 3syl 
 |-  ( ph -> j <_ N )
49 44 21 23 45 48 letrd 
 |-  ( ph -> ( j - 1 ) <_ N )
50 eluz2 
 |-  ( N e. ( ZZ>= ` ( j - 1 ) ) <-> ( ( j - 1 ) e. ZZ /\ N e. ZZ /\ ( j - 1 ) <_ N ) )
51 42 43 49 50 syl3anbrc 
 |-  ( ph -> N e. ( ZZ>= ` ( j - 1 ) ) )
52 fzss2 
 |-  ( N e. ( ZZ>= ` ( j - 1 ) ) -> ( 0 ... ( j - 1 ) ) C_ ( 0 ... N ) )
53 51 52 syl 
 |-  ( ph -> ( 0 ... ( j - 1 ) ) C_ ( 0 ... N ) )
54 53 sselda 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> i e. ( 0 ... N ) )
55 54 17 syldan 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( ( X ` i ) ` t ) e. RR )
56 39 55 remulcld 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
57 38 56 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) e. RR )
58 57 29 readdcld 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) e. RR )
59 21 ltm1d 
 |-  ( ph -> ( j - 1 ) < j )
60 fzdisj 
 |-  ( ( j - 1 ) < j -> ( ( 0 ... ( j - 1 ) ) i^i ( j ... N ) ) = (/) )
61 59 60 syl 
 |-  ( ph -> ( ( 0 ... ( j - 1 ) ) i^i ( j ... N ) ) = (/) )
62 fzssp1 
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
63 1 nncnd 
 |-  ( ph -> N e. CC )
64 1cnd 
 |-  ( ph -> 1 e. CC )
65 63 64 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
66 65 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
67 62 66 sseqtrid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
68 1zzd 
 |-  ( ph -> 1 e. ZZ )
69 fzsubel 
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
70 68 43 20 68 69 syl22anc 
 |-  ( ph -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
71 3 70 mpbid 
 |-  ( ph -> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) )
72 1m1e0 
 |-  ( 1 - 1 ) = 0
73 72 oveq1i 
 |-  ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) )
74 71 73 eleqtrdi 
 |-  ( ph -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
75 67 74 sseldd 
 |-  ( ph -> ( j - 1 ) e. ( 0 ... N ) )
76 fzsplit 
 |-  ( ( j - 1 ) e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... ( j - 1 ) ) u. ( ( ( j - 1 ) + 1 ) ... N ) ) )
77 75 76 syl 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( j - 1 ) ) u. ( ( ( j - 1 ) + 1 ) ... N ) ) )
78 20 zcnd 
 |-  ( ph -> j e. CC )
79 78 64 npcand 
 |-  ( ph -> ( ( j - 1 ) + 1 ) = j )
80 79 oveq1d 
 |-  ( ph -> ( ( ( j - 1 ) + 1 ) ... N ) = ( j ... N ) )
81 80 uneq2d 
 |-  ( ph -> ( ( 0 ... ( j - 1 ) ) u. ( ( ( j - 1 ) + 1 ) ... N ) ) = ( ( 0 ... ( j - 1 ) ) u. ( j ... N ) ) )
82 77 81 eqtrd 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( j - 1 ) ) u. ( j ... N ) ) )
83 7 rpcnd 
 |-  ( ph -> E e. CC )
84 83 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> E e. CC )
85 17 recnd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) e. CC )
86 84 85 mulcld 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. CC )
87 61 82 13 86 fsumsplit 
 |-  ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) = ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + sum_ i e. ( j ... N ) ( E x. ( ( X ` i ) ` t ) ) ) )
88 fzfid 
 |-  ( ph -> ( j ... N ) e. Fin )
89 14 adantr 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> E e. RR )
90 0zd 
 |-  ( ph -> 0 e. ZZ )
91 0red 
 |-  ( ph -> 0 e. RR )
92 0le1 
 |-  0 <_ 1
93 92 a1i 
 |-  ( ph -> 0 <_ 1 )
94 elfzuz 
 |-  ( j e. ( 1 ... N ) -> j e. ( ZZ>= ` 1 ) )
95 3 94 syl 
 |-  ( ph -> j e. ( ZZ>= ` 1 ) )
96 eluz2 
 |-  ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
97 95 96 sylib 
 |-  ( ph -> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
98 97 simp3d 
 |-  ( ph -> 1 <_ j )
99 91 25 21 93 98 letrd 
 |-  ( ph -> 0 <_ j )
100 eluz2 
 |-  ( j e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ j e. ZZ /\ 0 <_ j ) )
101 90 20 99 100 syl3anbrc 
 |-  ( ph -> j e. ( ZZ>= ` 0 ) )
102 fzss1 
 |-  ( j e. ( ZZ>= ` 0 ) -> ( j ... N ) C_ ( 0 ... N ) )
103 101 102 syl 
 |-  ( ph -> ( j ... N ) C_ ( 0 ... N ) )
104 103 sselda 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
105 104 4 syldan 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( X ` i ) : T --> RR )
106 2 adantr 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> t e. T )
107 105 106 ffvelrnd 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) e. RR )
108 89 107 remulcld 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
109 88 108 fsumrecl 
 |-  ( ph -> sum_ i e. ( j ... N ) ( E x. ( ( X ` i ) ` t ) ) e. RR )
110 eluzfz2 
 |-  ( N e. ( ZZ>= ` j ) -> N e. ( j ... N ) )
111 ne0i 
 |-  ( N e. ( j ... N ) -> ( j ... N ) =/= (/) )
112 3 46 110 111 4syl 
 |-  ( ph -> ( j ... N ) =/= (/) )
113 1 adantr 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> N e. NN )
114 89 113 nndivred 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( E / N ) e. RR )
115 89 114 remulcld 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( E x. ( E / N ) ) e. RR )
116 7 rpgt0d 
 |-  ( ph -> 0 < E )
117 116 adantr 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> 0 < E )
118 ltmul2 
 |-  ( ( ( ( X ` i ) ` t ) e. RR /\ ( E / N ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( ( X ` i ) ` t ) < ( E / N ) <-> ( E x. ( ( X ` i ) ` t ) ) < ( E x. ( E / N ) ) ) )
119 107 114 89 117 118 syl112anc 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( ( ( X ` i ) ` t ) < ( E / N ) <-> ( E x. ( ( X ` i ) ` t ) ) < ( E x. ( E / N ) ) ) )
120 6 119 mpbid 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( E x. ( ( X ` i ) ` t ) ) < ( E x. ( E / N ) ) )
121 88 112 108 115 120 fsumlt 
 |-  ( ph -> sum_ i e. ( j ... N ) ( E x. ( ( X ` i ) ` t ) ) < sum_ i e. ( j ... N ) ( E x. ( E / N ) ) )
122 1 nnne0d 
 |-  ( ph -> N =/= 0 )
123 83 63 122 divcld 
 |-  ( ph -> ( E / N ) e. CC )
124 83 123 mulcld 
 |-  ( ph -> ( E x. ( E / N ) ) e. CC )
125 fsumconst 
 |-  ( ( ( j ... N ) e. Fin /\ ( E x. ( E / N ) ) e. CC ) -> sum_ i e. ( j ... N ) ( E x. ( E / N ) ) = ( ( # ` ( j ... N ) ) x. ( E x. ( E / N ) ) ) )
126 88 124 125 syl2anc 
 |-  ( ph -> sum_ i e. ( j ... N ) ( E x. ( E / N ) ) = ( ( # ` ( j ... N ) ) x. ( E x. ( E / N ) ) ) )
127 hashfz 
 |-  ( N e. ( ZZ>= ` j ) -> ( # ` ( j ... N ) ) = ( ( N - j ) + 1 ) )
128 3 46 127 3syl 
 |-  ( ph -> ( # ` ( j ... N ) ) = ( ( N - j ) + 1 ) )
129 128 oveq1d 
 |-  ( ph -> ( ( # ` ( j ... N ) ) x. ( E x. ( E / N ) ) ) = ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) )
130 126 129 eqtrd 
 |-  ( ph -> sum_ i e. ( j ... N ) ( E x. ( E / N ) ) = ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) )
131 121 130 breqtrd 
 |-  ( ph -> sum_ i e. ( j ... N ) ( E x. ( ( X ` i ) ` t ) ) < ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) )
132 109 29 57 131 ltadd2dd 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + sum_ i e. ( j ... N ) ( E x. ( ( X ` i ) ` t ) ) ) < ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) )
133 87 132 eqbrtrd 
 |-  ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) < ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) )
134 54 5 syldan 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( ( X ` i ) ` t ) <_ 1 )
135 1red 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> 1 e. RR )
136 116 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> 0 < E )
137 lemul2 
 |-  ( ( ( ( X ` i ) ` t ) e. RR /\ 1 e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( ( X ` i ) ` t ) <_ 1 <-> ( E x. ( ( X ` i ) ` t ) ) <_ ( E x. 1 ) ) )
138 55 135 39 136 137 syl112anc 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( ( ( X ` i ) ` t ) <_ 1 <-> ( E x. ( ( X ` i ) ` t ) ) <_ ( E x. 1 ) ) )
139 134 138 mpbid 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( E x. ( ( X ` i ) ` t ) ) <_ ( E x. 1 ) )
140 83 mulid1d 
 |-  ( ph -> ( E x. 1 ) = E )
141 140 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( E x. 1 ) = E )
142 139 141 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( E x. ( ( X ` i ) ` t ) ) <_ E )
143 38 56 39 142 fsumle 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) <_ sum_ i e. ( 0 ... ( j - 1 ) ) E )
144 fsumconst 
 |-  ( ( ( 0 ... ( j - 1 ) ) e. Fin /\ E e. CC ) -> sum_ i e. ( 0 ... ( j - 1 ) ) E = ( ( # ` ( 0 ... ( j - 1 ) ) ) x. E ) )
145 38 83 144 syl2anc 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) E = ( ( # ` ( 0 ... ( j - 1 ) ) ) x. E ) )
146 0z 
 |-  0 e. ZZ
147 1e0p1 
 |-  1 = ( 0 + 1 )
148 147 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
149 95 148 eleqtrdi 
 |-  ( ph -> j e. ( ZZ>= ` ( 0 + 1 ) ) )
150 eluzp1m1 
 |-  ( ( 0 e. ZZ /\ j e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
151 146 149 150 sylancr 
 |-  ( ph -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
152 hashfz 
 |-  ( ( j - 1 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( j - 1 ) ) ) = ( ( ( j - 1 ) - 0 ) + 1 ) )
153 151 152 syl 
 |-  ( ph -> ( # ` ( 0 ... ( j - 1 ) ) ) = ( ( ( j - 1 ) - 0 ) + 1 ) )
154 78 64 subcld 
 |-  ( ph -> ( j - 1 ) e. CC )
155 154 subid1d 
 |-  ( ph -> ( ( j - 1 ) - 0 ) = ( j - 1 ) )
156 155 oveq1d 
 |-  ( ph -> ( ( ( j - 1 ) - 0 ) + 1 ) = ( ( j - 1 ) + 1 ) )
157 153 156 79 3eqtrd 
 |-  ( ph -> ( # ` ( 0 ... ( j - 1 ) ) ) = j )
158 157 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ... ( j - 1 ) ) ) x. E ) = ( j x. E ) )
159 78 83 mulcomd 
 |-  ( ph -> ( j x. E ) = ( E x. j ) )
160 145 158 159 3eqtrd 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) E = ( E x. j ) )
161 143 160 breqtrd 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) <_ ( E x. j ) )
162 57 22 29 161 leadd1dd 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) <_ ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) )
163 19 58 30 133 162 ltletrd 
 |-  ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) < ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) )
164 14 14 remulcld 
 |-  ( ph -> ( E x. E ) e. RR )
165 22 164 readdcld 
 |-  ( ph -> ( ( E x. j ) + ( E x. E ) ) e. RR )
166 63 78 subcld 
 |-  ( ph -> ( N - j ) e. CC )
167 166 64 addcld 
 |-  ( ph -> ( ( N - j ) + 1 ) e. CC )
168 83 167 123 mul12d 
 |-  ( ph -> ( E x. ( ( ( N - j ) + 1 ) x. ( E / N ) ) ) = ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) )
169 168 oveq2d 
 |-  ( ph -> ( ( E x. j ) + ( E x. ( ( ( N - j ) + 1 ) x. ( E / N ) ) ) ) = ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) )
170 26 27 remulcld 
 |-  ( ph -> ( ( ( N - j ) + 1 ) x. ( E / N ) ) e. RR )
171 14 170 remulcld 
 |-  ( ph -> ( E x. ( ( ( N - j ) + 1 ) x. ( E / N ) ) ) e. RR )
172 167 83 63 122 div12d 
 |-  ( ph -> ( ( ( N - j ) + 1 ) x. ( E / N ) ) = ( E x. ( ( ( N - j ) + 1 ) / N ) ) )
173 25 21 resubcld 
 |-  ( ph -> ( 1 - j ) e. RR )
174 elfzle1 
 |-  ( j e. ( 1 ... N ) -> 1 <_ j )
175 3 174 syl 
 |-  ( ph -> 1 <_ j )
176 25 21 suble0d 
 |-  ( ph -> ( ( 1 - j ) <_ 0 <-> 1 <_ j ) )
177 175 176 mpbird 
 |-  ( ph -> ( 1 - j ) <_ 0 )
178 173 91 23 177 leadd2dd 
 |-  ( ph -> ( N + ( 1 - j ) ) <_ ( N + 0 ) )
179 63 64 78 addsub12d 
 |-  ( ph -> ( N + ( 1 - j ) ) = ( 1 + ( N - j ) ) )
180 64 166 addcomd 
 |-  ( ph -> ( 1 + ( N - j ) ) = ( ( N - j ) + 1 ) )
181 179 180 eqtrd 
 |-  ( ph -> ( N + ( 1 - j ) ) = ( ( N - j ) + 1 ) )
182 63 addid1d 
 |-  ( ph -> ( N + 0 ) = N )
183 178 181 182 3brtr3d 
 |-  ( ph -> ( ( N - j ) + 1 ) <_ N )
184 1 nngt0d 
 |-  ( ph -> 0 < N )
185 lediv1 
 |-  ( ( ( ( N - j ) + 1 ) e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( N - j ) + 1 ) <_ N <-> ( ( ( N - j ) + 1 ) / N ) <_ ( N / N ) ) )
186 26 23 23 184 185 syl112anc 
 |-  ( ph -> ( ( ( N - j ) + 1 ) <_ N <-> ( ( ( N - j ) + 1 ) / N ) <_ ( N / N ) ) )
187 183 186 mpbid 
 |-  ( ph -> ( ( ( N - j ) + 1 ) / N ) <_ ( N / N ) )
188 63 122 dividd 
 |-  ( ph -> ( N / N ) = 1 )
189 187 188 breqtrd 
 |-  ( ph -> ( ( ( N - j ) + 1 ) / N ) <_ 1 )
190 26 1 nndivred 
 |-  ( ph -> ( ( ( N - j ) + 1 ) / N ) e. RR )
191 190 25 7 lemul2d 
 |-  ( ph -> ( ( ( ( N - j ) + 1 ) / N ) <_ 1 <-> ( E x. ( ( ( N - j ) + 1 ) / N ) ) <_ ( E x. 1 ) ) )
192 189 191 mpbid 
 |-  ( ph -> ( E x. ( ( ( N - j ) + 1 ) / N ) ) <_ ( E x. 1 ) )
193 192 140 breqtrd 
 |-  ( ph -> ( E x. ( ( ( N - j ) + 1 ) / N ) ) <_ E )
194 172 193 eqbrtrd 
 |-  ( ph -> ( ( ( N - j ) + 1 ) x. ( E / N ) ) <_ E )
195 170 14 7 lemul2d 
 |-  ( ph -> ( ( ( ( N - j ) + 1 ) x. ( E / N ) ) <_ E <-> ( E x. ( ( ( N - j ) + 1 ) x. ( E / N ) ) ) <_ ( E x. E ) ) )
196 194 195 mpbid 
 |-  ( ph -> ( E x. ( ( ( N - j ) + 1 ) x. ( E / N ) ) ) <_ ( E x. E ) )
197 171 164 22 196 leadd2dd 
 |-  ( ph -> ( ( E x. j ) + ( E x. ( ( ( N - j ) + 1 ) x. ( E / N ) ) ) ) <_ ( ( E x. j ) + ( E x. E ) ) )
198 169 197 eqbrtrrd 
 |-  ( ph -> ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) <_ ( ( E x. j ) + ( E x. E ) ) )
199 83 78 mulcomd 
 |-  ( ph -> ( E x. j ) = ( j x. E ) )
200 199 oveq1d 
 |-  ( ph -> ( ( E x. j ) + ( E x. E ) ) = ( ( j x. E ) + ( E x. E ) ) )
201 78 83 83 adddird 
 |-  ( ph -> ( ( j + E ) x. E ) = ( ( j x. E ) + ( E x. E ) ) )
202 200 201 eqtr4d 
 |-  ( ph -> ( ( E x. j ) + ( E x. E ) ) = ( ( j + E ) x. E ) )
203 21 14 readdcld 
 |-  ( ph -> ( j + E ) e. RR )
204 14 35 21 8 ltadd2dd 
 |-  ( ph -> ( j + E ) < ( j + ( 1 / 3 ) ) )
205 203 36 7 204 ltmul1dd 
 |-  ( ph -> ( ( j + E ) x. E ) < ( ( j + ( 1 / 3 ) ) x. E ) )
206 202 205 eqbrtrd 
 |-  ( ph -> ( ( E x. j ) + ( E x. E ) ) < ( ( j + ( 1 / 3 ) ) x. E ) )
207 30 165 37 198 206 lelttrd 
 |-  ( ph -> ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) < ( ( j + ( 1 / 3 ) ) x. E ) )
208 19 30 37 163 207 lttrd 
 |-  ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) < ( ( j + ( 1 / 3 ) ) x. E ) )
209 12 208 eqbrtrd 
 |-  ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) )