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 elfzuz 
 |-  ( j e. ( 1 ... N ) -> j e. ( ZZ>= ` 1 ) )
21 3 20 syl 
 |-  ( ph -> j e. ( ZZ>= ` 1 ) )
22 eluz2 
 |-  ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
23 21 22 sylib 
 |-  ( ph -> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
24 23 simp2d 
 |-  ( ph -> j e. ZZ )
25 24 zred 
 |-  ( ph -> j e. RR )
26 14 25 remulcld 
 |-  ( ph -> ( E x. j ) e. RR )
27 1 nnred 
 |-  ( ph -> N e. RR )
28 27 25 resubcld 
 |-  ( ph -> ( N - j ) e. RR )
29 1red 
 |-  ( ph -> 1 e. RR )
30 28 29 readdcld 
 |-  ( ph -> ( ( N - j ) + 1 ) e. RR )
31 14 1 nndivred 
 |-  ( ph -> ( E / N ) e. RR )
32 14 31 remulcld 
 |-  ( ph -> ( E x. ( E / N ) ) e. RR )
33 30 32 remulcld 
 |-  ( ph -> ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) e. RR )
34 26 33 readdcld 
 |-  ( ph -> ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) e. RR )
35 3re 
 |-  3 e. RR
36 35 a1i 
 |-  ( ph -> 3 e. RR )
37 3ne0 
 |-  3 =/= 0
38 37 a1i 
 |-  ( ph -> 3 =/= 0 )
39 36 38 rereccld 
 |-  ( ph -> ( 1 / 3 ) e. RR )
40 25 39 readdcld 
 |-  ( ph -> ( j + ( 1 / 3 ) ) e. RR )
41 40 14 remulcld 
 |-  ( ph -> ( ( j + ( 1 / 3 ) ) x. E ) e. RR )
42 fzfid 
 |-  ( ph -> ( 0 ... ( j - 1 ) ) e. Fin )
43 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> E e. RR )
44 elfzelz 
 |-  ( j e. ( 1 ... N ) -> j e. ZZ )
45 peano2zm 
 |-  ( j e. ZZ -> ( j - 1 ) e. ZZ )
46 3 44 45 3syl 
 |-  ( ph -> ( j - 1 ) e. ZZ )
47 1 nnzd 
 |-  ( ph -> N e. ZZ )
48 25 29 resubcld 
 |-  ( ph -> ( j - 1 ) e. RR )
49 25 lem1d 
 |-  ( ph -> ( j - 1 ) <_ j )
50 elfzuz3 
 |-  ( j e. ( 1 ... N ) -> N e. ( ZZ>= ` j ) )
51 eluzle 
 |-  ( N e. ( ZZ>= ` j ) -> j <_ N )
52 3 50 51 3syl 
 |-  ( ph -> j <_ N )
53 48 25 27 49 52 letrd 
 |-  ( ph -> ( j - 1 ) <_ N )
54 eluz2 
 |-  ( N e. ( ZZ>= ` ( j - 1 ) ) <-> ( ( j - 1 ) e. ZZ /\ N e. ZZ /\ ( j - 1 ) <_ N ) )
55 46 47 53 54 syl3anbrc 
 |-  ( ph -> N e. ( ZZ>= ` ( j - 1 ) ) )
