Metamath Proof Explorer


Theorem stoweidlem34

Description: This lemma proves that for all t in T there is a j as in the proof of BrosowskiDeutsh p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem34.1
|- F/_ t F
stoweidlem34.2
|- F/ j ph
stoweidlem34.3
|- F/ t ph
stoweidlem34.4
|- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
stoweidlem34.5
|- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
stoweidlem34.6
|- J = ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
stoweidlem34.7
|- ( ph -> N e. NN )
stoweidlem34.8
|- ( ph -> T e. _V )
stoweidlem34.9
|- ( ph -> F : T --> RR )
stoweidlem34.10
|- ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )
stoweidlem34.11
|- ( ( ph /\ t e. T ) -> ( F ` t ) < ( ( N - 1 ) x. E ) )
stoweidlem34.12
|- ( ph -> E e. RR+ )
stoweidlem34.13
|- ( ph -> E < ( 1 / 3 ) )
stoweidlem34.14
|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR )
stoweidlem34.15
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) )
stoweidlem34.16
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 )
stoweidlem34.17
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) )
stoweidlem34.18
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) )
Assertion stoweidlem34
|- ( ph -> A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem34.1
 |-  F/_ t F
2 stoweidlem34.2
 |-  F/ j ph
3 stoweidlem34.3
 |-  F/ t ph
4 stoweidlem34.4
 |-  D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
5 stoweidlem34.5
 |-  B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
6 stoweidlem34.6
 |-  J = ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
7 stoweidlem34.7
 |-  ( ph -> N e. NN )
8 stoweidlem34.8
 |-  ( ph -> T e. _V )
9 stoweidlem34.9
 |-  ( ph -> F : T --> RR )
10 stoweidlem34.10
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )
11 stoweidlem34.11
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) < ( ( N - 1 ) x. E ) )
12 stoweidlem34.12
 |-  ( ph -> E e. RR+ )
13 stoweidlem34.13
 |-  ( ph -> E < ( 1 / 3 ) )
14 stoweidlem34.14
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR )
15 stoweidlem34.15
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) )
16 stoweidlem34.16
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 )
17 stoweidlem34.17
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) )
18 stoweidlem34.18
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) )
19 simpr
 |-  ( ( ph /\ t e. T ) -> t e. T )
20 ovex
 |-  ( 1 ... N ) e. _V
21 20 rabex
 |-  { j e. ( 1 ... N ) | t e. ( D ` j ) } e. _V
