Theorem stoweidlem34 40251

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
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 ) ) ) )

Distinct variable groups:   i, j, t, E   D, i   i, J   i, N, j, t   T, i, j, t   ph, i   j, F   j, X, t

Allowed substitution hints:   ph( t, j)   B( t, i, j)   D( t, j)   F( t, i)   J( t, j)   X( i)

Proof of Theorem stoweidlem34

Dummy variables x k l s are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem34.3	. 2 |- F/ t ph
2		simpr 477	. . . . . . . 8 |- ( ( ph /\ t e. T ) -> t e. T )
3		ovex 6678	. . . . . . . . 9 |- ( 1 ... N ) e. _V
4	3	rabex 4813	. . . . . . . 8 |- { j e. ( 1 ... N ) | t e. ( D ` j ) } e. _V
5		stoweidlem34.6	. . . . . . . . 9 |- J = ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
6	5	fvmpt2 6291	. . . . . . . 8 |- ( ( t e. T /\ { j e. ( 1 ... N ) | t e. ( D ` j ) } e. _V ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } )
7	2, 4, 6	sylancl 694	. . . . . . 7 |- ( ( ph /\ t e. T ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } )
8		ssrab2 3687	. . . . . . 7 |- { j e. ( 1 ... N ) | t e. ( D ` j ) } C_ ( 1 ... N )
9	7, 8	syl6eqss 3655	. . . . . 6 |- ( ( ph /\ t e. T ) -> ( J ` t ) C_ ( 1 ... N ) )
10		elfznn 12370	. . . . . . 7 |- ( x e. ( 1 ... N ) -> x e. NN )
11	10	ssriv 3607	. . . . . 6 |- ( 1 ... N ) C_ NN
12	9, 11	syl6ss 3615	. . . . 5 |- ( ( ph /\ t e. T ) -> ( J ` t ) C_ NN )
13		nnssre 11024	. . . . 5 |- NN C_ RR
14	12, 13	syl6ss 3615	. . . 4 |- ( ( ph /\ t e. T ) -> ( J ` t ) C_ RR )
15		stoweidlem34.7	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. NN )
16	15	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ t e. T ) -> N e. NN )
17		nnuz 11723	. . . . . . . . . . . . . . 15 |- NN = ( ZZ>= ` 1 )
18	16, 17	syl6eleq 2711	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. T ) -> N e. ( ZZ>= ` 1 ) )
19		eluzfz2 12349	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
20	18, 19	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. T ) -> N e. ( 1 ... N ) )
21		stoweidlem34.11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. T ) -> ( F ` t ) < ( ( N - 1 ) x. E ) )
22		3re 11094	. . . . . . . . . . . . . . . . . . . . 21 |- 3 e. RR
23		3ne0 11115	. . . . . . . . . . . . . . . . . . . . 21 |- 3 =/= 0
24	22, 23	rereccli 10790	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 / 3 ) e. RR
25	24	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> ( 1 / 3 ) e. RR )
26		1red 10055	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> 1 e. RR )
27	16	nnred 11035	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> N e. RR )
28		1lt3 11196	. . . . . . . . . . . . . . . . . . . . 21 |- 1 < 3
29	22, 28	pm3.2i 471	. . . . . . . . . . . . . . . . . . . 20 |- ( 3 e. RR /\ 1 < 3 )
30		recgt1i 10920	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 3 e. RR /\ 1 < 3 ) -> ( 0 < ( 1 / 3 ) /\ ( 1 / 3 ) < 1 ) )
31	30	simprd 479	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 3 e. RR /\ 1 < 3 ) -> ( 1 / 3 ) < 1 )
32	29, 31	mp1i 13	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> ( 1 / 3 ) < 1 )
33	25, 26, 27, 32	ltsub2dd 10640	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ t e. T ) -> ( N - 1 ) < ( N - ( 1 / 3 ) ) )
34	27, 26	resubcld 10458	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> ( N - 1 ) e. RR )
35	27, 25	resubcld 10458	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> ( N - ( 1 / 3 ) ) e. RR )
36		stoweidlem34.12	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> E e. RR+ )
37	36	rpred 11872	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> E e. RR )
38	37	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> E e. RR )
39	36	rpgt0d 11875	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> 0 < E )
40	39	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. T ) -> 0 < E )
41		ltmul1 10873	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
42	34, 35, 38, 40, 41	syl112anc 1330	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ t e. T ) -> ( ( N - 1 ) < ( N - ( 1 / 3 ) ) <-> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) )
43	33, 42	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. T ) -> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) )
44	21, 43	jca 554	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ t e. T ) -> ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) )
45		stoweidlem34.9	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F : T --> RR )
46	45	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
47	34, 38	remulcld 10070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. T ) -> ( ( N - 1 ) x. E ) e. RR )
48	35, 38	remulcld 10070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. T ) -> ( ( N - ( 1 / 3 ) ) x. E ) e. RR )
49		lttr 10114	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
50		ltle 10126	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
51	50	3adant2 1080	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
52	49, 51	syld 47	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
53	46, 47, 48, 52	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
54	44, 53	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( ph /\ t e. T ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) )
55		rabid 3116	. . . . . . . . . . . . . . 15 |- ( t e. { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
56	2, 54, 55	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. T ) -> t e. { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
57		nnnn0 11299	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> N e. NN0 )
58		nn0uz 11722	. . . . . . . . . . . . . . . . . 18 |- NN0 = ( ZZ>= ` 0 )
59	57, 58	syl6eleq 2711	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> N e. ( ZZ>= ` 0 ) )
60		eluzfz2 12349	. . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
61	15, 59, 60	3syl 18	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. ( 0 ... N ) )
62		stoweidlem34.8	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. _V )
63		rabexg 4812	. . . . . . . . . . . . . . . . 17 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V )
64	62, 63	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V )
65		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( j = N -> ( j - ( 1 / 3 ) ) = ( N - ( 1 / 3 ) ) )
66	65	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 |- ( j = N -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( N - ( 1 / 3 ) ) x. E ) )
67	66	breq2d 4665	. . . . . . . . . . . . . . . . . 18 |- ( j = N -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) )
68	67	rabbidv 3189	. . . . . . . . . . . . . . . . 17 |- ( j = N -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
69		stoweidlem34.4	. . . . . . . . . . . . . . . . 17 |- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
70	68, 69	fvmptg 6280	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( 0 ... N ) /\ { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V ) -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
71	61, 64, 70	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ph -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
72	71	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. T ) -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } )
73	56, 72	eleqtrrd 2704	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. T ) -> t e. ( D ` N ) )
74		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ j N
75		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ j ( 1 ... N )
76		nfmpt1 4747	. . . . . . . . . . . . . . . . 17 |- F/_ j ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
77	69, 76	nfcxfr 2762	. . . . . . . . . . . . . . . 16 |- F/_ j D
78	77, 74	nffv 6198	. . . . . . . . . . . . . . 15 |- F/_ j ( D ` N )
79	78	nfcri 2758	. . . . . . . . . . . . . 14 |- F/ j t e. ( D ` N )
80		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( j = N -> ( D ` j ) = ( D ` N ) )
81	80	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( j = N -> ( t e. ( D ` j ) <-> t e. ( D ` N ) ) )
82	74, 75, 79, 81	elrabf 3360	. . . . . . . . . . . . 13 |- ( N e. { j e. ( 1 ... N ) | t e. ( D ` j ) } <-> ( N e. ( 1 ... N ) /\ t e. ( D ` N ) ) )
83	20, 73, 82	sylanbrc 698	. . . . . . . . . . . 12 |- ( ( ph /\ t e. T ) -> N e. { j e. ( 1 ... N ) | t e. ( D ` j ) } )
84	83, 7	eleqtrrd 2704	. . . . . . . . . . 11 |- ( ( ph /\ t e. T ) -> N e. ( J ` t ) )
85		ne0i 3921	. . . . . . . . . . 11 |- ( N e. ( J ` t ) -> ( J ` t ) =/= (/) )
86	84, 85	syl 17	. . . . . . . . . 10 |- ( ( ph /\ t e. T ) -> ( J ` t ) =/= (/) )
87		nnwo 11753	. . . . . . . . . . 11 |- ( ( ( J ` t ) C_ NN /\ ( J ` t ) =/= (/) ) -> E. i e. ( J ` t ) A. k e. ( J ` t ) i <_ k )
88		nfcv 2764	. . . . . . . . . . . 12 |- F/_ i ( J ` t )
89		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ j T
90		nfrab1 3122	. . . . . . . . . . . . . . 15 |- F/_ j { j e. ( 1 ... N ) | t e. ( D ` j ) }
91	89, 90	nfmpt 4746	. . . . . . . . . . . . . 14 |- F/_ j ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
92	5, 91	nfcxfr 2762	. . . . . . . . . . . . 13 |- F/_ j J
93		nfcv 2764	. . . . . . . . . . . . 13 |- F/_ j t
94	92, 93	nffv 6198	. . . . . . . . . . . 12 |- F/_ j ( J ` t )
95		nfv 1843	. . . . . . . . . . . . 13 |- F/ j i <_ k
96	94, 95	nfral 2945	. . . . . . . . . . . 12 |- F/ j A. k e. ( J ` t ) i <_ k
97		nfv 1843	. . . . . . . . . . . 12 |- F/ i A. k e. ( J ` t ) j <_ k
98		breq1 4656	. . . . . . . . . . . . 13 |- ( i = j -> ( i <_ k <-> j <_ k ) )
99	98	ralbidv 2986	. . . . . . . . . . . 12 |- ( i = j -> ( A. k e. ( J ` t ) i <_ k <-> A. k e. ( J ` t ) j <_ k ) )
100	88, 94, 96, 97, 99	cbvrexf 3166	. . . . . . . . . . 11 |- ( E. i e. ( J ` t ) A. k e. ( J ` t ) i <_ k <-> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k )
101	87, 100	sylib 208	. . . . . . . . . 10 |- ( ( ( J ` t ) C_ NN /\ ( J ` t ) =/= (/) ) -> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k )
102	12, 86, 101	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k )
103		stoweidlem34.2	. . . . . . . . . . 11 |- F/ j ph
104		nfv 1843	. . . . . . . . . . 11 |- F/ j t e. T
105	103, 104	nfan 1828	. . . . . . . . . 10 |- F/ j ( ph /\ t e. T )
106	7	eleq2d 2687	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) <-> j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } ) )
107	106	biimpa 501	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } )
108		rabid 3116	. . . . . . . . . . . . . . 15 |- ( j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } <-> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) )
109	107, 108	sylib 208	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) )
110	109	simprd 479	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> t e. ( D ` j ) )
111	110	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> t e. ( D ` j ) )
112		simp3 1063	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> t e. ( D ` ( j - 1 ) ) )
113		simp1l 1085	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ph )
114		noel 3919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -. t e. (/)
115		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( j = 1 -> ( j - 1 ) = ( 1 - 1 ) )
116		1m1e0 11089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 1 - 1 ) = 0
117	115, 116	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( j = 1 -> ( j - 1 ) = 0 )
118	117	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( j = 1 -> ( D ` ( j - 1 ) ) = ( D ` 0 ) )
119	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ t e. T ) -> 3 e. RR )
120	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ t e. T ) -> 3 =/= 0 )
121	26, 119, 120	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ t e. T ) -> ( 1 / 3 ) e. RR )
122	121	renegcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ t e. T ) -> -u ( 1 / 3 ) e. RR )
123	122, 38	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) e. RR )
124		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ t e. T ) -> 0 e. RR )
125		3pos 11114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- 0 < 3
126	22, 125	recgt0ii 10929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- 0 < ( 1 / 3 )
127		lt0neg2 10535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( 1 / 3 ) e. RR -> ( 0 < ( 1 / 3 ) <-> -u ( 1 / 3 ) < 0 ) )
128	24, 127	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( 0 < ( 1 / 3 ) <-> -u ( 1 / 3 ) < 0 )
129	126, 128	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- -u ( 1 / 3 ) < 0
130		ltmul1 10873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( -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 ) ) )
131	122, 124, 38, 40, 130	syl112anc 1330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) < 0 <-> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) ) )
132	129, 131	mpbii 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) )
133		mul02lem2 10213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( E e. RR -> ( 0 x. E ) = 0 )
134	38, 133	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ t e. T ) -> ( 0 x. E ) = 0 )
135	132, 134	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < 0 )
136		stoweidlem34.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )
137	123, 124, 46, 135, 136	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < ( F ` t ) )
138	123, 46	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ t e. T ) -> ( ( -u ( 1 / 3 ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
139	137, 138	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ t e. T ) -> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) )
140		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph -> -. ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) <-> ( ( ph /\ t e. T ) -> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
141	139, 140	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> -. ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
142		rabid 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( t e. { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
143	141, 142	sylnibr 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> -. t e. { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
144	15	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> N e. NN0 )
145		elnn0uz 11725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
146	144, 145	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> N e. ( ZZ>= ` 0 ) )
147		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> 0 e. ( 0 ... N ) )
149		rabexg 4812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V )
150	62, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V )
151		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( j = 0 -> ( j - ( 1 / 3 ) ) = ( 0 - ( 1 / 3 ) ) )
152		df-neg 10269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- -u ( 1 / 3 ) = ( 0 - ( 1 / 3 ) )
153	151, 152	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( j = 0 -> ( j - ( 1 / 3 ) ) = -u ( 1 / 3 ) )
154	153	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( j = 0 -> ( ( j - ( 1 / 3 ) ) x. E ) = ( -u ( 1 / 3 ) x. E ) )
155	154	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( j = 0 -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) )
156	155	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( j = 0 -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
157	156, 69	fvmptg 6280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 0 e. ( 0 ... N ) /\ { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V ) -> ( D ` 0 ) = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
158	148, 150, 157	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> ( D ` 0 ) = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } )
159	143, 158	neleqtrrd 2723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> -. t e. ( D ` 0 ) )
160	1, 159	alrimi 2082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> A. t -. t e. ( D ` 0 ) )
161		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- F/_ t ( 0 ... N )
162		nfrab1 3122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- F/_ t { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) }
163	161, 162	nfmpt 4746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
164	69, 163	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- F/_ t D
165		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- F/_ t 0
166	164, 165	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- F/_ t ( D ` 0 )
167	166	eq0f 3925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( D ` 0 ) = (/) <-> A. t -. t e. ( D ` 0 ) )
168	160, 167	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( D ` 0 ) = (/) )
169	118, 168	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j = 1 ) -> ( D ` ( j - 1 ) ) = (/) )
170	169	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 1 ) -> ( t e. ( D ` ( j - 1 ) ) <-> t e. (/) ) )
171	114, 170	mtbiri 317	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j = 1 ) -> -. t e. ( D ` ( j - 1 ) ) )
172	171	ex 450	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( j = 1 -> -. t e. ( D ` ( j - 1 ) ) ) )
173	172	con2d 129	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( t e. ( D ` ( j - 1 ) ) -> -. j = 1 ) )
174	113, 112, 173	sylc 65	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. j = 1 )
175		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> ph )
176	106, 108	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) <-> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) ) )
177	176	simprbda 653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. ( 1 ... N ) )
178	15, 17	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> N e. ( ZZ>= ` 1 ) )
179	178	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. ( J ` t ) ) -> N e. ( ZZ>= ` 1 ) )
180		elfzp12 12419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. ( ZZ>= ` 1 ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) )
181	179, 180	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) )
182	181	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) )
183	177, 182	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) )
184	183	orcanai 952	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> j e. ( ( 1 + 1 ) ... N ) )
185		fzssp1 12384	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 1 ... ( N - 1 ) ) C_ ( 1 ... ( ( N - 1 ) + 1 ) )
186	15	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> N e. CC )
187		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> 1 e. CC )
188	186, 187	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
189	188	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
190	185, 189	syl5sseq 3653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
191	190	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
192		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> j e. ( ( 1 + 1 ) ... N ) )
193		1z 11407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- 1 e. ZZ
194		zaddcl 11417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 1 e. ZZ /\ 1 e. ZZ ) -> ( 1 + 1 ) e. ZZ )
195	193, 193, 194	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 1 + 1 ) e. ZZ
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( 1 + 1 ) e. ZZ )
197	15	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> N e. ZZ )
198	197	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> N e. ZZ )
199		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( j e. ( ( 1 + 1 ) ... N ) -> j e. ZZ )
200	199	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> j e. ZZ )
201		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> 1 e. ZZ )
202		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 ) ) ) )
203	196, 198, 200, 201, 202	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j e. ( ( 1 + 1 ) ... N ) <-> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
204	192, 203	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) )
205		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 1 e. CC
206	205, 205	pncan3oi 10297	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 1 + 1 ) - 1 ) = 1
207	206	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
208	204, 207	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( 1 ... ( N - 1 ) ) )
209	191, 208	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( 1 ... N ) )
210	175, 184, 209	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> ( j - 1 ) e. ( 1 ... N ) )
211	210	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( -. j = 1 -> ( j - 1 ) e. ( 1 ... N ) ) )
212	211	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( -. j = 1 -> ( j - 1 ) e. ( 1 ... N ) ) )
213	174, 212	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. ( 1 ... N ) )
214		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i = ( j - 1 ) -> ( D ` i ) = ( D ` ( j - 1 ) ) )
215	214	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = ( j - 1 ) -> ( t e. ( D ` i ) <-> t e. ( D ` ( j - 1 ) ) ) )
216	215	elrab3 3364	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j - 1 ) e. ( 1 ... N ) -> ( ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } <-> t e. ( D ` ( j - 1 ) ) ) )
217	213, 216	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) )
218	112, 217	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } )
219		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 |- F/_ i ( 1 ... N )
220		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 |- F/ i t e. ( D ` j )
221		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j i
222	77, 221	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ j ( D ` i )
223	222	nfcri 2758	. . . . . . . . . . . . . . . . . . . 20 |- F/ j t e. ( D ` i )
224		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = i -> ( D ` j ) = ( D ` i ) )
225	224	eleq2d 2687	. . . . . . . . . . . . . . . . . . . 20 |- ( j = i -> ( t e. ( D ` j ) <-> t e. ( D ` i ) ) )
226	75, 219, 220, 223, 225	cbvrab 3198	. . . . . . . . . . . . . . . . . . 19 |- { j e. ( 1 ... N ) | t e. ( D ` j ) } = { i e. ( 1 ... N ) | t e. ( D ` i ) }
227	218, 226	syl6eleqr 2712	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. { j e. ( 1 ... N ) | t e. ( D ` j ) } )
228	7	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } )
229	227, 228	eleqtrrd 2704	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. ( J ` t ) )
230		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ( 1 ... N ) -> j e. ZZ )
231		zre 11381	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ZZ -> j e. RR )
232	177, 230, 231	3syl 18	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. RR )
233	232	3adant3 1081	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> j e. RR )
234		peano2rem 10348	. . . . . . . . . . . . . . . . . . 19 |- ( j e. RR -> ( j - 1 ) e. RR )
235	233, 234	jccir 562	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j e. RR /\ ( j - 1 ) e. RR ) )
236		ltm1 10863	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. RR -> ( j - 1 ) < j )
237	236	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. RR /\ ( j - 1 ) e. RR ) -> ( j - 1 ) < j )
238		ltnle 10117	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( j - 1 ) e. RR /\ j e. RR ) -> ( ( j - 1 ) < j <-> -. j <_ ( j - 1 ) ) )
239	238	ancoms 469	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. RR /\ ( j - 1 ) e. RR ) -> ( ( j - 1 ) < j <-> -. j <_ ( j - 1 ) ) )
240	237, 239	mpbid 222	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. RR /\ ( j - 1 ) e. RR ) -> -. j <_ ( j - 1 ) )
241	235, 240	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. j <_ ( j - 1 ) )
242		breq2 4657	. . . . . . . . . . . . . . . . . . 19 |- ( k = ( j - 1 ) -> ( j <_ k <-> j <_ ( j - 1 ) ) )
243	242	notbid 308	. . . . . . . . . . . . . . . . . 18 |- ( k = ( j - 1 ) -> ( -. j <_ k <-> -. j <_ ( j - 1 ) ) )
244	243	rspcev 3309	. . . . . . . . . . . . . . . . 17 |- ( ( ( j - 1 ) e. ( J ` t ) /\ -. j <_ ( j - 1 ) ) -> E. k e. ( J ` t ) -. j <_ k )
245	229, 241, 244	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> E. k e. ( J ` t ) -. j <_ k )
246		rexnal 2995	. . . . . . . . . . . . . . . 16 |- ( E. k e. ( J ` t ) -. j <_ k <-> -. A. k e. ( J ` t ) j <_ k )
247	245, 246	sylib 208	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. A. k e. ( J ` t ) j <_ k )
248	247	3expia 1267	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( t e. ( D ` ( j - 1 ) ) -> -. A. k e. ( J ` t ) j <_ k ) )
249	248	con2d 129	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( A. k e. ( J ` t ) j <_ k -> -. t e. ( D ` ( j - 1 ) ) ) )
250	249	imp 445	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> -. t e. ( D ` ( j - 1 ) ) )
251	111, 250	eldifd 3585	. . . . . . . . . . 11 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
252	251	exp31 630	. . . . . . . . . 10 |- ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) -> ( A. k e. ( J ` t ) j <_ k -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) )
253	105, 252	reximdai 3012	. . . . . . . . 9 |- ( ( 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 ) ) ) ) )
254	102, 253	mpd 15	. . . . . . . 8 |- ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
255		df-rex 2918	. . . . . . . 8 |- ( 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 ) ) ) ) )
256	254, 255	sylib 208	. . . . . . 7 |- ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) )
257		simprl 794	. . . . . . . . . 10 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. ( J ` t ) )
258		eldifn 3733	. . . . . . . . . . . . 13 |- ( t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) -> -. t e. ( D ` ( j - 1 ) ) )
259		simplr 792	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> t e. T )
260		simpll 790	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ph )
261	177	adantrr 753	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> j e. ( 1 ... N ) )
262		simprr 796	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. t e. ( D ` ( j - 1 ) ) )
263		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = k -> ( j - ( 1 / 3 ) ) = ( k - ( 1 / 3 ) ) )
264	263	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = k -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( k - ( 1 / 3 ) ) x. E ) )
265	264	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = k -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) ) )
266	265	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = k -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } )
267	266	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) } )
268	69, 267	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22 |- D = ( k e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } )
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( 1 ... N ) ) -> D = ( k e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } ) )
270		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = ( j - 1 ) -> ( k - ( 1 / 3 ) ) = ( ( j - 1 ) - ( 1 / 3 ) ) )
271	270	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = ( j - 1 ) -> ( ( k - ( 1 / 3 ) ) x. E ) = ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) )
272	271	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k = ( j - 1 ) -> ( ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) )
273	272	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = ( j - 1 ) -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
274	273	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k = ( j - 1 ) ) -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
275		fzssp1 12384	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
276	188	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
277	275, 276	syl5sseq 3653	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
278	277	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
279		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
280		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. ( 1 ... N ) ) -> 1 e. ZZ )
281	197	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. ( 1 ... N ) ) -> N e. ZZ )
282	230	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ZZ )
283		fzsubel 12377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
284	280, 281, 282, 280, 283	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
285	279, 284	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) )
286	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( 1 - 1 ) = 0 )
287	286	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) ) )
288	285, 287	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
289	278, 288	sseldd 3604	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ... N ) )
290	62	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. ( 1 ... N ) ) -> T e. _V )
291		rabexg 4812	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
292	290, 291	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( 1 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
293	269, 274, 289, 292	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( D ` ( j - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
294	293	eleq2d 2687	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( t e. ( D ` ( j - 1 ) ) <-> t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) )
295	294	notbid 308	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( -. t e. ( D ` ( j - 1 ) ) <-> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) )
296	295	biimpa 501	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ -. t e. ( D ` ( j - 1 ) ) ) -> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } )
297	260, 261, 262, 296	syl21anc 1325	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) } )
298		rabid 3116	. . . . . . . . . . . . . . . . 17 |- ( t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) )
299	232	adantrr 753	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> j e. RR )
300		recn 10026	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. RR -> j e. CC )
301		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. RR -> 1 e. CC )
302		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 1 e. RR
303	302, 22, 23	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 e. RR /\ 3 e. RR /\ 3 =/= 0 )
304		redivcl 10744	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 e. RR /\ 3 e. RR /\ 3 =/= 0 ) -> ( 1 / 3 ) e. RR )
305		recn 10026	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 / 3 ) e. RR -> ( 1 / 3 ) e. CC )
306	303, 304, 305	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 / 3 ) e. CC
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. RR -> ( 1 / 3 ) e. CC )
308	300, 301, 307	subsub4d 10423	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. RR -> ( ( j - 1 ) - ( 1 / 3 ) ) = ( j - ( 1 + ( 1 / 3 ) ) ) )
309		3cn 11095	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 3 e. CC
310	309, 205, 309, 23	divdiri 10782	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
311		3p1e4 11153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 3 + 1 ) = 4
312	311	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
313	309, 23	dividi 10758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 3 / 3 ) = 1
314	313	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
315	310, 312, 314	3eqtr3i 2652	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 4 / 3 ) = ( 1 + ( 1 / 3 ) )
316	315	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. RR -> ( 4 / 3 ) = ( 1 + ( 1 / 3 ) ) )
317	316	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. RR -> ( j - ( 4 / 3 ) ) = ( j - ( 1 + ( 1 / 3 ) ) ) )
318	308, 317	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. RR -> ( ( j - 1 ) - ( 1 / 3 ) ) = ( j - ( 4 / 3 ) ) )
319	318	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. RR -> ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) )
320	299, 319	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) )
321	320	breq2d 4665	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
322	321	anbi2d 740	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
323	298, 322	syl5bb 272	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) ) )
324	297, 323	mtbid 314	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
325		imnan 438	. . . . . . . . . . . . . . 15 |- ( ( t e. T -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) <-> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
326	324, 325	sylibr 224	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( t e. T -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) )
327	259, 326	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) )
328	258, 327	sylanr2 685	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) )
329	232	adantrr 753	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. RR )
330		4re 11097	. . . . . . . . . . . . . . . . 17 |- 4 e. RR
331	330	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 4 e. RR )
332	22	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 3 e. RR )
333	23	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 3 =/= 0 )
334	331, 332, 333	redivcld 10853	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( 4 / 3 ) e. RR )
335	329, 334	resubcld 10458	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( j - ( 4 / 3 ) ) e. RR )
336	37	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E e. RR )
337		remulcl 10021	. . . . . . . . . . . . . . 15 |- ( ( ( j - ( 4 / 3 ) ) e. RR /\ E e. RR ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR )
338	337	rexrd 10089	. . . . . . . . . . . . . 14 |- ( ( ( j - ( 4 / 3 ) ) e. RR /\ E e. RR ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR* )
339	335, 336, 338	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR* )
340	46	rexrd 10089	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR* )
341	340	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( F ` t ) e. RR* )
342		xrltnle 10105	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
343	339, 341, 342	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
344	328, 343	mpbird 247	. . . . . . . . . . 11 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) )
345		simpl 473	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ph /\ t e. T ) )
346		simprr 796	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
347	346	eldifad 3586	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. ( D ` j ) )
348		simplll 798	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ph )
349	177	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> j e. ( 1 ... N ) )
350		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> t e. ( D ` j ) )
351		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = j -> ( k - ( 1 / 3 ) ) = ( j - ( 1 / 3 ) ) )
352	351	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( ( k - ( 1 / 3 ) ) x. E ) = ( ( j - ( 1 / 3 ) ) x. E ) )
353	352	breq2d 4665	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
354	353	rabbidv 3189	. . . . . . . . . . . . . . . . . . 19 |- ( k = j -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
355	354	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k = j ) -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
356		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 + 1 ) = 1
357	356	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 + 1 ) ... N ) = ( 1 ... N )
358		0z 11388	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. ZZ
359		fzp1ss 12392	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 e. ZZ -> ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) )
360	358, 359	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 + 1 ) ... N ) C_ ( 0 ... N )
361	357, 360	eqsstr3i 3636	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 ... N ) C_ ( 0 ... N )
362	361	sseli 3599	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 1 ... N ) -> j e. ( 0 ... N ) )
363	362	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 0 ... N ) )
364		rabexg 4812	. . . . . . . . . . . . . . . . . . 19 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V )
365	290, 364	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 1 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V )
366	269, 355, 363, 365	fvmptd 6288	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
367	366	eleq2d 2687	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 1 ... N ) ) -> ( t e. ( D ` j ) <-> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) )
368	367	biimpa 501	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ t e. ( D ` j ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
369	348, 349, 350, 368	syl21anc 1325	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
370		rabid 3116	. . . . . . . . . . . . . 14 |- ( t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
371	369, 370	sylib 208	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
372	371	simprd 479	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
373	345, 257, 347, 372	syl21anc 1325	. . . . . . . . . . 11 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
374	344, 373	jca 554	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
375	15	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> N e. NN )
376		simplr 792	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. T )
377	177	adantrr 753	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. ( 1 ... N ) )
378		nfv 1843	. . . . . . . . . . . . . . . 16 |- F/ j i e. ( 0 ... N )
379	103, 378	nfan 1828	. . . . . . . . . . . . . . 15 |- F/ j ( ph /\ i e. ( 0 ... N ) )
380		nfv 1843	. . . . . . . . . . . . . . 15 |- F/ j ( X ` i ) : T --> RR
381	379, 380	nfim 1825	. . . . . . . . . . . . . 14 |- F/ j ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
382		eleq1 2689	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( j e. ( 0 ... N ) <-> i e. ( 0 ... N ) ) )
383	382	anbi2d 740	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ i e. ( 0 ... N ) ) ) )
384		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( X ` j ) = ( X ` i ) )
385	384	feq1d 6030	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( X ` j ) : T --> RR <-> ( X ` i ) : T --> RR ) )
386	383, 385	imbi12d 334	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) ) )
387		stoweidlem34.14	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR )
388	381, 386, 387	chvar 2262	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
389	388	ad4ant14 1293	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
390		simplll 798	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ph )
391		simpr 477	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) )
392		simpllr 799	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> t e. T )
393	103, 378, 104	nf3an 1831	. . . . . . . . . . . . . . 15 |- F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. T )
394		nfv 1843	. . . . . . . . . . . . . . 15 |- F/ j ( ( X ` i ) ` t ) <_ 1
395	393, 394	nfim 1825	. . . . . . . . . . . . . 14 |- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 )
396	382	3anbi2d 1404	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. T ) ) )
397	384	fveq1d 6193	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( ( X ` j ) ` t ) = ( ( X ` i ) ` t ) )
398	397	breq1d 4663	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( ( X ` j ) ` t ) <_ 1 <-> ( ( X ` i ) ` t ) <_ 1 ) )
399	396, 398	imbi12d 334	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
400		stoweidlem34.16	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 )
401	395, 399, 400	chvar 2262	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 )
402	390, 391, 392, 401	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) <_ 1 )
403		simplll 798	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ph )
404		0zd 11389	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 e. ZZ )
405		elfzel2 12340	. . . . . . . . . . . . . . . . 17 |- ( i e. ( j ... N ) -> N e. ZZ )
406	405	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> N e. ZZ )
407		elfzelz 12342	. . . . . . . . . . . . . . . . 17 |- ( i e. ( j ... N ) -> i e. ZZ )
408	407	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. ZZ )
409	404, 406, 408	3jca 1242	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) )
410		0red 10041	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 e. RR )
411		elfzel1 12341	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( j ... N ) -> j e. ZZ )
412	411	zred 11482	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( j ... N ) -> j e. RR )
413	412	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> j e. RR )
414	407	zred 11482	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( j ... N ) -> i e. RR )
415	414	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. RR )
416		0red 10041	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 e. RR )
417		1red 10055	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 1 e. RR )
418		0le1 10551	. . . . . . . . . . . . . . . . . . . 20 |- 0 <_ 1
419	418	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 <_ 1 )
420		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 1 ... N ) -> 1 <_ j )
421	177, 420	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 1 <_ j )
422	416, 417, 232, 419, 421	letrd 10194	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 <_ j )
423	422	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 <_ j )
424		elfzle1 12344	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( j ... N ) -> j <_ i )
425	424	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> j <_ i )
426	410, 413, 415, 423, 425	letrd 10194	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 <_ i )
427		elfzle2 12345	. . . . . . . . . . . . . . . . 17 |- ( i e. ( j ... N ) -> i <_ N )
428	427	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i <_ N )
429	426, 428	jca 554	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> ( 0 <_ i /\ i <_ N ) )
430		elfz2 12333	. . . . . . . . . . . . . . 15 |- ( i e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) /\ ( 0 <_ i /\ i <_ N ) ) )
431	409, 429, 430	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
432	431	adantlrr 757	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
433		simpll 790	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ( ph /\ t e. T ) )
434		simplrl 800	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> j e. ( J ` t ) )
435		simplrr 801	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) ) )
436	435	eldifad 3586	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` j ) )
437		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> i e. ( j ... N ) )
438		simpl1 1064	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ph /\ t e. T ) )
439	438	simprd 479	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. T )
440	438, 46	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) e. RR )
441	412	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. RR )
442	24	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( 1 / 3 ) e. RR )
443	441, 442	resubcld 10458	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( j - ( 1 / 3 ) ) e. RR )
444		simpl1l 1112	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ph )
445	444, 37	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> E e. RR )
446	443, 445	remulcld 10070	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) e. RR )
447	414	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( j ... N ) ) -> i e. RR )
448	24	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( j ... N ) ) -> ( 1 / 3 ) e. RR )
449	447, 448	resubcld 10458	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( j ... N ) ) -> ( i - ( 1 / 3 ) ) e. RR )
450	37	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( j ... N ) ) -> E e. RR )
451	449, 450	remulcld 10070	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( j ... N ) ) -> ( ( i - ( 1 / 3 ) ) x. E ) e. RR )
452	444, 451	sylancom 701	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( i - ( 1 / 3 ) ) x. E ) e. RR )
453		simpl3 1066	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` j ) )
454		simpl2 1065	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. ( J ` t ) )
455	438, 454, 177	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. ( 1 ... N ) )
456	444, 455, 366	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) } )
457	453, 456	eleqtrd 2703	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) } )
458	457, 370	sylib 208	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) ) )
459	458	simprd 479	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
460	414	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. RR )
461	424	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j <_ i )
462	441, 460, 442, 461	lesub1dd 10643	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) )
463	444, 449	sylancom 701	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( i - ( 1 / 3 ) ) e. RR )
464	36	rpregt0d 11878	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( E e. RR /\ 0 < E ) )
465	444, 464	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( E e. RR /\ 0 < E ) )
466		lemul1 10875	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
467	443, 463, 465, 466	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) ) )
468	462, 467	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) )
469	440, 446, 452, 459, 468	letrd 10194	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) )
470		rabid 3116	. . . . . . . . . . . . . . . 16 |- ( t e. { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) )
471	439, 469, 470	sylanbrc 698	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) } )
472		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. ( j ... N ) )
473		0zd 11389	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> 0 e. ZZ )
474	405	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> N e. ZZ )
475	407	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> i e. ZZ )
476	473, 474, 475	3jca 1242	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) )
477	429	3impa 1259	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> ( 0 <_ i /\ i <_ N ) )
478	476, 477, 430	sylanbrc 698	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
479	438, 454, 472, 478	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) )
480		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) )
481		rabexg 4812	. . . . . . . . . . . . . . . . . . 19 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V )
482	62, 481	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V )
483	482	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V )
484		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = i -> ( j - ( 1 / 3 ) ) = ( i - ( 1 / 3 ) ) )
485	484	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 |- ( j = i -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( i - ( 1 / 3 ) ) x. E ) )
486	485	breq2d 4665	. . . . . . . . . . . . . . . . . . 19 |- ( j = i -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) )
487	486	rabbidv 3189	. . . . . . . . . . . . . . . . . 18 |- ( j = i -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
488	487, 69	fvmptg 6280	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0 ... N ) /\ { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V ) -> ( D ` i ) = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
489	480, 483, 488	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( D ` i ) = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } )
490	444, 479, 489	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) } )
491	471, 490	eleqtrrd 2704	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` i ) )
492	433, 434, 436, 437, 491	syl31anc 1329	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` i ) )
493	103, 378, 223	nf3an 1831	. . . . . . . . . . . . . . 15 |- F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) )
494		nfv 1843	. . . . . . . . . . . . . . 15 |- F/ j ( ( X ` i ) ` t ) < ( E / N )
495	493, 494	nfim 1825	. . . . . . . . . . . . . 14 |- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
496	382, 225	3anbi23d 1402	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) ) )
497	397	breq1d 4663	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( ( X ` j ) ` t ) < ( E / N ) <-> ( ( X ` i ) ` t ) < ( E / N ) ) )
498	496, 497	imbi12d 334	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
499		stoweidlem34.17	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) )
500	495, 498, 499	chvar 2262	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
501	403, 432, 492, 500	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )
502	36	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E e. RR+ )
503		stoweidlem34.13	. . . . . . . . . . . . 13 |- ( ph -> E < ( 1 / 3 ) )
504	503	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E < ( 1 / 3 ) )
505	375, 376, 377, 389, 402, 501, 502, 504	stoweidlem11 40228	. . . . . . . . . . 11 |- ( ( ( 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 ) )
506		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( l = j -> ( l e. ( J ` t ) <-> j e. ( J ` t ) ) )
507		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( l = j -> ( D ` l ) = ( D ` j ) )
508		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( l = j -> ( l - 1 ) = ( j - 1 ) )
509	508	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( l = j -> ( D ` ( l - 1 ) ) = ( D ` ( j - 1 ) ) )
510	507, 509	difeq12d 3729	. . . . . . . . . . . . . . . . . 18 |- ( l = j -> ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) = ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) )
511	510	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( l = j -> ( t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) <-> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) )
512	506, 511	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( l = j -> ( ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) <-> ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) )
513	512	anbi2d 740	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) ) )
514		oveq1 6657	. . . . . . . . . . . . . . . . 17 |- ( l = j -> ( l - ( 4 / 3 ) ) = ( j - ( 4 / 3 ) ) )
515	514	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( l = j -> ( ( l - ( 4 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) )
516	515	breq1d 4663	. . . . . . . . . . . . . . 15 |- ( 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 ) ) )
517	513, 516	imbi12d 334	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
518		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20 |- ( s = t -> ( s e. T <-> t e. T ) )
519	518	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 |- ( s = t -> ( ( ph /\ s e. T ) <-> ( ph /\ t e. T ) ) )
520		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = t -> ( J ` s ) = ( J ` t ) )
521	520	eleq2d 2687	. . . . . . . . . . . . . . . . . . . 20 |- ( s = t -> ( l e. ( J ` s ) <-> l e. ( J ` t ) ) )
522		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20 |- ( s = t -> ( s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) <-> t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) )
523	521, 522	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 |- ( s = t -> ( ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) <-> ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) )
524	519, 523	anbi12d 747	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) ) ) )
525		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) )
526	525	breq2d 4665	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) )
527	524, 526	imbi12d 334	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) )
528		stoweidlem34.1	. . . . . . . . . . . . . . . . . 18 |- F/_ t F
529		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 |- F/ j s e. T
530	103, 529	nfan 1828	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( ph /\ s e. T )
531		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j s
532	92, 531	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ j ( J ` s )
533	532	nfcri 2758	. . . . . . . . . . . . . . . . . . . 20 |- F/ j l e. ( J ` s )
534		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ j l
535	77, 534	nffv 6198	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j ( D ` l )
536		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ j ( l - 1 )
537	77, 536	nffv 6198	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j ( D ` ( l - 1 ) )
538	535, 537	nfdif 3731	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ j ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
539	538	nfcri 2758	. . . . . . . . . . . . . . . . . . . 20 |- F/ j s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
540	533, 539	nfan 1828	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) )
541	530, 540	nfan 1828	. . . . . . . . . . . . . . . . . 18 |- F/ j ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) )
542		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 |- F/ t s e. T
543	1, 542	nfan 1828	. . . . . . . . . . . . . . . . . . 19 |- F/ t ( ph /\ s e. T )
544		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )
545	5, 544	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ t J
546		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ t s
547	545, 546	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t ( J ` s )
548	547	nfcri 2758	. . . . . . . . . . . . . . . . . . . 20 |- F/ t l e. ( J ` s )
549		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t l
550	164, 549	nffv 6198	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ t ( D ` l )
551		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t ( l - 1 )
552	164, 551	nffv 6198	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ t ( D ` ( l - 1 ) )
553	550, 552	nfdif 3731	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
554	553	nfcri 2758	. . . . . . . . . . . . . . . . . . . 20 |- F/ t s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) )
555	548, 554	nfan 1828	. . . . . . . . . . . . . . . . . . 19 |- F/ t ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) )
556	543, 555	nfan 1828	. . . . . . . . . . . . . . . . . 18 |- F/ t ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) )
557		stoweidlem34.5	. . . . . . . . . . . . . . . . . 18 |- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
558	15	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> N e. NN )
559	62	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> T e. _V )
560	3	rabex 4813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { j e. ( 1 ... N ) | s e. ( D ` j ) } e. _V
561		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- F/_ t j
562	164, 561	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- F/_ t ( D ` j )
563	562	nfcri 2758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/ t s e. ( D ` j )
564		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ t ( 1 ... N )
565	563, 564	nfrab 3123	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ t { j e. ( 1 ... N ) | s e. ( D ` j ) }
566		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( t = s -> ( t e. ( D ` j ) <-> s e. ( D ` j ) ) )
567	566	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( t = s -> { j e. ( 1 ... N ) | t e. ( D ` j ) } = { j e. ( 1 ... N ) | s e. ( D ` j ) } )
568	546, 565, 567, 5	fvmptf 6301	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s e. T /\ { j e. ( 1 ... N ) | s e. ( D ` j ) } e. _V ) -> ( J ` s ) = { j e. ( 1 ... N ) | s e. ( D ` j ) } )
569	560, 568	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. T -> ( J ` s ) = { j e. ( 1 ... N ) | s e. ( D ` j ) } )
570	569	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. T -> ( l e. ( J ` s ) <-> l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } ) )
571	570	biimpa 501	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. T /\ l e. ( J ` s ) ) -> l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } )
572	535	nfcri 2758	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ j s e. ( D ` l )
573		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> ( D ` j ) = ( D ` l ) )
574	573	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = l -> ( s e. ( D ` j ) <-> s e. ( D ` l ) ) )
575	534, 75, 572, 574	elrabf 3360	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } <-> ( l e. ( 1 ... N ) /\ s e. ( D ` l ) ) )
576	571, 575	sylib 208	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s e. T /\ l e. ( J ` s ) ) -> ( l e. ( 1 ... N ) /\ s e. ( D ` l ) ) )
577	576	simpld 475	. . . . . . . . . . . . . . . . . . 19 |- ( ( s e. T /\ l e. ( J ` s ) ) -> l e. ( 1 ... N ) )
578	577	ad2ant2lr 784	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> l e. ( 1 ... N ) )
579		simprr 796	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) )
580	45	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> F : T --> RR )
581	36	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> E e. RR+ )
582	503	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> E < ( 1 / 3 ) )
583	388	ad4ant14 1293	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
584		simp1ll 1124	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. T ) -> ph )
585		nfv 1843	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j 0 <_ ( ( X ` i ) ` t )
586	393, 585	nfim 1825	. . . . . . . . . . . . . . . . . . . 20 |- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
587	397	breq2d 4665	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = i -> ( 0 <_ ( ( X ` j ) ` t ) <-> 0 <_ ( ( X ` i ) ` t ) ) )
588	396, 587	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) )
589		stoweidlem34.15	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) )
590	586, 588, 589	chvar 2262	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
591	584, 590	syld3an1 1372	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) )
592		simp1ll 1124	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ph )
593		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ j ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
594	557, 593	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ j B
595	594, 221	nffv 6198	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ j ( B ` i )
596	595	nfcri 2758	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ j t e. ( B ` i )
597	103, 378, 596	nf3an 1831	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) )
598		nfv 1843	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j ( 1 - ( E / N ) ) < ( ( X ` i ) ` t )
599	597, 598	nfim 1825	. . . . . . . . . . . . . . . . . . . 20 |- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
600		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = i -> ( B ` j ) = ( B ` i ) )
601	600	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = i -> ( t e. ( B ` j ) <-> t e. ( B ` i ) ) )
602	382, 601	3anbi23d 1402	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) ) )
603	397	breq2d 4665	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = i -> ( ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) )
604	602, 603	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) )
605		stoweidlem34.18	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) )
606	599, 604, 605	chvar 2262	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
607	592, 606	syld3an1 1372	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) )
608	528, 541, 556, 69, 557, 558, 559, 578, 579, 580, 581, 582, 583, 591, 607	stoweidlem26 40243	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) )
609	527, 608	vtoclg 3266	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) )
610	609	ad2antlr 763	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
611	610	pm2.43i 52	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
612	517, 611	vtoclg 3266	. . . . . . . . . . . . 13 |- ( 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 ) ) )
613	612	ad2antrl 764	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
614	613	pm2.43i 52	. . . . . . . . . . 11 |- ( ( ( 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 ) )
615	505, 614	jca 554	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
616	257, 374, 615	3jca 1242	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
617	616	ex 450	. . . . . . . 8 |- ( ( 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 ) ) ) ) )
618	105, 617	eximd 2085	. . . . . . 7 |- ( ( 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 ) ) ) ) )
619	256, 618	mpd 15	. . . . . 6 |- ( ( 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 ) ) ) )
620		3anass 1042	. . . . . . 7 |- ( ( 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 ) ) ) ) )
621	620	exbii 1774	. . . . . 6 |- ( 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 ) ) ) ) )
622	619, 621	sylib 208	. . . . 5 |- ( ( 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 ) ) ) ) )
623		df-rex 2918	. . . . 5 |- ( 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 ) ) ) ) )
624	622, 623	sylibr 224	. . . 4 |- ( ( 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 ) ) ) )
625		nfcv 2764	. . . . 5 |- F/_ j RR
626	94, 625	ssrexf 3665	. . . 4 |- ( ( 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 ) ) ) ) )
627	14, 624, 626	sylc 65	. . 3 |- ( ( 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 ) ) ) )
628	627	ex 450	. 2 |- ( 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 ) ) ) ) )
629	1, 628	ralrimi 2957	1 |- ( 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 ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   F/wnf 1708   e. wcel 1990   F/_wnfc 2751   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   class class class wbr 4653   |-> cmpt 4729   -->wf 5884   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   3c3 11071   4c4 11072   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   ...cfz 12326   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417

This theorem is referenced by:  stoweidlem60  40277