56 fzss2 
 |-  ( N e. ( ZZ>= ` ( j - 1 ) ) -> ( 0 ... ( j - 1 ) ) C_ ( 0 ... N ) )
57 55 56 syl 
 |-  ( ph -> ( 0 ... ( j - 1 ) ) C_ ( 0 ... N ) )
58 57 sselda 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> i e. ( 0 ... N ) )
59 58 17 syldan 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( ( X ` i ) ` t ) e. RR )
60 43 59 remulcld 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
61 42 60 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) e. RR )
62 61 33 readdcld 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( j - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) e. RR )
63 25 ltm1d 
 |-  ( ph -> ( j - 1 ) < j )
64 fzdisj 
 |-  ( ( j - 1 ) < j -> ( ( 0 ... ( j - 1 ) ) i^i ( j ... N ) ) = (/) )
65 63 64 syl 
 |-  ( ph -> ( ( 0 ... ( j - 1 ) ) i^i ( j ... N ) ) = (/) )
66 fzssp1 
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
67 1 nncnd 
 |-  ( ph -> N e. CC )
68 1cnd 
 |-  ( ph -> 1 e. CC )
69 67 68 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
70 69 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
71 66 70 sseqtrid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
72 1zzd 
 |-  ( ph -> 1 e. ZZ )
73 fzsubel 
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
74 72 47 24 72 73 syl22anc 
 |-  ( ph -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
75 3 74 mpbid 
 |-  ( ph -> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) )
76 1m1e0 
 |-  ( 1 - 1 ) = 0
77 76 oveq1i 
 |-  ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) )
78 75 77 eleqtrdi 
 |-  ( ph -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
79 71 78 sseldd 
 |-  ( ph -> ( j - 1 ) e. ( 0 ... N ) )
80 fzsplit 
 |-  ( ( j - 1 ) e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... ( j - 1 ) ) u. ( ( ( j - 1 ) + 1 ) ... N ) ) )
81 79 80 syl 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( j - 1 ) ) u. ( ( ( j - 1 ) + 1 ) ... N ) ) )
82 24 zcnd 
 |-  ( ph -> j e. CC )
83 82 68 npcand 
 |-  ( ph -> ( ( j - 1 ) + 1 ) = j )
84 83 oveq1d 
 |-  ( ph -> ( ( ( j - 1 ) + 1 ) ... N ) = ( j ... N ) )
85 84 uneq2d 
 |-  ( ph -> ( ( 0 ... ( j - 1 ) ) u. ( ( ( j - 1 ) + 1 ) ... N ) ) = ( ( 0 ... ( j - 1 ) ) u. ( j ... N ) ) )
86 81 85 eqtrd 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( j - 1 ) ) u. ( j ... N ) ) )
87 7 rpcnd 
 |-  ( ph -> E e. CC )
88 87 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> E e. CC )
89 17 recnd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) e. CC )
90 88 89 mulcld 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. CC )
91 65 86 13 90 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 ) ) ) )
92 fzfid 
 |-  ( ph -> ( j ... N ) e. Fin )
93 14 adantr 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> E e. RR )
94 0zd 
 |-  ( ph -> 0 e. ZZ )
95 0red 
 |-  ( ph -> 0 e. RR )
96 0le1 
 |-  0 <_ 1
97 96 a1i 
 |-  ( ph -> 0 <_ 1 )
98 23 simp3d 
 |-  ( ph -> 1 <_ j )
99 95 29 25 97 98 letrd 
 |-  ( ph -> 0 <_ j )
100 eluz2 
 |-  ( j e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ j e. ZZ /\ 0 <_ j ) )
101 94 24 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 93 107 remulcld 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
109 92 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 50 110 111 4syl 
 |-  ( ph -> ( j ... N ) =/= (/) )
113 1 adantr 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> N e. NN )
114 93 113 nndivred 
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( E / N ) e. RR )
115 93 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 93 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 92 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 87 67 122 divcld 
 |-  ( ph -> ( E / N ) e. CC )
124 87 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 92 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 50 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 33 61 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 91 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 58 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 59 135 43 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 87 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 42 60 43 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 42 87 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 21 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 82 68 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 83 3eqtrd 
 |-  ( ph -> ( # ` ( 0 ... ( j - 1 ) ) ) = j )
158 157 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ... ( j - 1 ) ) ) x. E ) = ( j x. E ) )
159 82 87 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 61 26 33 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 62 34 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 26 164 readdcld 
 |-  ( ph -> ( ( E x. j ) + ( E x. E ) ) e. RR )
166 67 82 subcld 
 |-  ( ph -> ( N - j ) e. CC )
167 166 68 addcld 
 |-  ( ph -> ( ( N - j ) + 1 ) e. CC )
168 87 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 30 31 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 87 67 122 div12d 
 |-  ( ph -> ( ( ( N - j ) + 1 ) x. ( E / N ) ) = ( E x. ( ( ( N - j ) + 1 ) / N ) ) )
173 29 25 resubcld 
 |-  ( ph -> ( 1 - j ) e. RR )
174 elfzle1 
 |-  ( j e. ( 1 ... N ) -> 1 <_ j )
175 3 174 syl 
 |-  ( ph -> 1 <_ j )
176 29 25 suble0d 
 |-  ( ph -> ( ( 1 - j ) <_ 0 <-> 1 <_ j ) )
177 175 176 mpbird 
 |-  ( ph -> ( 1 - j ) <_ 0 )
178 173 95 27 177 leadd2dd 
 |-  ( ph -> ( N + ( 1 - j ) ) <_ ( N + 0 ) )
179 67 68 82 addsub12d 
 |-  ( ph -> ( N + ( 1 - j ) ) = ( 1 + ( N - j ) ) )
180 68 166 addcomd 
 |-  ( ph -> ( 1 + ( N - j ) ) = ( ( N - j ) + 1 ) )
181 179 180 eqtrd 
 |-  ( ph -> ( N + ( 1 - j ) ) = ( ( N - j ) + 1 ) )
182 67 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 30 27 27 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 67 122 dividd 
 |-  ( ph -> ( N / N ) = 1 )
189 187 188 breqtrd 
 |-  ( ph -> ( ( ( N - j ) + 1 ) / N ) <_ 1 )
190 30 1 nndivred 
 |-  ( ph -> ( ( ( N - j ) + 1 ) / N ) e. RR )
191 190 29 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 26 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 87 82 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 82 87 87 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 25 14 readdcld 
 |-  ( ph -> ( j + E ) e. RR )
204 14 39 25 8 ltadd2dd 
 |-  ( ph -> ( j + E ) < ( j + ( 1 / 3 ) ) )
205 203 40 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 34 165 41 198 206 lelttrd 
 |-  ( ph -> ( ( E x. j ) + ( ( ( N - j ) + 1 ) x. ( E x. ( E / N ) ) ) ) < ( ( j + ( 1 / 3 ) ) x. E ) )
208 19 34 41 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 ) )