22 6 fvmpt2
 |-  ( ( t e. T /\ { j e. ( 1 ... N ) | t e. ( D ` j ) } e. _V ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } )
23 19 21 22 sylancl
 |-  ( ( ph /\ t e. T ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } )
24 ssrab2
 |-  { j e. ( 1 ... N ) | t e. ( D ` j ) } C_ ( 1 ... N )
25 23 24 eqsstrdi
 |-  ( ( ph /\ t e. T ) -> ( J ` t ) C_ ( 1 ... N ) )
26 elfznn
 |-  ( x e. ( 1 ... N ) -> x e. NN )
27 26 ssriv
 |-  ( 1 ... N ) C_ NN
28 25 27 sstrdi
 |-  ( ( ph /\ t e. T ) -> ( J ` t ) C_ NN )
29 nnssre
 |-  NN C_ RR
30 28 29 sstrdi
 |-  ( ( ph /\ t e. T ) -> ( J ` t ) C_ RR )
31 7 adantr
 |-  ( ( ph /\ t e. T ) -> N e. NN )
32 nnuz
 |-  NN = ( ZZ>= ` 1 )
33 31 32 eleqtrdi
 |-  ( ( ph /\ t e. T ) -> N e. ( ZZ>= ` 1 ) )
34 eluzfz2
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
35 33 34 syl
 |-  ( ( ph /\ t e. T ) -> N e. ( 1 ... N ) )
36 3re
 |-  3 e. RR
37 3ne0
 |-  3 =/= 0
38 36 37 rereccli
 |-  ( 1 / 3 ) e. RR
39 38 a1i
 |-  ( ( ph /\ t e. T ) -> ( 1 / 3 ) e. RR )
40 1red
 |-  ( ( ph /\ t e. T ) -> 1 e. RR )
41 31 nnred
 |-  ( ( ph /\ t e. T ) -> N e. RR )
42 1lt3
 |-  1 < 3
43 36 42 pm3.2i
 |-  ( 3 e. RR /\ 1 < 3 )
44 recgt1i
 |-  ( ( 3 e. RR /\ 1 < 3 ) -> ( 0 < ( 1 / 3 ) /\ ( 1 / 3 ) < 1 ) )
45 44 simprd
 |-  ( ( 3 e. RR /\ 1 < 3 ) -> ( 1 / 3 ) < 1 )
46 43 45 mp1i
 |-  ( ( ph /\ t e. T ) -> ( 1 / 3 ) < 1 )
47 39 40 41 46 ltsub2dd
 |-  ( ( ph /\ t e. T ) -> ( N - 1 ) < ( N - ( 1 / 3 ) ) )
48 41 40 resubcld
 |-  ( ( ph /\ t e. T ) -> ( N - 1 ) e. RR )
49 41 39 resubcld
 |-  ( ( ph /\ t e. T ) -> ( N - ( 1 / 3 ) ) e. RR )
50 12 rpred
 |-  ( ph -> E e. RR )
51 50 adantr
 |-  ( ( ph /\ t e. T ) -> E e. RR )
52 12 rpgt0d
 |-  ( ph -> 0 < E )
53 52 adantr
 |-  ( ( ph /\ t e. T ) -> 0 < E )
54 ltmul1
 |-  ( ( ( N - 1 ) e. RR /\ ( N - ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( N - 1 ) < ( N - ( 1 / 3 ) ) <-> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) )
55 48 49 51 53 54 syl112anc
 |-  ( ( ph /\ t e. T ) -> ( ( N - 1 ) < ( N - ( 1 / 3 ) ) <-> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) )
56 47 55 mpbid
 |-  ( ( ph /\ t e. T ) -> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) )
57 11 56 jca
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) )
58 9 ffvelrnda
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
59 48 51 remulcld
 |-  ( ( ph /\ t e. T ) -> ( ( N - 1 ) x. E ) e. RR )
60 49 51 remulcld
 |-  ( ( ph /\ t e. T ) -> ( ( N - ( 1 / 3 ) ) x. E ) e. RR )
61 lttr
 |-  ( ( ( F ` t ) e. RR /\ ( ( N - 1 ) x. E ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) -> ( F ` t ) < ( ( N - ( 1 / 3 ) ) x. E ) ) )
62 ltle
 |-  ( ( ( F ` t ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( F ` t ) < ( ( N - ( 1 / 3 ) ) x. E ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
63 62 3adant2
 |-  ( ( ( F ` t ) e. RR /\ ( ( N - 1 ) x. E ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( F ` t ) < ( ( N - ( 1 / 3 ) ) x. E ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
64 61 63 syld
 |-  ( ( ( F ` t ) e. RR /\ ( ( N - 1 ) x. E ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
65 58 59 60 64 syl3anc
 |-  ( ( ph /\ t e. T ) -> ( ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
66 57 65 mpd
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) )
67 rabid
 |-  ( t e. { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
68 19 66 67 sylanbrc
 |-  ( ( ph /\ t e. T ) -> t e. { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
69 oveq1
 |-  ( j = N -> ( j - ( 1 / 3 ) ) = ( N - ( 1 / 3 ) ) )
70 69 oveq1d
 |-  ( j = N -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( N - ( 1 / 3 ) ) x. E ) )
71 70 breq2d
 |-  ( j = N -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
72 71 rabbidv
 |-  ( j = N -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
73 nnnn0
 |-  ( N e. NN -> N e. NN0 )
74 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
75 73 74 eleqtrdi
 |-  ( N e. NN -> N e. ( ZZ>= ` 0 ) )
76 eluzfz2
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
77 7 75 76 3syl
 |-  ( ph -> N e. ( 0 ... N ) )
78 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V )
79 8 78 syl
 |-  ( ph -> { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V )
80 4 72 77 79 fvmptd3
 |-  ( ph -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
81 80 adantr
 |-  ( ( ph /\ t e. T ) -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
82 68 81 eleqtrrd
 |-  ( ( ph /\ t e. T ) -> t e. ( D ` N ) )
83 nfcv
 |-  F/_ j N
84 nfcv
 |-  F/_ j ( 1 ... N )
85 nfmpt1
 |-  F/_ j ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
86 4 85 nfcxfr
 |-  F/_ j D
87 86 83 nffv
 |-  F/_ j ( D ` N )
88 87 nfcri
 |-  F/ j t e. ( D ` N )
89 fveq2
 |-  ( j = N -> ( D ` j ) = ( D ` N ) )
90 89 eleq2d
 |-  ( j = N -> ( t e. ( D ` j ) <-> t e. ( D ` N ) ) )
91 83 84 88 90 elrabf
 |-  ( N e. { j e. ( 1 ... N ) | t e. ( D ` j ) } <-> ( N e. ( 1 ... N ) /\ t e. ( D ` N ) ) )
92 35 82 91 sylanbrc
 |-  ( ( ph /\ t e. T ) -> N e. { j e. ( 1 ... N ) | t e. ( D ` j ) } )
93 92 23 eleqtrrd
 |-  ( ( ph /\ t e. T ) -> N e. ( J ` t ) )
94 ne0i
 |-  ( N e. ( J ` t ) -> ( J ` t ) =/= (/) )
95 93 94 syl
 |-  ( ( ph /\ t e. T ) -> ( J ` t ) =/= (/) )
96 nnwo
 |-  ( ( ( J ` t ) C_ NN /\ ( J ` t ) =/= (/) ) -> E. i e. ( J ` t ) A. k e. ( J ` t ) i <_ k )
97 nfcv
 |-  F/_ i ( J ` t )
98 nfcv
 |-  F/_ j T
99 nfrab1
 |-  F/_ j { j e. ( 1 ... N ) | t e. ( D ` j ) }
100 98 99 nfmpt
 |-  F/_ j ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
101 6 100 nfcxfr
 |-  F/_ j J
102 nfcv
 |-  F/_ j t
103 101 102 nffv
 |-  F/_ j ( J ` t )
104 nfv
 |-  F/ j i <_ k
105 103 104 nfralw
 |-  F/ j A. k e. ( J ` t ) i <_ k
106 nfv
 |-  F/ i A. k e. ( J ` t ) j <_ k
107 breq1
 |-  ( i = j -> ( i <_ k <-> j <_ k ) )
108 107 ralbidv
 |-  ( i = j -> ( A. k e. ( J ` t ) i <_ k <-> A. k e. ( J ` t ) j <_ k ) )
109 97 103 105 106 108 cbvrexfw
 |-  ( E. i e. ( J ` t ) A. k e. ( J ` t ) i <_ k <-> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k )
110 96 109 sylib
 |-  ( ( ( J ` t ) C_ NN /\ ( J ` t ) =/= (/) ) -> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k )
111 28 95 110 syl2anc
 |-  ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k )
112 nfv
 |-  F/ j t e. T
113 2 112 nfan
 |-  F/ j ( ph /\ t e. T )
114 23 eleq2d
 |-  ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) <-> j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } ) )
115 114 biimpa
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } )
116 rabid
 |-  ( j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } <-> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) )
117 115 116 sylib
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) )
118 117 simprd
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> t e. ( D ` j ) )
119 118 adantr
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> t e. ( D ` j ) )
120 simp3
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> t e. ( D ` ( j - 1 ) ) )
121 simp1l
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ph )
122 noel
 |-  -. t e. (/)
123 oveq1
 |-  ( j = 1 -> ( j - 1 ) = ( 1 - 1 ) )
124 1m1e0
 |-  ( 1 - 1 ) = 0
125 123 124 eqtrdi
 |-  ( j = 1 -> ( j - 1 ) = 0 )
126 125 fveq2d
 |-  ( j = 1 -> ( D ` ( j - 1 ) ) = ( D ` 0 ) )
127 36 a1i
 |-  ( ( ph /\ t e. T ) -> 3 e. RR )
128 37 a1i
 |-  ( ( ph /\ t e. T ) -> 3 =/= 0 )
129 40 127 128 redivcld
 |-  ( ( ph /\ t e. T ) -> ( 1 / 3 ) e. RR )
130 129 renegcld
 |-  ( ( ph /\ t e. T ) -> -u ( 1 / 3 ) e. RR )
131 130 51 remulcld
 |-  ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) e. RR )
132 0red
 |-  ( ( ph /\ t e. T ) -> 0 e. RR )
133 3pos
 |-  0 < 3
134 36 133 recgt0ii
 |-  0 < ( 1 / 3 )
135 lt0neg2
 |-  ( ( 1 / 3 ) e. RR -> ( 0 < ( 1 / 3 ) <-> -u ( 1 / 3 ) < 0 ) )
136 38 135 ax-mp
 |-  ( 0 < ( 1 / 3 ) <-> -u ( 1 / 3 ) < 0 )
137 134 136 mpbi
 |-  -u ( 1 / 3 ) < 0
138 ltmul1
 |-  ( ( -u ( 1 / 3 ) e. RR /\ 0 e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( -u ( 1 / 3 ) < 0 <-> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) ) )
139 130 132 51 53 138 syl112anc
 |-  ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) < 0 <-> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) ) )
140 137 139 mpbii
 |-  ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) )
141 mul02lem2
 |-  ( E e. RR -> ( 0 x. E ) = 0 )
142 51 141 syl
 |-  ( ( ph /\ t e. T ) -> ( 0 x. E ) = 0 )
143 140 142 breqtrd
 |-  ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < 0 )
144 131 132 58 143 10 ltletrd
 |-  ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < ( F ` t ) )
145 131 58 ltnled
 |-  ( ( ph /\ t e. T ) -> ( ( -u ( 1 / 3 ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
146 144 145 mpbid
 |-  ( ( ph /\ t e. T ) -> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) )
147 nan
 |-  ( ( ph -> -. ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) <-> ( ( ph /\ t e. T ) -> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
148 146 147 mpbir
 |-  ( ph -> -. ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
149 rabid
 |-  ( t e. { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
150 148 149 sylnibr
 |-  ( ph -> -. t e. { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
151 oveq1
 |-  ( j = 0 -> ( j - ( 1 / 3 ) ) = ( 0 - ( 1 / 3 ) ) )
152 df-neg
 |-  -u ( 1 / 3 ) = ( 0 - ( 1 / 3 ) )
153 151 152 eqtr4di
 |-  ( j = 0 -> ( j - ( 1 / 3 ) ) = -u ( 1 / 3 ) )
154 153 oveq1d
 |-  ( j = 0 -> ( ( j - ( 1 / 3 ) ) x. E ) = ( -u ( 1 / 3 ) x. E ) )
155 154 breq2d
 |-  ( j = 0 -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
156 155 rabbidv
 |-  ( j = 0 -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
157 7 nnnn0d
 |-  ( ph -> N e. NN0 )
158 elnn0uz
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
159 157 158 sylib
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
160 eluzfz1
 |-  ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
161 159 160 syl
 |-  ( ph -> 0 e. ( 0 ... N ) )
162 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V )
163 8 162 syl
 |-  ( ph -> { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V )
164 4 156 161 163 fvmptd3
 |-  ( ph -> ( D ` 0 ) = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
165 150 164 neleqtrrd
 |-  ( ph -> -. t e. ( D ` 0 ) )
166 3 165 alrimi
 |-  ( ph -> A. t -. t e. ( D ` 0 ) )
167 nfcv
 |-  F/_ t ( 0 ... N )
168 nfrab1
 |-  F/_ t { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) }
169 167 168 nfmpt
 |-  F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
170 4 169 nfcxfr
 |-  F/_ t D
171 nfcv
 |-  F/_ t 0
172 170 171 nffv
 |-  F/_ t ( D ` 0 )
173 172 eq0f
 |-  ( ( D ` 0 ) = (/) <-> A. t -. t e. ( D ` 0 ) )
174 166 173 sylibr
 |-  ( ph -> ( D ` 0 ) = (/) )
175 126 174 sylan9eqr
 |-  ( ( ph /\ j = 1 ) -> ( D ` ( j - 1 ) ) = (/) )
176 175 eleq2d
 |-  ( ( ph /\ j = 1 ) -> ( t e. ( D ` ( j - 1 ) ) <-> t e. (/) ) )
177 122 176 mtbiri
 |-  ( ( ph /\ j = 1 ) -> -. t e. ( D ` ( j - 1 ) ) )
178 177 ex
 |-  ( ph -> ( j = 1 -> -. t e. ( D ` ( j - 1 ) ) ) )
179 178 con2d
 |-  ( ph -> ( t e. ( D ` ( j - 1 ) ) -> -. j = 1 ) )
180 121 120 179 sylc
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. j = 1 )
181 simplll
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> ph )
182 114 116 bitrdi
 |-  ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) <-> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) ) )
183 182 simprbda
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. ( 1 ... N ) )
184 7 32 eleqtrdi
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
185 184 adantr
 |-  ( ( ph /\ j e. ( J ` t ) ) -> N e. ( ZZ>= ` 1 ) )
186 elfzp12
 |-  ( N e. ( ZZ>= ` 1 ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) )
187 185 186 syl
 |-  ( ( ph /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) )
188 187 adantlr
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) )
189 183 188 mpbid
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) )
190 189 orcanai
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> j e. ( ( 1 + 1 ) ... N ) )
191 fzssp1
 |-  ( 1 ... ( N - 1 ) ) C_ ( 1 ... ( ( N - 1 ) + 1 ) )
192 7 nncnd
 |-  ( ph -> N e. CC )
193 1cnd
 |-  ( ph -> 1 e. CC )
194 192 193 npcand
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
195 194 oveq2d
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
196 191 195 sseqtrid
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
197 196 adantr
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
198 simpr
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> j e. ( ( 1 + 1 ) ... N ) )
199 1z
 |-  1 e. ZZ
200 zaddcl
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ ) -> ( 1 + 1 ) e. ZZ )
201 199 199 200 mp2an
 |-  ( 1 + 1 ) e. ZZ
202 201 a1i
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( 1 + 1 ) e. ZZ )
203 7 nnzd
 |-  ( ph -> N e. ZZ )
204 203 adantr
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> N e. ZZ )
205 elfzelz
 |-  ( j e. ( ( 1 + 1 ) ... N ) -> j e. ZZ )
206 205 adantl
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> j e. ZZ )
207 1zzd
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> 1 e. ZZ )
208 fzsubel
 |-  ( ( ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( ( 1 + 1 ) ... N ) <-> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
209 202 204 206 207 208 syl22anc
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j e. ( ( 1 + 1 ) ... N ) <-> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
210 198 209 mpbid
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) )
211 ax-1cn
 |-  1 e. CC
212 211 211 pncan3oi
 |-  ( ( 1 + 1 ) - 1 ) = 1
213 212 oveq1i
 |-  ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
214 210 213 eleqtrdi
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( 1 ... ( N - 1 ) ) )
215 197 214 sseldd
 |-  ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( 1 ... N ) )
216 181 190 215 syl2anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> ( j - 1 ) e. ( 1 ... N ) )
217 216 ex
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( -. j = 1 -> ( j - 1 ) e. ( 1 ... N ) ) )
218 217 3adant3
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( -. j = 1 -> ( j - 1 ) e. ( 1 ... N ) ) )
219 180 218 mpd
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. ( 1 ... N ) )
220 fveq2
 |-  ( i = ( j - 1 ) -> ( D ` i ) = ( D ` ( j - 1 ) ) )
221 220 eleq2d
 |-  ( i = ( j - 1 ) -> ( t e. ( D ` i ) <-> t e. ( D ` ( j - 1 ) ) ) )
222 221 elrab3
 |-  ( ( j - 1 ) e. ( 1 ... N ) -> ( ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } <-> t e. ( D ` ( j - 1 ) ) ) )
223 219 222 syl
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } <-> t e. ( D ` ( j - 1 ) ) ) )
224 120 223 mpbird
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } )
225 nfcv
 |-  F/_ i ( 1 ... N )
226 nfv
 |-  F/ i t e. ( D ` j )
227 nfcv
 |-  F/_ j i
228 86 227 nffv
 |-  F/_ j ( D ` i )
229 228 nfcri
 |-  F/ j t e. ( D ` i )
230 fveq2
 |-  ( j = i -> ( D ` j ) = ( D ` i ) )
231 230 eleq2d
 |-  ( j = i -> ( t e. ( D ` j ) <-> t e. ( D ` i ) ) )
232 84 225 226 229 231 cbvrabw
 |-  { j e. ( 1 ... N ) | t e. ( D ` j ) } = { i e. ( 1 ... N ) | t e. ( D ` i ) }
233 224 232 eleqtrrdi
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. { j e. ( 1 ... N ) | t e. ( D ` j ) } )
234 23 3ad2ant1
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } )
235 233 234 eleqtrrd
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. ( J ` t ) )
236 elfzelz
 |-  ( j e. ( 1 ... N ) -> j e. ZZ )
237 zre
 |-  ( j e. ZZ -> j e. RR )
238 183 236 237 3syl
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. RR )
239 238 3adant3
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> j e. RR )
240 peano2rem
 |-  ( j e. RR -> ( j - 1 ) e. RR )
241 ltm1
 |-  ( j e. RR -> ( j - 1 ) < j )
242 241 adantr
 |-  ( ( j e. RR /\ ( j - 1 ) e. RR ) -> ( j - 1 ) < j )
243 ltnle
 |-  ( ( ( j - 1 ) e. RR /\ j e. RR ) -> ( ( j - 1 ) < j <-> -. j <_ ( j - 1 ) ) )
244 243 ancoms
 |-  ( ( j e. RR /\ ( j - 1 ) e. RR ) -> ( ( j - 1 ) < j <-> -. j <_ ( j - 1 ) ) )
245 242 244 mpbid
 |-  ( ( j e. RR /\ ( j - 1 ) e. RR ) -> -. j <_ ( j - 1 ) )
246 239 240 245 syl2anc2
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. j <_ ( j - 1 ) )
247 breq2
 |-  ( k = ( j - 1 ) -> ( j <_ k <-> j <_ ( j - 1 ) ) )
248 247 notbid
 |-  ( k = ( j - 1 ) -> ( -. j <_ k <-> -. j <_ ( j - 1 ) ) )
249 248 rspcev
 |-  ( ( ( j - 1 ) e. ( J ` t ) /\ -. j <_ ( j - 1 ) ) -> E. k e. ( J ` t ) -. j <_ k )
250 235 246 249 syl2anc
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> E. k e. ( J ` t ) -. j <_ k )
251 rexnal
 |-  ( E. k e. ( J ` t ) -. j <_ k <-> -. A. k e. ( J ` t ) j <_ k )
252 250 251 sylib
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. A. k e. ( J ` t ) j <_ k )
253 252 3expia
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( t e. ( D ` ( j - 1 ) ) -> -. A. k e. ( J ` t ) j <_ k ) )
254 253 con2d
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( A. k e. ( J ` t ) j <_ k -> -. t e. ( D ` ( j - 1 ) ) ) )
255 254 imp
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> -. t e. ( D ` ( j - 1 ) ) )
256 119 255 eldifd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
257 256 exp31
 |-  ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) -> ( A. k e. ( J ` t ) j <_ k -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) )
258 113 257 reximdai
 |-  ( ( ph /\ t e. T ) -> ( E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k -> E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) )
259 111 258 mpd
 |-  ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
260 df-rex
 |-  ( E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) <-> E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) )
