Theorem stoweidlem26 37455

Description: This lemma is used to prove that there is a function g as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here L is used to represnt j in the paper, D is used to represent A in the paper, S is used to represent t, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Hypotheses

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

Assertion

Ref	Expression
stoweidlem26	|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) )

Distinct variable groups:   i, j, t, E   i, L, j, t   i, N, j, t   S, i, t   ph, i   j, F   T, j, t   t, X

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

Proof of Theorem stoweidlem26

Step	Hyp	Ref	Expression
1		1re 9641	. . . . . . . 8 |- 1 e. RR
2		eleq1 2501	. . . . . . . 8 |- ( L = 1 -> ( L e. RR <-> 1 e. RR ) )
3	1, 2	mpbiri 236	. . . . . . 7 |- ( L = 1 -> L e. RR )
4	3	adantl 467	. . . . . 6 |- ( ( ph /\ L = 1 ) -> L e. RR )
5		4re 10686	. . . . . . . 8 |- 4 e. RR
6	5	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 4 e. RR )
7		3re 10683	. . . . . . . 8 |- 3 e. RR
8	7	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 e. RR )
9		3ne0 10704	. . . . . . . 8 |- 3 =/= 0
10	9	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 =/= 0 )
11	6, 8, 10	redivcld 10434	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
12	4, 11	resubcld 10046	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
13		stoweidlem26.11	. . . . . . 7 |- ( ph -> E e. RR+ )
14	13	rpred 11341	. . . . . 6 |- ( ph -> E e. RR )
15	14	adantr 466	. . . . 5 |- ( ( ph /\ L = 1 ) -> E e. RR )
16	12, 15	remulcld 9670	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
17		0red 9643	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 e. RR )
18		fzfid 12183	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
19	14	adantr 466	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> E e. RR )
20		stoweidlem26.13	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
21		stoweidlem26.9	. . . . . . . . . . . . . 14 |- ( ph -> S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) )
22		eldif 3452	. . . . . . . . . . . . . 14 |- ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
23	21, 22	sylib 199	. . . . . . . . . . . . 13 |- ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
24	23	simpld 460	. . . . . . . . . . . 12 |- ( ph -> S e. ( D ` L ) )
25		1e0p1 11079	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
26	25	oveq1i 6315	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) = ( ( 0 + 1 ) ... N )
27		0z 10948	. . . . . . . . . . . . . . . 16 |- 0 e. ZZ
28		fzp1ss 11845	. . . . . . . . . . . . . . . 16 |- ( 0 e. ZZ -> ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) )
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( 0 + 1 ) ... N ) C_ ( 0 ... N )
30	26, 29	eqsstri 3500	. . . . . . . . . . . . . 14 |- ( 1 ... N ) C_ ( 0 ... N )
31		stoweidlem26.8	. . . . . . . . . . . . . 14 |- ( ph -> L e. ( 1 ... N ) )
32	30, 31	sseldi 3468	. . . . . . . . . . . . 13 |- ( ph -> L e. ( 0 ... N ) )
33		stoweidlem26.7	. . . . . . . . . . . . . 14 |- ( ph -> T e. _V )
34		rabexg 4575	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
35	33, 34	syl 17	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
36		oveq1 6312	. . . . . . . . . . . . . . . . 17 |- ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) )
37	36	oveq1d 6320	. . . . . . . . . . . . . . . 16 |- ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) )
38	37	breq2d 4438	. . . . . . . . . . . . . . 15 |- ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
39	38	rabbidv 3079	. . . . . . . . . . . . . 14 |- ( j = L -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
40		stoweidlem26.4	. . . . . . . . . . . . . 14 |- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
41	39, 40	fvmptg 5962	. . . . . . . . . . . . 13 |- ( ( L e. ( 0 ... N ) /\ { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V ) -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
42	32, 35, 41	syl2anc 665	. . . . . . . . . . . 12 |- ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
43	24, 42	eleqtrd 2519	. . . . . . . . . . 11 |- ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
44		nfcv 2591	. . . . . . . . . . . 12 |- F/_ t S
45		nfcv 2591	. . . . . . . . . . . 12 |- F/_ t T
46		stoweidlem26.1	. . . . . . . . . . . . . 14 |- F/_ t F
47	46, 44	nffv 5888	. . . . . . . . . . . . 13 |- F/_ t ( F ` S )
48		nfcv 2591	. . . . . . . . . . . . 13 |- F/_ t <_
49		nfcv 2591	. . . . . . . . . . . . 13 |- F/_ t ( ( L - ( 1 / 3 ) ) x. E )
50	47, 48, 49	nfbr 4470	. . . . . . . . . . . 12 |- F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E )
51		fveq2 5881	. . . . . . . . . . . . 13 |- ( t = S -> ( F ` t ) = ( F ` S ) )
52	51	breq1d 4436	. . . . . . . . . . . 12 |- ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
53	44, 45, 50, 52	elrabf 3233	. . . . . . . . . . 11 |- ( S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
54	43, 53	sylib 199	. . . . . . . . . 10 |- ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
55	54	simpld 460	. . . . . . . . 9 |- ( ph -> S e. T )
56	55	adantr 466	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T )
57	20, 56	ffvelrnd 6038	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
58	19, 57	remulcld 9670	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
59	18, 58	fsumrecl 13778	. . . . 5 |- ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
60	59	adantr 466	. . . 4 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
61	5, 7, 9	redivcli 10373	. . . . . . 7 |- ( 4 / 3 ) e. RR
62	61	a1i 11	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
63	4, 62	resubcld 10046	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
64	4	recnd 9668	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> L e. CC )
65	64	subid1d 9974	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) = L )
66		3cn 10684	. . . . . . . . . 10 |- 3 e. CC
67	66, 9	dividi 10339	. . . . . . . . 9 |- ( 3 / 3 ) = 1
68		3lt4 10779	. . . . . . . . . 10 |- 3 < 4
69		3pos 10703	. . . . . . . . . . 11 |- 0 < 3
70	7, 5, 7, 69	ltdiv1ii 10536	. . . . . . . . . 10 |- ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) )
71	68, 70	mpbi 211	. . . . . . . . 9 |- ( 3 / 3 ) < ( 4 / 3 )
72	67, 71	eqbrtrri 4447	. . . . . . . 8 |- 1 < ( 4 / 3 )
73		breq1 4429	. . . . . . . . 9 |- ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
74	73	adantl 467	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
75	72, 74	mpbiri 236	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) )
76	65, 75	eqbrtrd 4446	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) )
77	4, 17, 62, 76	ltsub23d 10217	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 )
78	13	rpgt0d 11344	. . . . . 6 |- ( ph -> 0 < E )
79	78	adantr 466	. . . . 5 |- ( ( ph /\ L = 1 ) -> 0 < E )
80		mulltgt0 36983	. . . . 5 |- ( ( ( ( L - ( 4 / 3 ) ) e. RR /\ ( L - ( 4 / 3 ) ) < 0 ) /\ ( E e. RR /\ 0 < E ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
81	63, 77, 15, 79, 80	syl22anc 1265	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
82		0cn 9634	. . . . . . . 8 |- 0 e. CC
83		fsumconst 13829	. . . . . . . 8 |- ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
84	18, 82, 83	sylancl 666	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
85		hashcl 12535	. . . . . . . . 9 |- ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 )
86		nn0cn 10879	. . . . . . . . 9 |- ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC )
87	18, 85, 86	3syl 18	. . . . . . . 8 |- ( ph -> ( # ` ( 0 ... N ) ) e. CC )
88	87	mul01d 9831	. . . . . . 7 |- ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 )
89	84, 88	eqtrd 2470	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 )
90	89	adantr 466	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 )
91		0red 9643	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR )
92	13	rpge0d 11345	. . . . . . . . 9 |- ( ph -> 0 <_ E )
93	92	adantr 466	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E )
94		stoweidlem26.3	. . . . . . . . . . . 12 |- F/ t ph
95		nfv 1754	. . . . . . . . . . . 12 |- F/ t i e. ( 0 ... N )
96	94, 95	nfan 1986	. . . . . . . . . . 11 |- F/ t ( ph /\ i e. ( 0 ... N ) )
97		nfv 1754	. . . . . . . . . . 11 |- F/ t 0 <_ ( ( X ` i ) ` S )
98	96, 97	nfim 1978	. . . . . . . . . 10 |- F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
99		fveq2 5881	. . . . . . . . . . . 12 |- ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) )
100	99	breq2d 4438	. . . . . . . . . . 11 |- ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) )
101	100	imbi2d 317	. . . . . . . . . 10 |- ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) ) )
102		stoweidlem26.14	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
103	102	3expia 1207	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) )
104	103	com12 32	. . . . . . . . . 10 |- ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) )
105	44, 98, 101, 104	vtoclgaf 3150	. . . . . . . . 9 |- ( S e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) )
106	56, 105	mpcom 37	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
107	19, 57, 93, 106	mulge0d 10189	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
108	18, 91, 58, 107	fsumle 13837	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
109	108	adantr 466	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
110	90, 109	eqbrtrrd 4448	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
111	16, 17, 60, 81, 110	ltletrd 9794	. . 3 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
112		elfzelz 11798	. . . . . . . . 9 |- ( L e. ( 1 ... N ) -> L e. ZZ )
113		zre 10941	. . . . . . . . 9 |- ( L e. ZZ -> L e. RR )
114	31, 112, 113	3syl 18	. . . . . . . 8 |- ( ph -> L e. RR )
115	5	a1i 11	. . . . . . . . 9 |- ( ph -> 4 e. RR )
116	7	a1i 11	. . . . . . . . 9 |- ( ph -> 3 e. RR )
117	9	a1i 11	. . . . . . . . 9 |- ( ph -> 3 =/= 0 )
118	115, 116, 117	redivcld 10434	. . . . . . . 8 |- ( ph -> ( 4 / 3 ) e. RR )
119	114, 118	resubcld 10046	. . . . . . 7 |- ( ph -> ( L - ( 4 / 3 ) ) e. RR )
120	119, 14	remulcld 9670	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
121	120	adantr 466	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
122	1	a1i 11	. . . . . . . . 9 |- ( ph -> 1 e. RR )
123		stoweidlem26.6	. . . . . . . . . 10 |- ( ph -> N e. NN )
124	14, 123	nndivred 10658	. . . . . . . . 9 |- ( ph -> ( E / N ) e. RR )
125	122, 124	resubcld 10046	. . . . . . . 8 |- ( ph -> ( 1 - ( E / N ) ) e. RR )
126	114, 122	resubcld 10046	. . . . . . . 8 |- ( ph -> ( L - 1 ) e. RR )
127	125, 126	remulcld 9670	. . . . . . 7 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
128	14, 127	remulcld 9670	. . . . . 6 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
129	128	adantr 466	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
130		fzfid 12183	. . . . . . . 8 |- ( ph -> ( 0 ... ( L - 2 ) ) e. Fin )
131	31, 112	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> L e. ZZ )
132		2z 10969	. . . . . . . . . . . . . . 15 |- 2 e. ZZ
133	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. ZZ )
134	131, 133	zsubcld 11045	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) e. ZZ )
135	123	nnzd 11039	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
136	131	zred 11040	. . . . . . . . . . . . . . 15 |- ( ph -> L e. RR )
137		2re 10679	. . . . . . . . . . . . . . . 16 |- 2 e. RR
138	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. RR )
139	136, 138	resubcld 10046	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. RR )
140	123	nnred 10624	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
141		0le2 10700	. . . . . . . . . . . . . . . 16 |- 0 <_ 2
142		0red 9643	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. RR )
143	142, 138, 136	lesub2d 10220	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) )
144	141, 143	mpbii 214	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) <_ ( L - 0 ) )
145	131	zcnd 11041	. . . . . . . . . . . . . . . 16 |- ( ph -> L e. CC )
146	145	subid1d 9974	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 0 ) = L )
147	144, 146	breqtrd 4450	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) <_ L )
148		elfzle2 11801	. . . . . . . . . . . . . . 15 |- ( L e. ( 1 ... N ) -> L <_ N )
149	31, 148	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
150	139, 136, 140, 147, 149	letrd 9791	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) <_ N )
151	134, 135, 150	3jca 1185	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
152		eluz2 11165	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
153	151, 152	sylibr 215	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) )
154		fzss2 11836	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` ( L - 2 ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
155	153, 154	syl 17	. . . . . . . . . 10 |- ( ph -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
156	155	sselda 3470	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
157	156, 57	syldan 472	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
158	130, 157	fsumrecl 13778	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
159	14, 158	remulcld 9670	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
160	159	adantr 466	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
161	14, 126	remulcld 9670	. . . . . . . . 9 |- ( ph -> ( E x. ( L - 1 ) ) e. RR )
162	14, 14	remulcld 9670	. . . . . . . . 9 |- ( ph -> ( E x. E ) e. RR )
163	161, 162	resubcld 10046	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR )
164	126, 123	nndivred 10658	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) / N ) e. RR )
165	162, 164	remulcld 9670	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR )
166	161, 165	resubcld 10046	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR )
167	126, 14	resubcld 10046	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) - E ) e. RR )
168	122, 14	readdcld 9669	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) e. RR )
169	1, 7, 9	redivcli 10373	. . . . . . . . . . . . . . 15 |- ( 1 / 3 ) e. RR
170	169	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 3 ) e. RR )
171		stoweidlem26.12	. . . . . . . . . . . . . 14 |- ( ph -> E < ( 1 / 3 ) )
172	14, 170, 122, 171	ltadd2dd 9793	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) )
173		ax-1cn 9596	. . . . . . . . . . . . . . 15 |- 1 e. CC
174	66, 173, 66, 9	divdiri 10363	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
175		3p1e4 10735	. . . . . . . . . . . . . . 15 |- ( 3 + 1 ) = 4
176	175	oveq1i 6315	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
177	67	oveq1i 6315	. . . . . . . . . . . . . 14 |- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
178	174, 176, 177	3eqtr3ri 2467	. . . . . . . . . . . . 13 |- ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
179	172, 178	syl6breq 4465	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) < ( 4 / 3 ) )
180	168, 118, 114, 179	ltsub2dd 10225	. . . . . . . . . . 11 |- ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) )
181	173	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. CC )
182	13	rpcnd 11343	. . . . . . . . . . . 12 |- ( ph -> E e. CC )
183	145, 181, 182	subsub4d 10016	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) )
184	180, 183	breqtrrd 4452	. . . . . . . . . 10 |- ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) )
185	119, 167, 13, 184	ltmul1dd 11393	. . . . . . . . 9 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) )
186	145, 181	subcld 9985	. . . . . . . . . . . 12 |- ( ph -> ( L - 1 ) e. CC )
187	186, 182	subcld 9985	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) e. CC )
188	182, 187	mulcomd 9663	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) )
189	182, 186, 182	subdid 10073	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
190	188, 189	eqtr3d 2472	. . . . . . . . 9 |- ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
191	185, 190	breqtrd 4450	. . . . . . . 8 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
192		1zzd 10968	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. ZZ )
193		elfz 11788	. . . . . . . . . . . . . . . . 17 |- ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
194	131, 192, 135, 193	syl3anc 1264	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
195	31, 194	mpbid 213	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 <_ L /\ L <_ N ) )
196	195	simprd 464	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
197		zlem1lt 10988	. . . . . . . . . . . . . . 15 |- ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
198	131, 135, 197	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ph -> ( L <_ N <-> ( L - 1 ) < N ) )
199	196, 198	mpbid 213	. . . . . . . . . . . . 13 |- ( ph -> ( L - 1 ) < N )
200	123	nngt0d 10653	. . . . . . . . . . . . . 14 |- ( ph -> 0 < N )
201		ltdiv1 10468	. . . . . . . . . . . . . 14 |- ( ( ( L - 1 ) e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
202	126, 140, 140, 200, 201	syl112anc 1268	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
203	199, 202	mpbid 213	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 1 ) / N ) < ( N / N ) )
204	123	nncnd 10625	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
205	123	nnne0d 10654	. . . . . . . . . . . . 13 |- ( ph -> N =/= 0 )
206	204, 205	dividd 10380	. . . . . . . . . . . 12 |- ( ph -> ( N / N ) = 1 )
207	203, 206	breqtrd 4450	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) < 1 )
208	14, 14, 78, 78	mulgt0d 9789	. . . . . . . . . . . 12 |- ( ph -> 0 < ( E x. E ) )
209		ltmul2 10455	. . . . . . . . . . . 12 |- ( ( ( ( L - 1 ) / N ) e. RR /\ 1 e. RR /\ ( ( E x. E ) e. RR /\ 0 < ( E x. E ) ) ) -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
210	164, 122, 162, 208, 209	syl112anc 1268	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
211	207, 210	mpbid 213	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) )
212	182, 182	mulcld 9662	. . . . . . . . . . 11 |- ( ph -> ( E x. E ) e. CC )
213	212	mulid1d 9659	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) )
214	211, 213	breqtrd 4450	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) )
215	165, 162, 161, 214	ltsub2dd 10225	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
216	120, 163, 166, 191, 215	lttrd 9795	. . . . . . 7 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
217	182, 204, 205	divcld 10382	. . . . . . . . . . 11 |- ( ph -> ( E / N ) e. CC )
218	181, 217, 186	subdird 10074	. . . . . . . . . 10 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) )
219	186	mulid2d 9660	. . . . . . . . . . 11 |- ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) )
220	219	oveq1d 6320	. . . . . . . . . 10 |- ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
221	218, 220	eqtrd 2470	. . . . . . . . 9 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
222	221	oveq2d 6321	. . . . . . . 8 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) )
223	217, 186	mulcld 9662	. . . . . . . . 9 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC )
224	182, 186, 223	subdid 10073	. . . . . . . 8 |- ( ph -> ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) )
225	182, 204, 186, 205	div32d 10405	. . . . . . . . . . 11 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) )
226	225	oveq2d 6321	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
227	186, 204, 205	divcld 10382	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) e. CC )
228	182, 182, 227	mulassd 9665	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
229	226, 228	eqtr4d 2473	. . . . . . . . 9 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) )
230	229	oveq2d 6321	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
231	222, 224, 230	3eqtrd 2474	. . . . . . 7 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
232	216, 231	breqtrrd 4452	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
233	232	adantr 466	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
234	181, 217	subcld 9985	. . . . . . . . . 10 |- ( ph -> ( 1 - ( E / N ) ) e. CC )
235		fsumconst 13829	. . . . . . . . . 10 |- ( ( ( 0 ... ( L - 2 ) ) e. Fin /\ ( 1 - ( E / N ) ) e. CC ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
236	130, 234, 235	syl2anc 665	. . . . . . . . 9 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
237	236	adantr 466	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
238		0zd 10949	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 e. ZZ )
239	31	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 1 ... N ) )
240	239, 112	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> L e. ZZ )
241	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 e. ZZ )
242	240, 241	zsubcld 11045	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ )
243		elnnuz 11195	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
244	123, 243	sylib 199	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ( ZZ>= ` 1 ) )
245		elfzp12 11871	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( ZZ>= ` 1 ) -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
247	31, 246	mpbid 213	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) )
248	247	orcanai 921	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) )
249		1p1e2 10723	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
250	249	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 )
251	250	oveq1d 6320	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
252	248, 251	eleqtrd 2519	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) )
253		elfzle1 11800	. . . . . . . . . . . . . . 15 |- ( L e. ( 2 ... N ) -> 2 <_ L )
254	252, 253	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 <_ L )
255	114	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. RR )
256	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> 2 e. RR )
257	255, 256	subge0d 10202	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) )
258	254, 257	mpbird 235	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) )
259	238, 242, 258	3jca 1185	. . . . . . . . . . . 12 |- ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
260		eluz2 11165	. . . . . . . . . . . 12 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
261	259, 260	sylibr 215	. . . . . . . . . . 11 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) )
262		hashfz 12594	. . . . . . . . . . 11 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
263	261, 262	syl 17	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
264		2cn 10680	. . . . . . . . . . . . . . . 16 |- 2 e. CC
265	264	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. CC )
266	145, 265	subcld 9985	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. CC )
267	266	subid1d 9974	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) )
268	267	oveq1d 6320	. . . . . . . . . . . 12 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) )
269	145, 265, 181	subadd23d 10007	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) )
270	264, 173	negsubdi2i 9960	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = ( 1 - 2 )
271		2m1e1 10724	. . . . . . . . . . . . . . . . 17 |- ( 2 - 1 ) = 1
272	271	negeqi 9867	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = -u 1
273	270, 272	eqtr3i 2460	. . . . . . . . . . . . . . 15 |- ( 1 - 2 ) = -u 1
274	273	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 - 2 ) = -u 1 )
275	274	oveq2d 6321	. . . . . . . . . . . . 13 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) )
276	145, 181	negsubd 9991	. . . . . . . . . . . . 13 |- ( ph -> ( L + -u 1 ) = ( L - 1 ) )
277	275, 276	eqtrd 2470	. . . . . . . . . . . 12 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) )
278	268, 269, 277	3eqtrd 2474	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
279	278	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
280	263, 279	eqtrd 2470	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) )
281	280	oveq1d 6320	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) )
282	186, 234	mulcomd 9663	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
283	282	adantr 466	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
284	237, 281, 283	3eqtrd 2474	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
285		fzfid 12183	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin )
286		fzn0 11811	. . . . . . . . 9 |- ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) )
287	261, 286	sylibr 215	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) )
288	125	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR )
289		simpll 758	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph )
290	156	adantlr 719	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
291	289, 290, 57	syl2anc 665	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
292	55	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T )
293		elfzelz 11798	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ )
294	293	zred 11040	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR )
295	294	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. RR )
296	169	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 / 3 ) e. RR )
297	295, 296	readdcld 9669	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR )
298	14	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR )
299	297, 298	remulcld 9670	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR )
300	114	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> L e. RR )
301	137	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> 2 e. RR )
302	300, 301	resubcld 10046	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
303	302, 296	readdcld 9669	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
304	303, 298	remulcld 9670	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
305		stoweidlem26.10	. . . . . . . . . . . . . . . 16 |- ( ph -> F : T --> RR )
306	305, 55	jca 534	. . . . . . . . . . . . . . 15 |- ( ph -> ( F : T --> RR /\ S e. T ) )
307	306	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) )
308		ffvelrn 6035	. . . . . . . . . . . . . 14 |- ( ( F : T --> RR /\ S e. T ) -> ( F ` S ) e. RR )
309	307, 308	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F ` S ) e. RR )
310		elfzle2 11801	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) )
311	310	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) )
312	295, 302, 296, 311	leadd1dd 10226	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) )
313	14, 78	jca 534	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E e. RR /\ 0 < E ) )
314	313	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) )
315		lemul1 10456	. . . . . . . . . . . . . . 15 |- ( ( ( i + ( 1 / 3 ) ) e. RR /\ ( ( L - 2 ) + ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) ) )
316	297, 303, 314, 315	syl3anc 1264	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) ) )
317	312, 316	mpbid 213	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) )
318	114, 138	resubcld 10046	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L - 2 ) e. RR )
319	318, 170	readdcld 9669	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
320	319, 14	remulcld 9670	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
321	305, 55	ffvelrnd 6038	. . . . . . . . . . . . . . 15 |- ( ph -> ( F ` S ) e. RR )
322	126, 170	resubcld 10046	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR )
323	322, 14	remulcld 9670	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR )
324		addid1 9812	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 e. CC -> ( 1 + 0 ) = 1 )
325	324	eqcomd 2437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 e. CC -> 1 = ( 1 + 0 ) )
326	173, 325	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> 1 = ( 1 + 0 ) )
327	181	subidd 9973	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( 1 - 1 ) = 0 )
328	327	eqcomd 2437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 0 = ( 1 - 1 ) )
329	328	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) )
330		addsubass 9884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) )
331	330	eqcomd 2437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
332	181, 181, 181, 331	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
333	326, 329, 332	3eqtrd 2474	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 1 = ( ( 1 + 1 ) - 1 ) )
334	333	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) )
335	249	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 1 ) = 2 )
336	335	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) )
337	336	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) )
338	145, 265, 181	subsubd 10013	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) )
339	334, 337, 338	3eqtrd 2474	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) )
340	339	oveq1d 6320	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) )
341	264, 66, 9	divcli 10348	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 3 ) e. CC
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 / 3 ) e. CC )
343	266, 181, 342	addsubassd 10005	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) )
344	173, 66, 9	divcli 10348	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / 3 ) e. CC
345		df-3 10669	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 3 = ( 2 + 1 )
346	345	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
347	264, 173, 66, 9	divdiri 10363	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
348	346, 67, 347	3eqtr3ri 2467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
349	173, 341, 344, 348	subaddrii 9963	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - ( 2 / 3 ) ) = ( 1 / 3 )
350	349	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) )
351	350	oveq2d 6321	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
352	340, 343, 351	3eqtrd 2474	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
353	137, 7, 9	redivcli 10373	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 / 3 ) e. RR
354	353	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 / 3 ) e. RR )
355		1lt2 10776	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
356	7, 69	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 e. RR /\ 0 < 3 )
357	1, 137, 356	3pm3.2i 1183	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) )
358		ltdiv1 10468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
359	357, 358	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
360	355, 359	mpbii 214	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 / 3 ) < ( 2 / 3 ) )
361	170, 354, 126, 360	ltsub2dd 10225	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
362	352, 361	eqbrtrrd 4448	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
363	319, 322, 13, 362	ltmul1dd 11393	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
364	23	simprd 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. S e. ( D ` ( L - 1 ) ) )
365	195	simpld 460	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> 1 <_ L )
366	140, 122	readdcld 9669	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. RR )
367	140	lep1d 10538	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> N <_ ( N + 1 ) )
368	114, 140, 366, 196, 367	letrd 9791	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> L <_ ( N + 1 ) )
369	135	peano2zd 11043	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. ZZ )
370		elfz 11788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( L e. ZZ /\ 1 e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
371	131, 192, 369, 370	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
372	365, 368, 371	mpbir2and 930	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> L e. ( 1 ... ( N + 1 ) ) )
373	145, 181	npcand 9989	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( L - 1 ) + 1 ) = L )
374		0p1e1 10721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 1 ) = 1
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( 0 + 1 ) = 1 )
376	375	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
377	372, 373, 376	3eltr4d 2532	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
378		0zd 10949	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> 0 e. ZZ )
379	131, 192	zsubcld 11045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( L - 1 ) e. ZZ )
380		fzaddel 11831	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 0 e. ZZ /\ N e. ZZ ) /\ ( ( L - 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
381	378, 135, 379, 192, 380	syl22anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
382	377, 381	mpbird 235	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( L - 1 ) e. ( 0 ... N ) )
383		rabexg 4575	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
384	33, 383	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
385		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) )
386	385	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
387	386	breq2d 4438	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
388	387	rabbidv 3079	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = ( L - 1 ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
389	388, 40	fvmptg 5962	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( L - 1 ) e. ( 0 ... N ) /\ { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V ) -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
390	382, 384, 389	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
391	364, 390	neleqtrd 2541	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
392		nfcv 2591	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
393	47, 48, 392	nfbr 4470	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
394	51	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t = S -> ( ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
395	44, 45, 393, 394	elrabf 3233	. . . . . . . . . . . . . . . . . . . . . 22 |- ( S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
396	391, 395	sylnib 305	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
397		ianor 490	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
398	396, 397	sylib 199	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
399		olc 385	. . . . . . . . . . . . . . . . . . . . 21 |- ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
400	399	anim1i 570	. . . . . . . . . . . . . . . . . . . 20 |- ( ( S e. T /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) )
401	55, 398, 400	syl2anc 665	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) )
402		orcom 388	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) )
403	402	anbi2i 698	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) <-> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) )
404	401, 403	sylib 199	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) )
405		pm4.43 935	. . . . . . . . . . . . . . . . . 18 |- ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) )
406	404, 405	sylibr 215	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
407	323, 321	ltnled 9781	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
408	406, 407	mpbird 235	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
409	320, 323, 321, 363, 408	lttrd 9795	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
410	320, 321, 409	ltled 9782	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
411	410	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
412	299, 304, 309, 317, 411	letrd 9791	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
413		nfcv 2591	. . . . . . . . . . . . . 14 |- F/_ t ( ( i + ( 1 / 3 ) ) x. E )
414	413, 48, 47	nfbr 4470	. . . . . . . . . . . . 13 |- F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
415	51	breq2d 4438	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
416	44, 45, 414, 415	elrabf 3233	. . . . . . . . . . . 12 |- ( S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } <-> ( S e. T /\ ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
417	292, 412, 416	sylanbrc 668	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
418		rabexg 4575	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
419	33, 418	syl 17	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
420	419	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
421		oveq1 6312	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
422	421	oveq1d 6320	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
423	422	breq1d 4436	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
424	423	rabbidv 3079	. . . . . . . . . . . . 13 |- ( j = i -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
425		stoweidlem26.5	. . . . . . . . . . . . 13 |- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
426	424, 425	fvmptg 5962	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... N ) /\ { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
427	156, 420, 426	syl2anc 665	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
428	417, 427	eleqtrrd 2520	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
429	151	3ad2ant1 1026	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
430	429, 152	sylibr 215	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) )
431	430, 154	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
432		simp2 1006	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
433	431, 432	sseldd 3471	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
434		elex 3096	. . . . . . . . . . . . 13 |- ( S e. ( B ` i ) -> S e. _V )
435	434	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
436		nfcv 2591	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( 0 ... N )
437		nfrab1 3016	. . . . . . . . . . . . . . . . . . 19 |- F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
438	436, 437	nfmpt 4514	. . . . . . . . . . . . . . . . . 18 |- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
439	425, 438	nfcxfr 2589	. . . . . . . . . . . . . . . . 17 |- F/_ t B
440		nfcv 2591	. . . . . . . . . . . . . . . . 17 |- F/_ t i
441	439, 440	nffv 5888	. . . . . . . . . . . . . . . 16 |- F/_ t ( B ` i )
442	441	nfel2 2609	. . . . . . . . . . . . . . 15 |- F/ t S e. ( B ` i )
443	94, 95, 442	nf3an 1988	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
444		nfv 1754	. . . . . . . . . . . . . 14 |- F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
445	443, 444	nfim 1978	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
446		eleq1 2501	. . . . . . . . . . . . . . 15 |- ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
447	446	3anbi3d 1341	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
448	99	breq2d 4438	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
449	447, 448	imbi12d 321	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) ) )
450		stoweidlem26.15	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
451	445, 449, 450	vtoclg1f 3144	. . . . . . . . . . . 12 |- ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
452	435, 451	mpcom 37	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
453	433, 452	syld3an2 1311	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
454	428, 453	mpd3an3 1361	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
455	454	adantlr 719	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
456	285, 287, 288, 291, 455	fsumlt 13838	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
457	284, 456	eqbrtrrd 4448	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
458	127	adantr 466	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
459	158	adantr 466	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
460	313	adantr 466	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
461		ltmul2 10455	. . . . . . 7 |- ( ( ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR /\ sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) <-> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) ) )
462	458, 459, 460, 461	syl3anc 1264	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) <-> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) ) )
463	457, 462	mpbid 213	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
464	121, 129, 160, 233, 463	lttrd 9795	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
465	156, 58	syldan 472	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
466	465	adantlr 719	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
467	466	recnd 9668	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
468	285, 467	fsumcl 13777	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
469	468	addid1d 9832	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + 0 ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) )
470		0red 9643	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 e. RR )
471		fzfid 12183	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
472	14	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
473		0red 9643	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
474	126	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
475		elfzelz 11798	. . . . . . . . . . . . . . 15 |- ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
476	475	zred 11040	. . . . . . . . . . . . . 14 |- ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
477	476	adantl 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
478		1m1e0 10678	. . . . . . . . . . . . . . 15 |- ( 1 - 1 ) = 0
479	122, 114, 122, 365	lesub1dd 10228	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
480	478, 479	syl5eqbrr 4460	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( L - 1 ) )
481	480	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
482		simpr 462	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
483	475	adantl 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
484	379	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
485	135	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
486		elfz 11788	. . . . . . . . . . . . . . . 16 |- ( ( i e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
487	483, 484, 485, 486	syl3anc 1264	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
488	482, 487	mpbid 213	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
489	488	simpld 460	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
490	473, 474, 477, 481, 489	letrd 9791	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
491		elfzle2 11801	. . . . . . . . . . . . 13 |- ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
492	491	adantl 467	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
493		0zd 10949	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
494		elfz 11788	. . . . . . . . . . . . 13 |- ( ( i e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
495	483, 493, 485, 494	syl3anc 1264	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
496	490, 492, 495	mpbir2and 930	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
497	496, 57	syldan 472	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
498	472, 497	remulcld 9670	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
499	498	adantlr 719	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
500	471, 499	fsumrecl 13778	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
501	285, 466	fsumrecl 13778	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
502		fzfid 12183	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) ... N ) e. Fin )
503	182	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
504	503	mul01d 9831	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
505	496, 106	syldan 472	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
506	313	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
507		lemul2 10457	. . . . . . . . . . . 12 |- ( ( 0 e. RR /\ ( ( X ` i ) ` S ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
508	473, 497, 506, 507	syl3anc 1264	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
509	505, 508	mpbid 213	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
510	504, 509	eqbrtrrd 4448	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
511	502, 498, 510	fsumge0 13833	. . . . . . . 8 |- ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
512	511	adantr 466	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
513	470, 500, 501, 512	leadd2dd 10227	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + 0 ) <_ ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) )
514	469, 513	eqbrtrrd 4448	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) <_ ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) )
515	157	recnd 9668	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
516	130, 182, 515	fsummulc2 13823	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) )
517	516	adantr 466	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) )
518		stoweidlem26.2	. . . . . . . . 9 |- F/ j ph
519		elfzelz 11798	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
520	519	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
521	520	zred 11040	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
522	318	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
523	126	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
524		simpr 462	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
525		0zd 10949	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
526	134	adantr 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
527		elfz 11788	. . . . . . . . . . . . . . . . 17 |- ( ( j e. ZZ /\ 0 e. ZZ /\ ( L - 2 ) e. ZZ ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
528	520, 525, 526, 527	syl3anc 1264	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
529	524, 528	mpbid 213	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
530	529	simprd 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
531	122, 138, 114	ltsub2d 10222	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
532	355, 531	mpbii 214	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) < ( L - 1 ) )
533	532	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
534	521, 522, 523, 530, 533	lelttrd 9792	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
535	521, 523	ltnled 9781	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) )
536	534, 535	mpbid 213	. . . . . . . . . . . 12 |- ( ( ph