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 ffvelcdmda 
 |-  ( ( 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 bitrid 
 |-  ( ( ( 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 ) ) ) )