261 259 260 sylib
 |-  ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) )
262 simprl
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. ( J ` t ) )
263 eldifn
 |-  ( t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) -> -. t e. ( D ` ( j - 1 ) ) )
264 simplr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> t e. T )
265 simpll
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ph )
266 183 adantrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> j e. ( 1 ... N ) )
267 simprr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. t e. ( D ` ( j - 1 ) ) )
268 oveq1
 |-  ( j = k -> ( j - ( 1 / 3 ) ) = ( k - ( 1 / 3 ) ) )
269 268 oveq1d
 |-  ( j = k -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( k - ( 1 / 3 ) ) x. E ) )
270 269 breq2d
 |-  ( j = k -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) ) )
271 270 rabbidv
 |-  ( j = k -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } )
272 271 cbvmptv
 |-  ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) = ( k e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } )
273 4 272 eqtri
 |-  D = ( k e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } )
274 oveq1
 |-  ( k = ( j - 1 ) -> ( k - ( 1 / 3 ) ) = ( ( j - 1 ) - ( 1 / 3 ) ) )
275 274 oveq1d
 |-  ( k = ( j - 1 ) -> ( ( k - ( 1 / 3 ) ) x. E ) = ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) )
276 275 breq2d
 |-  ( k = ( j - 1 ) -> ( ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) )
277 276 rabbidv
 |-  ( k = ( j - 1 ) -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
278 fzssp1
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
279 194 oveq2d
 |-  ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
280 278 279 sseqtrid
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
281 280 adantr
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
282 simpr
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
283 1zzd
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> 1 e. ZZ )
284 203 adantr
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N e. ZZ )
285 236 adantl
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ZZ )
286 fzsubel
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
287 283 284 285 283 286 syl22anc
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
288 282 287 mpbid
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) )
289 124 a1i
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 1 - 1 ) = 0 )
290 289 oveq1d
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) ) )
291 288 290 eleqtrd
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
292 281 291 sseldd
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ... N ) )
293 8 adantr
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> T e. _V )
294 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
295 293 294 syl
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
296 273 277 292 295 fvmptd3
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( D ` ( j - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
297 296 eleq2d
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( t e. ( D ` ( j - 1 ) ) <-> t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) )
298 297 notbid
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( -. t e. ( D ` ( j - 1 ) ) <-> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) )
299 298 biimpa
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ -. t e. ( D ` ( j - 1 ) ) ) -> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
300 265 266 267 299 syl21anc
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
301 rabid
 |-  ( t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) )
302 238 adantrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> j e. RR )
303 recn
 |-  ( j e. RR -> j e. CC )
304 1cnd
 |-  ( j e. RR -> 1 e. CC )
305 1re
 |-  1 e. RR
306 305 36 37 3pm3.2i
 |-  ( 1 e. RR /\ 3 e. RR /\ 3 =/= 0 )
307 redivcl
 |-  ( ( 1 e. RR /\ 3 e. RR /\ 3 =/= 0 ) -> ( 1 / 3 ) e. RR )
308 recn
 |-  ( ( 1 / 3 ) e. RR -> ( 1 / 3 ) e. CC )
309 306 307 308 mp2b
 |-  ( 1 / 3 ) e. CC
310 309 a1i
 |-  ( j e. RR -> ( 1 / 3 ) e. CC )
311 303 304 310 subsub4d
 |-  ( j e. RR -> ( ( j - 1 ) - ( 1 / 3 ) ) = ( j - ( 1 + ( 1 / 3 ) ) ) )
312 3cn
 |-  3 e. CC
313 312 211 312 37 divdiri
 |-  ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
314 3p1e4
 |-  ( 3 + 1 ) = 4
315 314 oveq1i
 |-  ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
316 312 37 dividi
 |-  ( 3 / 3 ) = 1
317 316 oveq1i
 |-  ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
318 313 315 317 3eqtr3i
 |-  ( 4 / 3 ) = ( 1 + ( 1 / 3 ) )
319 318 a1i
 |-  ( j e. RR -> ( 4 / 3 ) = ( 1 + ( 1 / 3 ) ) )
320 319 oveq2d
 |-  ( j e. RR -> ( j - ( 4 / 3 ) ) = ( j - ( 1 + ( 1 / 3 ) ) ) )
321 311 320 eqtr4d
 |-  ( j e. RR -> ( ( j - 1 ) - ( 1 / 3 ) ) = ( j - ( 4 / 3 ) ) )
322 321 oveq1d
 |-  ( j e. RR -> ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) )
323 302 322 syl
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) )
324 323 breq2d
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
325 324 anbi2d
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( t e. T /\ ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) )
326 301 325 syl5bb
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) )
327 300 326 mtbid
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
328 imnan
 |-  ( ( t e. T -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) <-> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
329 327 328 sylibr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( t e. T -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
330 264 329 mpd
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) )
331 263 330 sylanr2
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) )
332 238 adantrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. RR )
333 4re
 |-  4 e. RR
334 333 a1i
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 4 e. RR )
335 36 a1i
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 3 e. RR )
336 37 a1i
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 3 =/= 0 )
337 334 335 336 redivcld
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( 4 / 3 ) e. RR )
338 332 337 resubcld
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( j - ( 4 / 3 ) ) e. RR )
339 50 ad2antrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E e. RR )
340 remulcl
 |-  ( ( ( j - ( 4 / 3 ) ) e. RR /\ E e. RR ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR )
341 340 rexrd
 |-  ( ( ( j - ( 4 / 3 ) ) e. RR /\ E e. RR ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR* )
342 338 339 341 syl2anc
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR* )
343 58 rexrd
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR* )
344 343 adantr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( F ` t ) e. RR* )
345 xrltnle
 |-  ( ( ( ( j - ( 4 / 3 ) ) x. E ) e. RR* /\ ( F ` t ) e. RR* ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
346 342 344 345 syl2anc
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
347 331 346 mpbird
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) )
348 simpl
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ph /\ t e. T ) )
349 simprr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
350 349 eldifad
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. ( D ` j ) )
351 simplll
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ph )
352 183 adantr
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> j e. ( 1 ... N ) )
353 simpr
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> t e. ( D ` j ) )
354 oveq1
 |-  ( k = j -> ( k - ( 1 / 3 ) ) = ( j - ( 1 / 3 ) ) )
355 354 oveq1d
 |-  ( k = j -> ( ( k - ( 1 / 3 ) ) x. E ) = ( ( j - ( 1 / 3 ) ) x. E ) )
356 355 breq2d
 |-  ( k = j -> ( ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
357 356 rabbidv
 |-  ( k = j -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
358 fz1ssfz0
 |-  ( 1 ... N ) C_ ( 0 ... N )
359 358 sseli
 |-  ( j e. ( 1 ... N ) -> j e. ( 0 ... N ) )
360 359 adantl
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 0 ... N ) )
361 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V )
362 293 361 syl
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V )
363 273 357 360 362 fvmptd3
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
364 363 eleq2d
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( t e. ( D ` j ) <-> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) )
365 364 biimpa
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ t e. ( D ` j ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
366 351 352 353 365 syl21anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
367 rabid
 |-  ( t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
368 366 367 sylib
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
369 368 simprd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
370 348 262 350 369 syl21anc
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
371 347 370 jca
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
372 7 ad2antrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> N e. NN )
373 simplr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. T )
374 183 adantrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. ( 1 ... N ) )
375 nfv
 |-  F/ j i e. ( 0 ... N )
376 2 375 nfan
 |-  F/ j ( ph /\ i e. ( 0 ... N ) )
377 nfv
 |-  F/ j ( X ` i ) : T --> RR
