Theorem stoweidlem26 27642

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 9046	. . . . . . . 8 |- 1 e. RR
2		eleq1 2464	. . . . . . . 8 |- ( L = 1 -> ( L e. RR <-> 1 e. RR ) )
3	1, 2	mpbiri 225	. . . . . . 7 |- ( L = 1 -> L e. RR )
4	3	adantl 453	. . . . . 6 |- ( ( ph /\ L = 1 ) -> L e. RR )
5		4re 10029	. . . . . . . 8 |- 4 e. RR
6	5	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 4 e. RR )
7		3re 10027	. . . . . . . 8 |- 3 e. RR
8	7	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 e. RR )
9		3ne0 10041	. . . . . . . 8 |- 3 =/= 0
10	9	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 =/= 0 )
11	6, 8, 10	redivcld 9798	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
12	4, 11	resubcld 9421	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
13		stoweidlem26.11	. . . . . . 7 |- ( ph -> E e. RR+ )
14	13	rpred 10604	. . . . . 6 |- ( ph -> E e. RR )
15	14	adantr 452	. . . . 5 |- ( ( ph /\ L = 1 ) -> E e. RR )
16	12, 15	remulcld 9072	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
17		0re 9047	. . . . 5 |- 0 e. RR
18	17	a1i 11	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 e. RR )
19		fzfid 11267	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
20	14	adantr 452	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> E e. RR )
21		stoweidlem26.13	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
22		stoweidlem26.9	. . . . . . . . . . . . . 14 |- ( ph -> S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) )
23		eldif 3290	. . . . . . . . . . . . . 14 |- ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
24	22, 23	sylib 189	. . . . . . . . . . . . 13 |- ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
25	24	simpld 446	. . . . . . . . . . . 12 |- ( ph -> S e. ( D ` L ) )
26		1e0p1 10366	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
27	26	oveq1i 6050	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) = ( ( 0 + 1 ) ... N )
28		0z 10249	. . . . . . . . . . . . . . . 16 |- 0 e. ZZ
29		fzp1ss 11054	. . . . . . . . . . . . . . . 16 |- ( 0 e. ZZ -> ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) )
30	28, 29	ax-mp 8	. . . . . . . . . . . . . . 15 |- ( ( 0 + 1 ) ... N ) C_ ( 0 ... N )
31	27, 30	eqsstri 3338	. . . . . . . . . . . . . 14 |- ( 1 ... N ) C_ ( 0 ... N )
32		stoweidlem26.8	. . . . . . . . . . . . . 14 |- ( ph -> L e. ( 1 ... N ) )
33	31, 32	sseldi 3306	. . . . . . . . . . . . 13 |- ( ph -> L e. ( 0 ... N ) )
34		stoweidlem26.7	. . . . . . . . . . . . . 14 |- ( ph -> T e. _V )
35		rabexg 4313	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
36	34, 35	syl 16	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
37		oveq1 6047	. . . . . . . . . . . . . . . . 17 |- ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) )
38	37	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) )
39	38	breq2d 4184	. . . . . . . . . . . . . . 15 |- ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
40	39	rabbidv 2908	. . . . . . . . . . . . . 14 |- ( j = L -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
41		stoweidlem26.4	. . . . . . . . . . . . . 14 |- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
42	40, 41	fvmptg 5763	. . . . . . . . . . . . 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 ) } )
43	33, 36, 42	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
44	25, 43	eleqtrd 2480	. . . . . . . . . . 11 |- ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
45		nfcv 2540	. . . . . . . . . . . 12 |- F/_ t S
46		nfcv 2540	. . . . . . . . . . . 12 |- F/_ t T
47		stoweidlem26.1	. . . . . . . . . . . . . 14 |- F/_ t F
48	47, 45	nffv 5694	. . . . . . . . . . . . 13 |- F/_ t ( F ` S )
49		nfcv 2540	. . . . . . . . . . . . 13 |- F/_ t <_
50		nfcv 2540	. . . . . . . . . . . . 13 |- F/_ t ( ( L - ( 1 / 3 ) ) x. E )
51	48, 49, 50	nfbr 4216	. . . . . . . . . . . 12 |- F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E )
52		fveq2 5687	. . . . . . . . . . . . 13 |- ( t = S -> ( F ` t ) = ( F ` S ) )
53	52	breq1d 4182	. . . . . . . . . . . 12 |- ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
54	45, 46, 51, 53	elrabf 3051	. . . . . . . . . . 11 |- ( S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
55	44, 54	sylib 189	. . . . . . . . . 10 |- ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
56	55	simpld 446	. . . . . . . . 9 |- ( ph -> S e. T )
57	56	adantr 452	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T )
58	21, 57	ffvelrnd 5830	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
59	20, 58	remulcld 9072	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
60	19, 59	fsumrecl 12483	. . . . 5 |- ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
61	60	adantr 452	. . . 4 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
62	5, 7, 9	redivcli 9737	. . . . . . 7 |- ( 4 / 3 ) e. RR
63	62	a1i 11	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
64	4, 63	resubcld 9421	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
65	4	recnd 9070	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> L e. CC )
66	65	subid1d 9356	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) = L )
67		3cn 10028	. . . . . . . . . 10 |- 3 e. CC
68	67, 9	dividi 9703	. . . . . . . . 9 |- ( 3 / 3 ) = 1
69		3lt4 10101	. . . . . . . . . 10 |- 3 < 4
70		3pos 10040	. . . . . . . . . . 11 |- 0 < 3
71	7, 5, 7, 70	ltdiv1ii 9896	. . . . . . . . . 10 |- ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) )
72	69, 71	mpbi 200	. . . . . . . . 9 |- ( 3 / 3 ) < ( 4 / 3 )
73	68, 72	eqbrtrri 4193	. . . . . . . 8 |- 1 < ( 4 / 3 )
74		breq1 4175	. . . . . . . . 9 |- ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
75	74	adantl 453	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
76	73, 75	mpbiri 225	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) )
77	66, 76	eqbrtrd 4192	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) )
78	4, 18, 63, 77	ltsub23d 9587	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 )
79	13	rpgt0d 10607	. . . . . 6 |- ( ph -> 0 < E )
80	79	adantr 452	. . . . 5 |- ( ( ph /\ L = 1 ) -> 0 < E )
81		mulltgt0 27560	. . . . 5 |- ( ( ( ( L - ( 4 / 3 ) ) e. RR /\ ( L - ( 4 / 3 ) ) < 0 ) /\ ( E e. RR /\ 0 < E ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
82	64, 78, 15, 80, 81	syl22anc 1185	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
83		0cn 9040	. . . . . . . 8 |- 0 e. CC
84		fsumconst 12528	. . . . . . . 8 |- ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
85	19, 83, 84	sylancl 644	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
86		hashcl 11594	. . . . . . . . 9 |- ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 )
87		nn0cn 10187	. . . . . . . . 9 |- ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC )
88	19, 86, 87	3syl 19	. . . . . . . 8 |- ( ph -> ( # ` ( 0 ... N ) ) e. CC )
89	88	mul01d 9221	. . . . . . 7 |- ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 )
90	85, 89	eqtrd 2436	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 )
91	90	adantr 452	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 )
92	17	a1i 11	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR )
93	13	rpge0d 10608	. . . . . . . . 9 |- ( ph -> 0 <_ E )
94	93	adantr 452	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E )
95		stoweidlem26.3	. . . . . . . . . . . 12 |- F/ t ph
96		nfv 1626	. . . . . . . . . . . 12 |- F/ t i e. ( 0 ... N )
97	95, 96	nfan 1842	. . . . . . . . . . 11 |- F/ t ( ph /\ i e. ( 0 ... N ) )
98		nfv 1626	. . . . . . . . . . 11 |- F/ t 0 <_ ( ( X ` i ) ` S )
99	97, 98	nfim 1828	. . . . . . . . . 10 |- F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
100		fveq2 5687	. . . . . . . . . . . 12 |- ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) )
101	100	breq2d 4184	. . . . . . . . . . 11 |- ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) )
102	101	imbi2d 308	. . . . . . . . . 10 |- ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) ) )
103		stoweidlem26.14	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )
104	103	3expia 1155	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) )
105	104	com12 29	. . . . . . . . . 10 |- ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) )
106	45, 99, 102, 105	vtoclgaf 2976	. . . . . . . . 9 |- ( S e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) )
107	57, 106	mpcom 34	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
108	20, 58, 94, 107	mulge0d 9559	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
109	19, 92, 59, 108	fsumle 12533	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
110	109	adantr 452	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
111	91, 110	eqbrtrrd 4194	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
112	16, 18, 61, 82, 111	ltletrd 9186	. . 3 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
113		elfzelz 11015	. . . . . . . . 9 |- ( L e. ( 1 ... N ) -> L e. ZZ )
114		zre 10242	. . . . . . . . 9 |- ( L e. ZZ -> L e. RR )
115	32, 113, 114	3syl 19	. . . . . . . 8 |- ( ph -> L e. RR )
116	5	a1i 11	. . . . . . . . 9 |- ( ph -> 4 e. RR )
117	7	a1i 11	. . . . . . . . 9 |- ( ph -> 3 e. RR )
118	9	a1i 11	. . . . . . . . 9 |- ( ph -> 3 =/= 0 )
119	116, 117, 118	redivcld 9798	. . . . . . . 8 |- ( ph -> ( 4 / 3 ) e. RR )
120	115, 119	resubcld 9421	. . . . . . 7 |- ( ph -> ( L - ( 4 / 3 ) ) e. RR )
121	120, 14	remulcld 9072	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
122	121	adantr 452	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
123	1	a1i 11	. . . . . . . . 9 |- ( ph -> 1 e. RR )
124		stoweidlem26.6	. . . . . . . . . 10 |- ( ph -> N e. NN )
125	14, 124	nndivred 10004	. . . . . . . . 9 |- ( ph -> ( E / N ) e. RR )
126	123, 125	resubcld 9421	. . . . . . . 8 |- ( ph -> ( 1 - ( E / N ) ) e. RR )
127	115, 123	resubcld 9421	. . . . . . . 8 |- ( ph -> ( L - 1 ) e. RR )
128	126, 127	remulcld 9072	. . . . . . 7 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
129	14, 128	remulcld 9072	. . . . . 6 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
130	129	adantr 452	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
131		fzfid 11267	. . . . . . . 8 |- ( ph -> ( 0 ... ( L - 2 ) ) e. Fin )
132	32, 113	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> L e. ZZ )
133		2z 10268	. . . . . . . . . . . . . . 15 |- 2 e. ZZ
134	133	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. ZZ )
135	132, 134	zsubcld 10336	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) e. ZZ )
136	124	nnzd 10330	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
137	132	zred 10331	. . . . . . . . . . . . . . 15 |- ( ph -> L e. RR )
138		2re 10025	. . . . . . . . . . . . . . . 16 |- 2 e. RR
139	138	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. RR )
140	137, 139	resubcld 9421	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. RR )
141	124	nnred 9971	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
142		2pos 10038	. . . . . . . . . . . . . . . . 17 |- 0 < 2
143	17, 138, 142	ltleii 9152	. . . . . . . . . . . . . . . 16 |- 0 <_ 2
144	17	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. RR )
145	144, 139, 137	lesub2d 9590	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) )
146	143, 145	mpbii 203	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) <_ ( L - 0 ) )
147	132	zcnd 10332	. . . . . . . . . . . . . . . 16 |- ( ph -> L e. CC )
148	147	subid1d 9356	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 0 ) = L )
149	146, 148	breqtrd 4196	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) <_ L )
150		elfzle2 11017	. . . . . . . . . . . . . . 15 |- ( L e. ( 1 ... N ) -> L <_ N )
151	32, 150	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
152	140, 137, 141, 149, 151	letrd 9183	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) <_ N )
153	135, 136, 152	3jca 1134	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
154		eluz2 10450	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
155	153, 154	sylibr 204	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) )
156		fzss2 11048	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` ( L - 2 ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
157	155, 156	syl 16	. . . . . . . . . 10 |- ( ph -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
158	157	sselda 3308	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
159	158, 58	syldan 457	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
160	131, 159	fsumrecl 12483	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
161	14, 160	remulcld 9072	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
162	161	adantr 452	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
163	14, 127	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( E x. ( L - 1 ) ) e. RR )
164	14, 14	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( E x. E ) e. RR )
165	163, 164	resubcld 9421	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR )
166	127, 124	nndivred 10004	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) / N ) e. RR )
167	164, 166	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR )
168	163, 167	resubcld 9421	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR )
169	127, 14	resubcld 9421	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) - E ) e. RR )
170	123, 14	readdcld 9071	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) e. RR )
171	1, 7, 9	redivcli 9737	. . . . . . . . . . . . . . 15 |- ( 1 / 3 ) e. RR
172	171	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 3 ) e. RR )
173		stoweidlem26.12	. . . . . . . . . . . . . 14 |- ( ph -> E < ( 1 / 3 ) )
174	14, 172, 123, 173	ltadd2dd 9185	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) )
175		ax-1cn 9004	. . . . . . . . . . . . . . 15 |- 1 e. CC
176	67, 175, 67, 9	divdiri 9727	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
177		3p1e4 10060	. . . . . . . . . . . . . . 15 |- ( 3 + 1 ) = 4
178	177	oveq1i 6050	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
179	68	oveq1i 6050	. . . . . . . . . . . . . 14 |- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
180	176, 178, 179	3eqtr3ri 2433	. . . . . . . . . . . . 13 |- ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
181	174, 180	syl6breq 4211	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) < ( 4 / 3 ) )
182	170, 119, 115, 181	ltsub2dd 9595	. . . . . . . . . . 11 |- ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) )
183	175	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. CC )
184	13	rpcnd 10606	. . . . . . . . . . . 12 |- ( ph -> E e. CC )
185	147, 183, 184	subsub4d 9398	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) )
186	182, 185	breqtrrd 4198	. . . . . . . . . 10 |- ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) )
187	120, 169, 13, 186	ltmul1dd 10655	. . . . . . . . 9 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) )
188	147, 183	subcld 9367	. . . . . . . . . . . 12 |- ( ph -> ( L - 1 ) e. CC )
189	188, 184	subcld 9367	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) e. CC )
190	184, 189	mulcomd 9065	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) )
191	184, 188, 184	subdid 9445	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
192	190, 191	eqtr3d 2438	. . . . . . . . 9 |- ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
193	187, 192	breqtrd 4196	. . . . . . . 8 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
194		1z 10267	. . . . . . . . . . . . . . . . . 18 |- 1 e. ZZ
195	194	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. ZZ )
196		elfz 11005	. . . . . . . . . . . . . . . . 17 |- ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
197	132, 195, 136, 196	syl3anc 1184	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
198	32, 197	mpbid 202	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 <_ L /\ L <_ N ) )
199	198	simprd 450	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
200		zlem1lt 10283	. . . . . . . . . . . . . . 15 |- ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
201	132, 136, 200	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ph -> ( L <_ N <-> ( L - 1 ) < N ) )
202	199, 201	mpbid 202	. . . . . . . . . . . . 13 |- ( ph -> ( L - 1 ) < N )
203	124	nngt0d 9999	. . . . . . . . . . . . . 14 |- ( ph -> 0 < N )
204		ltdiv1 9830	. . . . . . . . . . . . . 14 |- ( ( ( L - 1 ) e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
205	127, 141, 141, 203, 204	syl112anc 1188	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
206	202, 205	mpbid 202	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 1 ) / N ) < ( N / N ) )
207	124	nncnd 9972	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
208	124	nnne0d 10000	. . . . . . . . . . . . 13 |- ( ph -> N =/= 0 )
209	207, 208	dividd 9744	. . . . . . . . . . . 12 |- ( ph -> ( N / N ) = 1 )
210	206, 209	breqtrd 4196	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) < 1 )
211	14, 14, 79, 79	mulgt0d 9181	. . . . . . . . . . . 12 |- ( ph -> 0 < ( E x. E ) )
212		ltmul2 9817	. . . . . . . . . . . 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 ) ) )
213	166, 123, 164, 211, 212	syl112anc 1188	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
214	210, 213	mpbid 202	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) )
215	184, 184	mulcld 9064	. . . . . . . . . . 11 |- ( ph -> ( E x. E ) e. CC )
216	215	mulid1d 9061	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) )
217	214, 216	breqtrd 4196	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) )
218	167, 164, 163, 217	ltsub2dd 9595	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
219	121, 165, 168, 193, 218	lttrd 9187	. . . . . . 7 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
220	184, 207, 208	divcld 9746	. . . . . . . . . . 11 |- ( ph -> ( E / N ) e. CC )
221	183, 220, 188	subdird 9446	. . . . . . . . . 10 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) )
222	188	mulid2d 9062	. . . . . . . . . . 11 |- ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) )
223	222	oveq1d 6055	. . . . . . . . . 10 |- ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
224	221, 223	eqtrd 2436	. . . . . . . . 9 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
225	224	oveq2d 6056	. . . . . . . 8 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) )
226	220, 188	mulcld 9064	. . . . . . . . 9 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC )
227	184, 188, 226	subdid 9445	. . . . . . . 8 |- ( ph -> ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) )
228	184, 207, 188, 208	div32d 9769	. . . . . . . . . . 11 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) )
229	228	oveq2d 6056	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
230	188, 207, 208	divcld 9746	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) e. CC )
231	184, 184, 230	mulassd 9067	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
232	229, 231	eqtr4d 2439	. . . . . . . . 9 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) )
233	232	oveq2d 6056	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
234	225, 227, 233	3eqtrd 2440	. . . . . . 7 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
235	219, 234	breqtrrd 4198	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
236	235	adantr 452	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
237	183, 220	subcld 9367	. . . . . . . . . 10 |- ( ph -> ( 1 - ( E / N ) ) e. CC )
238		fsumconst 12528	. . . . . . . . . 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 ) ) ) )
239	131, 237, 238	syl2anc 643	. . . . . . . . 9 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
240	239	adantr 452	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
241	28	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 e. ZZ )
242	32	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 1 ... N ) )
243	242, 113	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> L e. ZZ )
244	133	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 e. ZZ )
245	243, 244	zsubcld 10336	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ )
246		elnnuz 10478	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
247	124, 246	sylib 189	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ( ZZ>= ` 1 ) )
248		elfzp12 11081	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( ZZ>= ` 1 ) -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
249	247, 248	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
250	32, 249	mpbid 202	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) )
251	250	orcanai 880	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) )
252		1p1e2 10050	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
253	252	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 )
254	253	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
255	251, 254	eleqtrd 2480	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) )
256		elfzle1 11016	. . . . . . . . . . . . . . 15 |- ( L e. ( 2 ... N ) -> 2 <_ L )
257	255, 256	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 <_ L )
258	115	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. RR )
259	138	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> 2 e. RR )
260	258, 259	subge0d 9572	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) )
261	257, 260	mpbird 224	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) )
262	241, 245, 261	3jca 1134	. . . . . . . . . . . 12 |- ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
263		eluz2 10450	. . . . . . . . . . . 12 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
264	262, 263	sylibr 204	. . . . . . . . . . 11 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) )
265		hashfz 11647	. . . . . . . . . . 11 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
266	264, 265	syl 16	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
267		2cn 10026	. . . . . . . . . . . . . . . 16 |- 2 e. CC
268	267	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. CC )
269	147, 268	subcld 9367	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. CC )
270	269	subid1d 9356	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) )
271	270	oveq1d 6055	. . . . . . . . . . . 12 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) )
272	147, 268, 183	subadd23d 9389	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) )
273	267, 175	negsubdi2i 9342	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = ( 1 - 2 )
274		2m1e1 10051	. . . . . . . . . . . . . . . . 17 |- ( 2 - 1 ) = 1
275	274	negeqi 9255	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = -u 1
276	273, 275	eqtr3i 2426	. . . . . . . . . . . . . . 15 |- ( 1 - 2 ) = -u 1
277	276	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 - 2 ) = -u 1 )
278	277	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) )
279	147, 183	negsubd 9373	. . . . . . . . . . . . 13 |- ( ph -> ( L + -u 1 ) = ( L - 1 ) )
280	278, 279	eqtrd 2436	. . . . . . . . . . . 12 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) )
281	271, 272, 280	3eqtrd 2440	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
282	281	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
283	266, 282	eqtrd 2436	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) )
284	283	oveq1d 6055	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) )
285	188, 237	mulcomd 9065	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
286	285	adantr 452	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
287	240, 284, 286	3eqtrd 2440	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
288		fzfid 11267	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin )
289		fzn0 11026	. . . . . . . . 9 |- ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) )
290	264, 289	sylibr 204	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) )
291	126	ad2antrr 707	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR )
292		simpll 731	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph )
293	158	adantlr 696	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
294	292, 293, 58	syl2anc 643	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
295	56	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T )
296		elfzelz 11015	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ )
297	296	zred 10331	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR )
298	297	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. RR )
299	171	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 / 3 ) e. RR )
300	298, 299	readdcld 9071	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR )
301	14	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR )
302	300, 301	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR )
303	115	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> L e. RR )
304	138	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> 2 e. RR )
305	303, 304	resubcld 9421	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
306	305, 299	readdcld 9071	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
307	306, 301	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
308		stoweidlem26.10	. . . . . . . . . . . . . . . 16 |- ( ph -> F : T --> RR )
309	308, 56	jca 519	. . . . . . . . . . . . . . 15 |- ( ph -> ( F : T --> RR /\ S e. T ) )
310	309	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) )
311		ffvelrn 5827	. . . . . . . . . . . . . 14 |- ( ( F : T --> RR /\ S e. T ) -> ( F ` S ) e. RR )
312	310, 311	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F ` S ) e. RR )
313		elfzle2 11017	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) )
314	313	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) )
315	298, 305, 299, 314	leadd1dd 9596	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) )
316	14, 79	jca 519	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E e. RR /\ 0 < E ) )
317	316	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) )
318		lemul1 9818	. . . . . . . . . . . . . . 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 ) ) )
319	300, 306, 317, 318	syl3anc 1184	. . . . . . . . . . . . . 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 ) ) )
320	315, 319	mpbid 202	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) )
321	115, 139	resubcld 9421	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L - 2 ) e. RR )
322	321, 172	readdcld 9071	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
323	322, 14	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
324	308, 56	ffvelrnd 5830	. . . . . . . . . . . . . . 15 |- ( ph -> ( F ` S ) e. RR )
325	127, 172	resubcld 9421	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR )
326	325, 14	remulcld 9072	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR )
327		addid1 9202	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 e. CC -> ( 1 + 0 ) = 1 )
328	327	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 e. CC -> 1 = ( 1 + 0 ) )
329	175, 328	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> 1 = ( 1 + 0 ) )
330	183	subidd 9355	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( 1 - 1 ) = 0 )
331	330	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 0 = ( 1 - 1 ) )
332	331	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) )
333		addsubass 9271	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) )
334	333	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
335	183, 183, 183, 334	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
336	329, 332, 335	3eqtrd 2440	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 1 = ( ( 1 + 1 ) - 1 ) )
337	336	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) )
338	252	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 1 ) = 2 )
339	338	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) )
340	339	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) )
341	147, 268, 183	subsubd 9395	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) )
342	337, 340, 341	3eqtrd 2440	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) )
343	342	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) )
344	267, 67, 9	divcli 9712	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 3 ) e. CC
345	344	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 / 3 ) e. CC )
346	269, 183, 345	addsubassd 9387	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) )
347	175, 67, 9	divcli 9712	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / 3 ) e. CC
348		df-3 10015	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 3 = ( 2 + 1 )
349	348	oveq1i 6050	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
350	267, 175, 67, 9	divdiri 9727	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
351	349, 68, 350	3eqtr3ri 2433	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
352	175, 344, 347, 351	subaddrii 9345	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - ( 2 / 3 ) ) = ( 1 / 3 )
353	352	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) )
354	353	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
355	343, 346, 354	3eqtrd 2440	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
356	138, 7, 9	redivcli 9737	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 / 3 ) e. RR
357	356	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 / 3 ) e. RR )
358		1lt2 10098	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
359	7, 70	pm3.2i 442	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 e. RR /\ 0 < 3 )
360	1, 138, 359	3pm3.2i 1132	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) )
361		ltdiv1 9830	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
362	360, 361	mp1i 12	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
363	358, 362	mpbii 203	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 / 3 ) < ( 2 / 3 ) )
364	172, 357, 127, 363	ltsub2dd 9595	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
365	355, 364	eqbrtrrd 4194	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
366	322, 325, 13, 365	ltmul1dd 10655	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
367	24	simprd 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. S e. ( D ` ( L - 1 ) ) )
368	198	simpld 446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> 1 <_ L )
369	141, 123	readdcld 9071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. RR )
370	141	lep1d 9898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> N <_ ( N + 1 ) )
371	115, 141, 369, 199, 370	letrd 9183	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> L <_ ( N + 1 ) )
372	136	peano2zd 10334	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. ZZ )
373		elfz 11005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( L e. ZZ /\ 1 e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
374	132, 195, 372, 373	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
375	368, 371, 374	mpbir2and 889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> L e. ( 1 ... ( N + 1 ) ) )
376	147, 183	npcand 9371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( L - 1 ) + 1 ) = L )
377	26	eqcomi 2408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 1 ) = 1
378	377	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( 0 + 1 ) = 1 )
379	378	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
380	375, 376, 379	3eltr4d 2485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
381	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> 0 e. ZZ )
382	132, 195	zsubcld 10336	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( L - 1 ) e. ZZ )
383		fzaddel 11043	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
384	381, 136, 382, 195, 383	syl22anc 1185	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
385	380, 384	mpbird 224	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( L - 1 ) e. ( 0 ... N ) )
386		rabexg 4313	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
387	34, 386	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
388		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) )
389	388	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
390	389	breq2d 4184	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
391	390	rabbidv 2908	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) } )
392	391, 41	fvmptg 5763	. . . . . . . . . . . . . . . . . . . . . . . 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 ) } )
393	385, 387, 392	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
394	367, 393	neleqtrd 2499	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
395		nfcv 2540	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
396	48, 49, 395	nfbr 4216	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
397	52	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t = S -> ( ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
398	45, 46, 396, 397	elrabf 3051	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
399	394, 398	sylnib 296	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
400		ianor 475	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
401	399, 400	sylib 189	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
402		olc 374	. . . . . . . . . . . . . . . . . . . . 21 |- ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
403	402	anim1i 552	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
404	56, 401, 403	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) )
405		orcom 377	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) )
406	405	anbi2i 676	. . . . . . . . . . . . . . . . . . 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 ) ) )
407	404, 406	sylib 189	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) )
408		pm4.43 894	. . . . . . . . . . . . . . . . . 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 ) ) )
409	407, 408	sylibr 204	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
410	326, 324	ltnled 9176	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
411	409, 410	mpbird 224	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
412	323, 326, 324, 366, 411	lttrd 9187	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
413	323, 324, 412	ltled 9177	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
414	413	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
415	302, 307, 312, 320, 414	letrd 9183	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
416		nfcv 2540	. . . . . . . . . . . . . 14 |- F/_ t ( ( i + ( 1 / 3 ) ) x. E )
417	416, 49, 48	nfbr 4216	. . . . . . . . . . . . 13 |- F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
418	52	breq2d 4184	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
419	45, 46, 417, 418	elrabf 3051	. . . . . . . . . . . 12 |- ( S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } <-> ( S e. T /\ ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
420	295, 415, 419	sylanbrc 646	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
421		rabexg 4313	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
422	34, 421	syl 16	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
423	422	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
424		oveq1 6047	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
425	424	oveq1d 6055	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
426	425	breq1d 4182	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
427	426	rabbidv 2908	. . . . . . . . . . . . 13 |- ( j = i -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
428		stoweidlem26.5	. . . . . . . . . . . . 13 |- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
429	427, 428	fvmptg 5763	. . . . . . . . . . . 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 ) } )
430	158, 423, 429	syl2anc 643	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
431	420, 430	eleqtrrd 2481	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
432	153	3ad2ant1 978	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
433	432, 154	sylibr 204	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) )
434	433, 156	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
435		simp2 958	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
436	434, 435	sseldd 3309	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
437		elex 2924	. . . . . . . . . . . . 13 |- ( S e. ( B ` i ) -> S e. _V )
438	437	3ad2ant3 980	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
439		nfcv 2540	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( 0 ... N )
440		nfrab1 2848	. . . . . . . . . . . . . . . . . . 19 |- F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
441	439, 440	nfmpt 4257	. . . . . . . . . . . . . . . . . 18 |- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
442	428, 441	nfcxfr 2537	. . . . . . . . . . . . . . . . 17 |- F/_ t B
443		nfcv 2540	. . . . . . . . . . . . . . . . 17 |- F/_ t i
444	442, 443	nffv 5694	. . . . . . . . . . . . . . . 16 |- F/_ t ( B ` i )
445	444	nfel2 2552	. . . . . . . . . . . . . . 15 |- F/ t S e. ( B ` i )
446	95, 96, 445	nf3an 1845	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
447		nfv 1626	. . . . . . . . . . . . . 14 |- F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
448	446, 447	nfim 1828	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
449		eleq1 2464	. . . . . . . . . . . . . . 15 |- ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
450	449	3anbi3d 1260	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
451	100	breq2d 4184	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
452	450, 451	imbi12d 312	. . . . . . . . . . . . 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 ) ) ) )
453		stoweidlem26.15	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
454	45, 448, 452, 453	vtoclgf 2970	. . . . . . . . . . . 12 |- ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
455	438, 454	mpcom 34	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
456	436, 455	syld3an2 1231	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
457	431, 456	mpd3an3 1280	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
458	457	adantlr 696	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
459	288, 290, 291, 294, 458	fsumlt 12534	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
460	287, 459	eqbrtrrd 4194	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
461	128	adantr 452	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
462	160	adantr 452	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
463	316	adantr 452	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
464		ltmul2 9817	. . . . . . 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 ) ) ) )
465	461, 462, 463, 464	syl3anc 1184	. . . . . 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 ) ) ) )
466	460, 465	mpbid 202	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
467	122, 130, 162, 236, 466	lttrd 9187	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
468	158, 59	syldan 457	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
469	468	adantlr 696	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
470	469	recnd 9070	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
471	288, 470	fsumcl 12482	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
472	471	addid1d 9222	. . . . . 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 ) ) )
473	17	a1i 11	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 e. RR )
474		fzfid 11267	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
475	14	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
476	17	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
477	127	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
478		elfzelz 11015	. . . . . . . . . . . . . . 15 |- ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
479	478	zred 10331	. . . . . . . . . . . . . 14 |- ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
480	479	adantl 453	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
481		1m1e0 10024	. . . . . . . . . . . . . . 15 |- ( 1 - 1 ) = 0
482	123, 115, 123, 368	lesub1dd 9598	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
483	481, 482	syl5eqbrr 4206	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( L - 1 ) )
484	483	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
485		simpr 448	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
486	478	adantl 453	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
487	382	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
488	136	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
489		elfz 11005	. . . . . . . . . . . . . . . 16 |- ( ( i e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
490	486, 487, 488, 489	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
491	485, 490	mpbid 202	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
492	491	simpld 446	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
493	476, 477, 480, 484, 492	letrd 9183	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
494		elfzle2 11017	. . . . . . . . . . . . 13 |- ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
495	494	adantl 453	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
496	28	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
497		elfz 11005	. . . . . . . . . . . . 13 |- ( ( i e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
498	486, 496, 488, 497	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
499	493, 495, 498	mpbir2and 889	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
500	499, 58	syldan 457	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
501	475, 500	remulcld 9072	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
502	501	adantlr 696	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
503	474, 502	fsumrecl 12483	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
504	288, 469	fsumrecl 12483	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
505		fzfid 11267	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) ... N ) e. Fin )
506	184	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
507	506	mul01d 9221	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
508	499, 107	syldan 457	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
509	316	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
510		lemul2 9819	. . . . . . . . . . . 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 ) ) ) )
511	476, 500, 509, 510	syl3anc 1184	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
512	508, 511	mpbid 202	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
513	507, 512	eqbrtrrd 4194	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
514	505, 501, 513	fsumge0 12529	. . . . . . . 8 |- ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
515	514	adantr 452	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
516	473, 503, 504, 515	leadd2dd 9597	. . . . . 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 ) ) ) )
517	472, 516	eqbrtrrd 4194	. . . . 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 ) ) ) )
518	159	recnd 9070	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
519	131, 184, 518	fsummulc2 12522	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) )
520	519	adantr 452	. . . . 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 ) ) )
521		stoweidlem26.2	. . . . . . . . 9 |- F/ j ph
522		elfzelz 11015	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
523	522	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
524	523	zred 10331	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
525	321	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
526	127	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
527		simpr 448	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
528	28	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
529	135	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
530		elfz 11005	. . . . . . . . . . . . . . . . 17 |- ( ( j e. ZZ /\ 0 e. ZZ /\ ( L - 2 ) e. ZZ ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
531	523, 528, 529, 530	syl3anc 1184	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
532	527, 531	mpbid 202	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
533	532	simprd 450	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
534	123, 139, 115	ltsub2d 9592	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
535	358, 534	mpbii 203	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) < ( L - 1 ) )
536	535	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
537	524, 525, 526, 533, 536	lelttrd 9184	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
538	524, 526	ltnled 9176	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) ->