378 376 377 nfim
 |-  F/ j ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
379 eleq1w
 |-  ( j = i -> ( j e. ( 0 ... N ) <-> i e. ( 0 ... N ) ) )
380 379 anbi2d
 |-  ( j = i -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ i e. ( 0 ... N ) ) ) )
381 fveq2
 |-  ( j = i -> ( X ` j ) = ( X ` i ) )
382 381 feq1d
 |-  ( j = i -> ( ( X ` j ) : T --> RR <-> ( X ` i ) : T --> RR ) )
383 380 382 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) ) )
384 378 383 14 chvarfv
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
385 384 ad4ant14
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
386 simplll
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ph )
387 simpr
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) )
388 simpllr
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> t e. T )
389 2 375 112 nf3an
 |-  F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. T )
390 nfv
 |-  F/ j ( ( X ` i ) ` t ) <_ 1
391 389 390 nfim
 |-  F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 )
392 379 3anbi2d
 |-  ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. T ) ) )
393 381 fveq1d
 |-  ( j = i -> ( ( X ` j ) ` t ) = ( ( X ` i ) ` t ) )
394 393 breq1d
 |-  ( j = i -> ( ( ( X ` j ) ` t ) <_ 1 <-> ( ( X ` i ) ` t ) <_ 1 ) )
395 392 394 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 ) ) )
396 391 395 16 chvarfv
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 )
397 386 387 388 396 syl3anc
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) <_ 1 )
398 simplll
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ph )
399 0zd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 e. ZZ )
400 elfzel2
 |-  ( i e. ( j ... N ) -> N e. ZZ )
401 400 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> N e. ZZ )
402 elfzelz
 |-  ( i e. ( j ... N ) -> i e. ZZ )
403 402 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. ZZ )
404 0red
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 e. RR )
405 elfzel1
 |-  ( i e. ( j ... N ) -> j e. ZZ )
406 405 zred
 |-  ( i e. ( j ... N ) -> j e. RR )
407 406 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> j e. RR )
408 402 zred
 |-  ( i e. ( j ... N ) -> i e. RR )
409 408 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. RR )
410 0red
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 e. RR )
411 1red
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 1 e. RR )
412 0le1
 |-  0 <_ 1
413 412 a1i
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 <_ 1 )
414 elfzle1
 |-  ( j e. ( 1 ... N ) -> 1 <_ j )
415 183 414 syl
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 1 <_ j )
416 410 411 238 413 415 letrd
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 <_ j )
417 416 adantr
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 <_ j )
418 elfzle1
 |-  ( i e. ( j ... N ) -> j <_ i )
419 418 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> j <_ i )
420 404 407 409 417 419 letrd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 <_ i )
421 elfzle2
 |-  ( i e. ( j ... N ) -> i <_ N )
422 421 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i <_ N )
423 399 401 403 420 422 elfzd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
424 423 adantlrr
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
425 simpll
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ( ph /\ t e. T ) )
426 simplrl
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> j e. ( J ` t ) )
427 simplrr
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
428 427 eldifad
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` j ) )
429 simpr
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> i e. ( j ... N ) )
430 simpl1
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ph /\ t e. T ) )
431 430 simprd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. T )
432 430 58 syl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) e. RR )
433 406 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. RR )
434 38 a1i
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( 1 / 3 ) e. RR )
435 433 434 resubcld
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( j - ( 1 / 3 ) ) e. RR )
436 simpl1l
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ph )
437 436 50 syl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> E e. RR )
438 435 437 remulcld
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) e. RR )
439 408 adantl
 |-  ( ( ph /\ i e. ( j ... N ) ) -> i e. RR )
440 38 a1i
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( 1 / 3 ) e. RR )
441 439 440 resubcld
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( i - ( 1 / 3 ) ) e. RR )
442 50 adantr
 |-  ( ( ph /\ i e. ( j ... N ) ) -> E e. RR )
443 441 442 remulcld
 |-  ( ( ph /\ i e. ( j ... N ) ) -> ( ( i - ( 1 / 3 ) ) x. E ) e. RR )
444 436 443 sylancom
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( i - ( 1 / 3 ) ) x. E ) e. RR )
445 simpl3
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` j ) )
446 simpl2
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. ( J ` t ) )
447 430 446 183 syl2anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. ( 1 ... N ) )
448 436 447 363 syl2anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
449 445 448 eleqtrd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
450 449 367 sylib
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
451 450 simprd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
452 408 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. RR )
453 418 adantl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j <_ i )
454 433 452 434 453 lesub1dd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) )
455 436 441 sylancom
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( i - ( 1 / 3 ) ) e. RR )
456 12 rpregt0d
 |-  ( ph -> ( E e. RR /\ 0 < E ) )
457 436 456 syl
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( E e. RR /\ 0 < E ) )
458 lemul1
 |-  ( ( ( j - ( 1 / 3 ) ) e. RR /\ ( i - ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) <-> ( ( j - ( 1 / 3 ) ) x. E ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) )
459 435 455 457 458 syl3anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) <-> ( ( j - ( 1 / 3 ) ) x. E ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) )
460 454 459 mpbid
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) <_ ( ( i - ( 1 / 3 ) ) x. E ) )
461 432 438 444 451 460 letrd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) )
462 rabid
 |-  ( t e. { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) )
463 431 461 462 sylanbrc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
464 simpr
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. ( j ... N ) )
465 0zd
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> 0 e. ZZ )
466 400 3ad2ant3
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> N e. ZZ )
467 402 3ad2ant3
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> i e. ZZ )
468 465 466 467 3jca
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) )
469 420 422 jca
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> ( 0 <_ i /\ i <_ N ) )
470 469 3impa
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> ( 0 <_ i /\ i <_ N ) )
471 elfz2
 |-  ( i e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) /\ ( 0 <_ i /\ i <_ N ) ) )
472 468 470 471 sylanbrc
 |-  ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
473 430 446 464 472 syl3anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
474 oveq1
 |-  ( j = i -> ( j - ( 1 / 3 ) ) = ( i - ( 1 / 3 ) ) )
475 474 oveq1d
 |-  ( j = i -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( i - ( 1 / 3 ) ) x. E ) )
476 475 breq2d
 |-  ( j = i -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) )
477 476 rabbidv
 |-  ( j = i -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
478 simpr
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) )
479 rabexg
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V )
480 8 479 syl
 |-  ( ph -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V )
481 480 adantr
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V )
482 4 477 478 481 fvmptd3
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( D ` i ) = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
483 436 473 482 syl2anc
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( D ` i ) = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
484 463 483 eleqtrrd
 |-  ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` i ) )
485 425 426 428 429 484 syl31anc
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` i ) )
486 2 375 229 nf3an
 |-  F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) )
487 nfv
 |-  F/ j ( ( X ` i ) ` t ) < ( E / N )
488 486 487 nfim
 |-  F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
489 379 231 3anbi23d
 |-  ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) ) )
490 393 breq1d
 |-  ( j = i -> ( ( ( X ` j ) ` t ) < ( E / N ) <-> ( ( X ` i ) ` t ) < ( E / N ) ) )
491 489 490 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) ) ) )
492 488 491 17 chvarfv
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
493 398 424 485 492 syl3anc
 |-  ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
494 12 ad2antrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E e. RR+ )
495 13 ad2antrr
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E < ( 1 / 3 ) )
496 372 373 374 385 397 493 494 495 stoweidlem11
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) )
497 eleq1w
 |-  ( l = j -> ( l e. ( J ` t ) <-> j e. ( J ` t ) ) )
498 fveq2
 |-  ( l = j -> ( D ` l ) = ( D ` j ) )
499 oveq1
 |-  ( l = j -> ( l - 1 ) = ( j - 1 ) )
500 499 fveq2d
 |-  ( l = j -> ( D ` ( l - 1 ) ) = ( D ` ( j - 1 ) ) )
501 498 500 difeq12d
 |-  ( l = j -> ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) = ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
502 501 eleq2d
 |-  ( l = j -> ( t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) <-> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) )
503 497 502 anbi12d
 |-  ( l = j -> ( ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) <-> ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) )
504 503 anbi2d
 |-  ( l = j -> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) <-> ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) ) )
505 oveq1
 |-  ( l = j -> ( l - ( 4 / 3 ) ) = ( j - ( 4 / 3 ) ) )
506 505 oveq1d
 |-  ( l = j -> ( ( l - ( 4 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) )
507 506 breq1d
 |-  ( l = j -> ( ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) <-> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
508 504 507 imbi12d
 |-  ( l = j -> ( ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) <-> ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
509 eleq1w
 |-  ( s = t -> ( s e. T <-> t e. T ) )
510 509 anbi2d
 |-  ( s = t -> ( ( ph /\ s e. T ) <-> ( ph /\ t e. T ) ) )
511 fveq2
 |-  ( s = t -> ( J ` s ) = ( J ` t ) )
512 511 eleq2d
 |-  ( s = t -> ( l e. ( J ` s ) <-> l e. ( J ` t ) ) )
513 eleq1w
 |-  ( s = t -> ( s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) <-> t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) )
514 512 513 anbi12d
 |-  ( s = t -> ( ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) <-> ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) )
515 510 514 anbi12d
 |-  ( s = t -> ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) <-> ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) ) )
516 fveq2
 |-  ( s = t -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) = ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) )
517 516 breq2d
 |-  ( s = t -> ( ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) <-> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
518 515 517 imbi12d
 |-  ( s = t -> ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) ) <-> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
519 nfv
 |-  F/ j s e. T
520 2 519 nfan
 |-  F/ j ( ph /\ s e. T )
521 nfcv
 |-  F/_ j s
522 101 521 nffv
 |-  F/_ j ( J ` s )
523 522 nfcri
 |-  F/ j l e. ( J ` s )
524 nfcv
 |-  F/_ j l
525 86 524 nffv
 |-  F/_ j ( D ` l )
526 nfcv
 |-  F/_ j ( l - 1 )
527 86 526 nffv
 |-  F/_ j ( D ` ( l - 1 ) )
528 525 527 nfdif
 |-  F/_ j ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
529 528 nfcri
 |-  F/ j s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
530 523 529 nfan
 |-  F/ j ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) )
531 520 530 nfan
 |-  F/ j ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) )
532 nfv
 |-  F/ t s e. T
533 3 532 nfan
 |-  F/ t ( ph /\ s e. T )
534 nfmpt1
 |-  F/_ t ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
535 6 534 nfcxfr
 |-  F/_ t J
536 nfcv
 |-  F/_ t s
537 535 536 nffv
 |-  F/_ t ( J ` s )
538 537 nfcri
 |-  F/ t l e. ( J ` s )
539 nfcv
 |-  F/_ t l
540 170 539 nffv
 |-  F/_ t ( D ` l )
541 nfcv
 |-  F/_ t ( l - 1 )
542 170 541 nffv
 |-  F/_ t ( D ` ( l - 1 ) )
543 540 542 nfdif
 |-  F/_ t ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
544 543 nfcri
 |-  F/ t s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
545 538 544 nfan
 |-  F/ t ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) )
546 533 545 nfan
 |-  F/ t ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) )
547 7 ad2antrr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> N e. NN )
548 8 ad2antrr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> T e. _V )
549 20 rabex
 |-  { j e. ( 1 ... N ) | s e. ( D ` j ) } e. _V
550 nfcv
 |-  F/_ t j
551 170 550 nffv
 |-  F/_ t ( D ` j )
552 551 nfcri
 |-  F/ t s e. ( D ` j )
553 nfcv
 |-  F/_ t ( 1 ... N )
554 552 553 nfrabw
 |-  F/_ t { j e. ( 1 ... N ) | s e. ( D ` j ) }
555 eleq1w
 |-  ( t = s -> ( t e. ( D ` j ) <-> s e. ( D ` j ) ) )
556 555 rabbidv
 |-  ( t = s -> { j e. ( 1 ... N ) | t e. ( D ` j ) } = { j e. ( 1 ... N ) | s e. ( D ` j ) } )
557 536 554 556 6 fvmptf
 |-  ( ( s e. T /\ { j e. ( 1 ... N ) | s e. ( D ` j ) } e. _V ) -> ( J ` s ) = { j e. ( 1 ... N ) | s e. ( D ` j ) } )
558 549 557 mpan2
 |-  ( s e. T -> ( J ` s ) = { j e. ( 1 ... N ) | s e. ( D ` j ) } )
559 558 eleq2d
 |-  ( s e. T -> ( l e. ( J ` s ) <-> l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } ) )
560 559 biimpa
 |-  ( ( s e. T /\ l e. ( J ` s ) ) -> l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } )
561 525 nfcri
 |-  F/ j s e. ( D ` l )
562 fveq2
 |-  ( j = l -> ( D ` j ) = ( D ` l ) )
563 562 eleq2d
 |-  ( j = l -> ( s e. ( D ` j ) <-> s e. ( D ` l ) ) )
564 524 84 561 563 elrabf
 |-  ( l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } <-> ( l e. ( 1 ... N ) /\ s e. ( D ` l ) ) )
565 560 564 sylib
 |-  ( ( s e. T /\ l e. ( J ` s ) ) -> ( l e. ( 1 ... N ) /\ s e. ( D ` l ) ) )
566 565 simpld
 |-  ( ( s e. T /\ l e. ( J ` s ) ) -> l e. ( 1 ... N ) )
567 566 ad2ant2lr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> l e. ( 1 ... N ) )
568 simprr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) )
569 9 ad2antrr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> F : T --> RR )
570 12 ad2antrr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> E e. RR+ )
571 13 ad2antrr
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> E < ( 1 / 3 ) )
572 384 ad4ant14
 |-  ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
573 simp1ll
 |-  ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. T ) -> ph )
574 nfv
 |-  F/ j 0 <_ ( ( X ` i ) ` t )
575 389 574 nfim
 |-  F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
576 393 breq2d
 |-  ( j = i -> ( 0 <_ ( ( X ` j ) ` t ) <-> 0 <_ ( ( X ` i ) ` t ) ) )
577 392 576 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) ) ) )
578 575 577 15 chvarfv
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
579 573 578 syld3an1
 |-  ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
580 simp1ll
 |-  ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ph )
581 nfmpt1
 |-  F/_ j ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
582 5 581 nfcxfr
 |-  F/_ j B
583 582 227 nffv
 |-  F/_ j ( B ` i )
584 583 nfcri
 |-  F/ j t e. ( B ` i )
585 2 375 584 nf3an
 |-  F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) )
586 nfv
 |-  F/ j ( 1 - ( E / N ) ) < ( ( X ` i ) ` t )
587 585 586 nfim
 |-  F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
588 fveq2
 |-  ( j = i -> ( B ` j ) = ( B ` i ) )
589 588 eleq2d
 |-  ( j = i -> ( t e. ( B ` j ) <-> t e. ( B ` i ) ) )
590 379 589 3anbi23d
 |-  ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) ) )
591 393 breq2d
 |-  ( j = i -> ( ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) )
592 590 591 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) ) )
593 587 592 18 chvarfv
 |-  ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
594 580 593 syld3an1
 |-  ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
595 1 531 546 4 5 547 548 567 568 569 570 571 572 579 594 stoweidlem26
 |-  ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) )
596 518 595 vtoclg
 |-  ( t e. T -> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
597 596 ad2antlr
 |-  ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
598 597 pm2.43i
 |-  ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) )
599 508 598 vtoclg
 |-  ( j e. ( J ` t ) -> ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
600 599 ad2antrl
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
601 600 pm2.43i
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) )
602 496 601 jca
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) )
603 262 371 602 3jca
 |-  ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
604 603 ex
 |-  ( ( ph /\ t e. T ) -> ( ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) -> ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
605 113 604 eximd
 |-  ( ( ph /\ t e. T ) -> ( E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) -> E. j ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
606 261 605 mpd
 |-  ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
607 3anass
 |-  ( ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) <-> ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
608 607 exbii
 |-  ( E. j ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) <-> E. j ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
609 606 608 sylib
 |-  ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
610 df-rex
 |-  ( E. j e. ( J ` t ) ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) <-> E. j ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
611 609 610 sylibr
 |-  ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
612 nfcv
 |-  F/_ j RR
613 103 612 ssrexf
 |-  ( ( J ` t ) C_ RR -> ( E. j e. ( J ` t ) ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) -> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
614 30 611 613 sylc
 |-  ( ( ph /\ t e. T ) -> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
615 614 ex
 |-  ( ph -> ( t e. T -> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) )
616 3 615 ralrimi
 |-  ( ph -> A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )