Theorem stoweidlem26 31697

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 9595	. . . . . . . 8 |- 1 e. RR
2		eleq1 2513	. . . . . . . 8 |- ( L = 1 -> ( L e. RR <-> 1 e. RR ) )
3	1, 2	mpbiri 233	. . . . . . 7 |- ( L = 1 -> L e. RR )
4	3	adantl 466	. . . . . 6 |- ( ( ph /\ L = 1 ) -> L e. RR )
5		4re 10615	. . . . . . . 8 |- 4 e. RR
6	5	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 4 e. RR )
7		3re 10612	. . . . . . . 8 |- 3 e. RR
8	7	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 e. RR )
9		3ne0 10633	. . . . . . . 8 |- 3 =/= 0
10	9	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 =/= 0 )
11	6, 8, 10	redivcld 10375	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
12	4, 11	resubcld 9990	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
13		stoweidlem26.11	. . . . . . 7 |- ( ph -> E e. RR+ )
14	13	rpred 11262	. . . . . 6 |- ( ph -> E e. RR )
15	14	adantr 465	. . . . 5 |- ( ( ph /\ L = 1 ) -> E e. RR )
16	12, 15	remulcld 9624	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
17		0red 9597	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 e. RR )
18		fzfid 12059	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
19	14	adantr 465	. . . . . . 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 3469	. . . . . . . . . . . . . 14 |- ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
23	21, 22	sylib 196	. . . . . . . . . . . . 13 |- ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
24	23	simpld 459	. . . . . . . . . . . 12 |- ( ph -> S e. ( D ` L ) )
25		1e0p1 11009	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
26	25	oveq1i 6288	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) = ( ( 0 + 1 ) ... N )
27		0z 10878	. . . . . . . . . . . . . . . 16 |- 0 e. ZZ
28		fzp1ss 11737	. . . . . . . . . . . . . . . 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 3517	. . . . . . . . . . . . . 14 |- ( 1 ... N ) C_ ( 0 ... N )
31		stoweidlem26.8	. . . . . . . . . . . . . 14 |- ( ph -> L e. ( 1 ... N ) )
32	30, 31	sseldi 3485	. . . . . . . . . . . . 13 |- ( ph -> L e. ( 0 ... N ) )
33		stoweidlem26.7	. . . . . . . . . . . . . 14 |- ( ph -> T e. _V )
34		rabexg 4584	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
35	33, 34	syl 16	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
36		oveq1 6285	. . . . . . . . . . . . . . . . 17 |- ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) )
37	36	oveq1d 6293	. . . . . . . . . . . . . . . 16 |- ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) )
38	37	breq2d 4446	. . . . . . . . . . . . . . 15 |- ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
39	38	rabbidv 3085	. . . . . . . . . . . . . 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 5936	. . . . . . . . . . . . 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 661	. . . . . . . . . . . 12 |- ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
43	24, 42	eleqtrd 2531	. . . . . . . . . . 11 |- ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
44		nfcv 2603	. . . . . . . . . . . 12 |- F/_ t S
45		nfcv 2603	. . . . . . . . . . . 12 |- F/_ t T
46		stoweidlem26.1	. . . . . . . . . . . . . 14 |- F/_ t F
47	46, 44	nffv 5860	. . . . . . . . . . . . 13 |- F/_ t ( F ` S )
48		nfcv 2603	. . . . . . . . . . . . 13 |- F/_ t <_
49		nfcv 2603	. . . . . . . . . . . . 13 |- F/_ t ( ( L - ( 1 / 3 ) ) x. E )
50	47, 48, 49	nfbr 4478	. . . . . . . . . . . 12 |- F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E )
51		fveq2 5853	. . . . . . . . . . . . 13 |- ( t = S -> ( F ` t ) = ( F ` S ) )
52	51	breq1d 4444	. . . . . . . . . . . 12 |- ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
53	44, 45, 50, 52	elrabf 3239	. . . . . . . . . . 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 196	. . . . . . . . . 10 |- ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
55	54	simpld 459	. . . . . . . . 9 |- ( ph -> S e. T )
56	55	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T )
57	20, 56	ffvelrnd 6014	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
58	19, 57	remulcld 9624	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
59	18, 58	fsumrecl 13532	. . . . 5 |- ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
60	59	adantr 465	. . . 4 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
61	5, 7, 9	redivcli 10314	. . . . . . 7 |- ( 4 / 3 ) e. RR
62	61	a1i 11	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
63	4, 62	resubcld 9990	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
64	4	recnd 9622	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> L e. CC )
65	64	subid1d 9922	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) = L )
66		3cn 10613	. . . . . . . . . 10 |- 3 e. CC
67	66, 9	dividi 10280	. . . . . . . . 9 |- ( 3 / 3 ) = 1
68		3lt4 10708	. . . . . . . . . 10 |- 3 < 4
69		3pos 10632	. . . . . . . . . . 11 |- 0 < 3
70	7, 5, 7, 69	ltdiv1ii 10478	. . . . . . . . . 10 |- ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) )
71	68, 70	mpbi 208	. . . . . . . . 9 |- ( 3 / 3 ) < ( 4 / 3 )
72	67, 71	eqbrtrri 4455	. . . . . . . 8 |- 1 < ( 4 / 3 )
73		breq1 4437	. . . . . . . . 9 |- ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
74	73	adantl 466	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
75	72, 74	mpbiri 233	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) )
76	65, 75	eqbrtrd 4454	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) )
77	4, 17, 62, 76	ltsub23d 10160	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 )
78	13	rpgt0d 11265	. . . . . 6 |- ( ph -> 0 < E )
79	78	adantr 465	. . . . 5 |- ( ( ph /\ L = 1 ) -> 0 < E )
80		mulltgt0 31348	. . . . 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 1228	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
82		0cn 9588	. . . . . . . 8 |- 0 e. CC
83		fsumconst 13581	. . . . . . . 8 |- ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
84	18, 82, 83	sylancl 662	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
85		hashcl 12404	. . . . . . . . 9 |- ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 )
86		nn0cn 10808	. . . . . . . . 9 |- ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC )
87	18, 85, 86	3syl 20	. . . . . . . 8 |- ( ph -> ( # ` ( 0 ... N ) ) e. CC )
88	87	mul01d 9779	. . . . . . 7 |- ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 )
89	84, 88	eqtrd 2482	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 )
90	89	adantr 465	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 )
91		0red 9597	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR )
92	13	rpge0d 11266	. . . . . . . . 9 |- ( ph -> 0 <_ E )
93	92	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E )
94		stoweidlem26.3	. . . . . . . . . . . 12 |- F/ t ph
95		nfv 1692	. . . . . . . . . . . 12 |- F/ t i e. ( 0 ... N )
96	94, 95	nfan 1912	. . . . . . . . . . 11 |- F/ t ( ph /\ i e. ( 0 ... N ) )
97		nfv 1692	. . . . . . . . . . 11 |- F/ t 0 <_ ( ( X ` i ) ` S )
98	96, 97	nfim 1904	. . . . . . . . . 10 |- F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
99		fveq2 5853	. . . . . . . . . . . 12 |- ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) )
100	99	breq2d 4446	. . . . . . . . . . 11 |- ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) )
101	100	imbi2d 316	. . . . . . . . . 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 1197	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) )
104	103	com12 31	. . . . . . . . . 10 |- ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) )
105	44, 98, 101, 104	vtoclgaf 3156	. . . . . . . . 9 |- ( S e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) )
106	56, 105	mpcom 36	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
107	19, 57, 93, 106	mulge0d 10132	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
108	18, 91, 58, 107	fsumle 13589	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
109	108	adantr 465	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
110	90, 109	eqbrtrrd 4456	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
111	16, 17, 60, 81, 110	ltletrd 9742	. . 3 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
112		elfzelz 11694	. . . . . . . . 9 |- ( L e. ( 1 ... N ) -> L e. ZZ )
113		zre 10871	. . . . . . . . 9 |- ( L e. ZZ -> L e. RR )
114	31, 112, 113	3syl 20	. . . . . . . 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 10375	. . . . . . . 8 |- ( ph -> ( 4 / 3 ) e. RR )
119	114, 118	resubcld 9990	. . . . . . 7 |- ( ph -> ( L - ( 4 / 3 ) ) e. RR )
120	119, 14	remulcld 9624	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
121	120	adantr 465	. . . . 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 10587	. . . . . . . . 9 |- ( ph -> ( E / N ) e. RR )
125	122, 124	resubcld 9990	. . . . . . . 8 |- ( ph -> ( 1 - ( E / N ) ) e. RR )
126	114, 122	resubcld 9990	. . . . . . . 8 |- ( ph -> ( L - 1 ) e. RR )
127	125, 126	remulcld 9624	. . . . . . 7 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
128	14, 127	remulcld 9624	. . . . . 6 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
129	128	adantr 465	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
130		fzfid 12059	. . . . . . . 8 |- ( ph -> ( 0 ... ( L - 2 ) ) e. Fin )
131	31, 112	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> L e. ZZ )
132		2z 10899	. . . . . . . . . . . . . . 15 |- 2 e. ZZ
133	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. ZZ )
134	131, 133	zsubcld 10976	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) e. ZZ )
135	123	nnzd 10970	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
136	131	zred 10971	. . . . . . . . . . . . . . 15 |- ( ph -> L e. RR )
137		2re 10608	. . . . . . . . . . . . . . . 16 |- 2 e. RR
138	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. RR )
139	136, 138	resubcld 9990	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. RR )
140	123	nnred 10554	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
141		0le2 10629	. . . . . . . . . . . . . . . 16 |- 0 <_ 2
142		0red 9597	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. RR )
143	142, 138, 136	lesub2d 10163	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) )
144	141, 143	mpbii 211	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) <_ ( L - 0 ) )
145	131	zcnd 10972	. . . . . . . . . . . . . . . 16 |- ( ph -> L e. CC )
146	145	subid1d 9922	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 0 ) = L )
147	144, 146	breqtrd 4458	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) <_ L )
148		elfzle2 11696	. . . . . . . . . . . . . . 15 |- ( L e. ( 1 ... N ) -> L <_ N )
149	31, 148	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
150	139, 136, 140, 147, 149	letrd 9739	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) <_ N )
151	134, 135, 150	3jca 1175	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
152		eluz2 11093	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
153	151, 152	sylibr 212	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) )
154		fzss2 11729	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` ( L - 2 ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
155	153, 154	syl 16	. . . . . . . . . 10 |- ( ph -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
156	155	sselda 3487	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
157	156, 57	syldan 470	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
158	130, 157	fsumrecl 13532	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
159	14, 158	remulcld 9624	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
160	159	adantr 465	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
161	14, 126	remulcld 9624	. . . . . . . . 9 |- ( ph -> ( E x. ( L - 1 ) ) e. RR )
162	14, 14	remulcld 9624	. . . . . . . . 9 |- ( ph -> ( E x. E ) e. RR )
163	161, 162	resubcld 9990	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR )
164	126, 123	nndivred 10587	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) / N ) e. RR )
165	162, 164	remulcld 9624	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR )
166	161, 165	resubcld 9990	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR )
167	126, 14	resubcld 9990	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) - E ) e. RR )
168	122, 14	readdcld 9623	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) e. RR )
169	1, 7, 9	redivcli 10314	. . . . . . . . . . . . . . 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 9741	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) )
173		ax-1cn 9550	. . . . . . . . . . . . . . 15 |- 1 e. CC
174	66, 173, 66, 9	divdiri 10304	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
175		3p1e4 10664	. . . . . . . . . . . . . . 15 |- ( 3 + 1 ) = 4
176	175	oveq1i 6288	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
177	67	oveq1i 6288	. . . . . . . . . . . . . 14 |- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
178	174, 176, 177	3eqtr3ri 2479	. . . . . . . . . . . . 13 |- ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
179	172, 178	syl6breq 4473	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) < ( 4 / 3 ) )
180	168, 118, 114, 179	ltsub2dd 10168	. . . . . . . . . . 11 |- ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) )
181	173	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. CC )
182	13	rpcnd 11264	. . . . . . . . . . . 12 |- ( ph -> E e. CC )
183	145, 181, 182	subsub4d 9964	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) )
184	180, 183	breqtrrd 4460	. . . . . . . . . 10 |- ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) )
185	119, 167, 13, 184	ltmul1dd 11313	. . . . . . . . 9 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) )
186	145, 181	subcld 9933	. . . . . . . . . . . 12 |- ( ph -> ( L - 1 ) e. CC )
187	186, 182	subcld 9933	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) e. CC )
188	182, 187	mulcomd 9617	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) )
189	182, 186, 182	subdid 10015	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
190	188, 189	eqtr3d 2484	. . . . . . . . 9 |- ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
191	185, 190	breqtrd 4458	. . . . . . . 8 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
192		1zzd 10898	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. ZZ )
193		elfz 11684	. . . . . . . . . . . . . . . . 17 |- ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
194	131, 192, 135, 193	syl3anc 1227	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
195	31, 194	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 <_ L /\ L <_ N ) )
196	195	simprd 463	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
197		zlem1lt 10918	. . . . . . . . . . . . . . 15 |- ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
198	131, 135, 197	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( L <_ N <-> ( L - 1 ) < N ) )
199	196, 198	mpbid 210	. . . . . . . . . . . . 13 |- ( ph -> ( L - 1 ) < N )
200	123	nngt0d 10582	. . . . . . . . . . . . . 14 |- ( ph -> 0 < N )
201		ltdiv1 10409	. . . . . . . . . . . . . 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 1231	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
203	199, 202	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 1 ) / N ) < ( N / N ) )
204	123	nncnd 10555	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
205	123	nnne0d 10583	. . . . . . . . . . . . 13 |- ( ph -> N =/= 0 )
206	204, 205	dividd 10321	. . . . . . . . . . . 12 |- ( ph -> ( N / N ) = 1 )
207	203, 206	breqtrd 4458	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) < 1 )
208	14, 14, 78, 78	mulgt0d 9737	. . . . . . . . . . . 12 |- ( ph -> 0 < ( E x. E ) )
209		ltmul2 10396	. . . . . . . . . . . 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 1231	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
211	207, 210	mpbid 210	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) )
212	182, 182	mulcld 9616	. . . . . . . . . . 11 |- ( ph -> ( E x. E ) e. CC )
213	212	mulid1d 9613	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) )
214	211, 213	breqtrd 4458	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) )
215	165, 162, 161, 214	ltsub2dd 10168	. . . . . . . 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 9743	. . . . . . 7 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
217	182, 204, 205	divcld 10323	. . . . . . . . . . 11 |- ( ph -> ( E / N ) e. CC )
218	181, 217, 186	subdird 10016	. . . . . . . . . 10 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) )
219	186	mulid2d 9614	. . . . . . . . . . 11 |- ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) )
220	219	oveq1d 6293	. . . . . . . . . 10 |- ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
221	218, 220	eqtrd 2482	. . . . . . . . 9 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
222	221	oveq2d 6294	. . . . . . . 8 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) )
223	217, 186	mulcld 9616	. . . . . . . . 9 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC )
224	182, 186, 223	subdid 10015	. . . . . . . 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 10346	. . . . . . . . . . 11 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) )
226	225	oveq2d 6294	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
227	186, 204, 205	divcld 10323	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) e. CC )
228	182, 182, 227	mulassd 9619	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
229	226, 228	eqtr4d 2485	. . . . . . . . 9 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) )
230	229	oveq2d 6294	. . . . . . . 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 2486	. . . . . . 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 4460	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
233	232	adantr 465	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
234	181, 217	subcld 9933	. . . . . . . . . 10 |- ( ph -> ( 1 - ( E / N ) ) e. CC )
235		fsumconst 13581	. . . . . . . . . 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 661	. . . . . . . . 9 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
237	236	adantr 465	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
238		0zd 10879	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 e. ZZ )
239	31	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 1 ... N ) )
240	239, 112	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> L e. ZZ )
241	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 e. ZZ )
242	240, 241	zsubcld 10976	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ )
243		elnnuz 11123	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
244	123, 243	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ( ZZ>= ` 1 ) )
245		elfzp12 11763	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( ZZ>= ` 1 ) -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
246	244, 245	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
247	31, 246	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) )
248	247	orcanai 911	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) )
249		1p1e2 10652	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
250	249	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 )
251	250	oveq1d 6293	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
252	248, 251	eleqtrd 2531	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) )
253		elfzle1 11695	. . . . . . . . . . . . . . 15 |- ( L e. ( 2 ... N ) -> 2 <_ L )
254	252, 253	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 <_ L )
255	114	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. RR )
256	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> 2 e. RR )
257	255, 256	subge0d 10145	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) )
258	254, 257	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) )
259	238, 242, 258	3jca 1175	. . . . . . . . . . . 12 |- ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
260		eluz2 11093	. . . . . . . . . . . 12 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
261	259, 260	sylibr 212	. . . . . . . . . . 11 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) )
262		hashfz 12461	. . . . . . . . . . 11 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
263	261, 262	syl 16	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
264		2cn 10609	. . . . . . . . . . . . . . . 16 |- 2 e. CC
265	264	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. CC )
266	145, 265	subcld 9933	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. CC )
267	266	subid1d 9922	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) )
268	267	oveq1d 6293	. . . . . . . . . . . 12 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) )
269	145, 265, 181	subadd23d 9955	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) )
270	264, 173	negsubdi2i 9908	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = ( 1 - 2 )
271		2m1e1 10653	. . . . . . . . . . . . . . . . 17 |- ( 2 - 1 ) = 1
272	271	negeqi 9815	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = -u 1
273	270, 272	eqtr3i 2472	. . . . . . . . . . . . . . 15 |- ( 1 - 2 ) = -u 1
274	273	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 - 2 ) = -u 1 )
275	274	oveq2d 6294	. . . . . . . . . . . . 13 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) )
276	145, 181	negsubd 9939	. . . . . . . . . . . . 13 |- ( ph -> ( L + -u 1 ) = ( L - 1 ) )
277	275, 276	eqtrd 2482	. . . . . . . . . . . 12 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) )
278	268, 269, 277	3eqtrd 2486	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
279	278	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
280	263, 279	eqtrd 2482	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) )
281	280	oveq1d 6293	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) )
282	186, 234	mulcomd 9617	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
283	282	adantr 465	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
284	237, 281, 283	3eqtrd 2486	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
285		fzfid 12059	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin )
286		fzn0 11706	. . . . . . . . 9 |- ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) )
287	261, 286	sylibr 212	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) )
288	125	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR )
289		simpll 753	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph )
290	156	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
291	289, 290, 57	syl2anc 661	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
292	55	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T )
293		elfzelz 11694	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ )
294	293	zred 10971	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR )
295	294	adantl 466	. . . . . . . . . . . . . . 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 9623	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR )
298	14	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR )
299	297, 298	remulcld 9624	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR )
300	114	adantr 465	. . . . . . . . . . . . . . . 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 9990	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
303	302, 296	readdcld 9623	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
304	303, 298	remulcld 9624	. . . . . . . . . . . . 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 532	. . . . . . . . . . . . . . 15 |- ( ph -> ( F : T --> RR /\ S e. T ) )
307	306	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) )
308		ffvelrn 6011	. . . . . . . . . . . . . 14 |- ( ( F : T --> RR /\ S e. T ) -> ( F ` S ) e. RR )
309	307, 308	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F ` S ) e. RR )
310		elfzle2 11696	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) )
311	310	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) )
312	295, 302, 296, 311	leadd1dd 10169	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) )
313	14, 78	jca 532	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E e. RR /\ 0 < E ) )
314	313	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) )
315		lemul1 10397	. . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . 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 210	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) )
318	114, 138	resubcld 9990	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L - 2 ) e. RR )
319	318, 170	readdcld 9623	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
320	319, 14	remulcld 9624	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
321	305, 55	ffvelrnd 6014	. . . . . . . . . . . . . . 15 |- ( ph -> ( F ` S ) e. RR )
322	126, 170	resubcld 9990	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR )
323	322, 14	remulcld 9624	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR )
324		addid1 9760	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 e. CC -> ( 1 + 0 ) = 1 )
325	324	eqcomd 2449	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 e. CC -> 1 = ( 1 + 0 ) )
326	173, 325	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> 1 = ( 1 + 0 ) )
327	181	subidd 9921	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( 1 - 1 ) = 0 )
328	327	eqcomd 2449	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 0 = ( 1 - 1 ) )
329	328	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) )
330		addsubass 9832	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) )
331	330	eqcomd 2449	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
332	181, 181, 181, 331	syl3anc 1227	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
333	326, 329, 332	3eqtrd 2486	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 1 = ( ( 1 + 1 ) - 1 ) )
334	333	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) )
335	249	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 1 ) = 2 )
336	335	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) )
337	336	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) )
338	145, 265, 181	subsubd 9961	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) )
339	334, 337, 338	3eqtrd 2486	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) )
340	339	oveq1d 6293	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) )
341	264, 66, 9	divcli 10289	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 3 ) e. CC
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 / 3 ) e. CC )
343	266, 181, 342	addsubassd 9953	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) )
344	173, 66, 9	divcli 10289	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / 3 ) e. CC
345		df-3 10598	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 3 = ( 2 + 1 )
346	345	oveq1i 6288	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
347	264, 173, 66, 9	divdiri 10304	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
348	346, 67, 347	3eqtr3ri 2479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
349	173, 341, 344, 348	subaddrii 9911	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - ( 2 / 3 ) ) = ( 1 / 3 )
350	349	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) )
351	350	oveq2d 6294	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
352	340, 343, 351	3eqtrd 2486	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
353	137, 7, 9	redivcli 10314	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 / 3 ) e. RR
354	353	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 / 3 ) e. RR )
355		1lt2 10705	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
356	7, 69	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 e. RR /\ 0 < 3 )
357	1, 137, 356	3pm3.2i 1173	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) )
358		ltdiv1 10409	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
359	357, 358	mp1i 12	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
360	355, 359	mpbii 211	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 / 3 ) < ( 2 / 3 ) )
361	170, 354, 126, 360	ltsub2dd 10168	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
362	352, 361	eqbrtrrd 4456	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
363	319, 322, 13, 362	ltmul1dd 11313	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
364	23	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. S e. ( D ` ( L - 1 ) ) )
365	195	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> 1 <_ L )
366	140, 122	readdcld 9623	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. RR )
367	140	lep1d 10480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> N <_ ( N + 1 ) )
368	114, 140, 366, 196, 367	letrd 9739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> L <_ ( N + 1 ) )
369	135	peano2zd 10974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. ZZ )
370		elfz 11684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
372	365, 368, 371	mpbir2and 920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> L e. ( 1 ... ( N + 1 ) ) )
373	145, 181	npcand 9937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( L - 1 ) + 1 ) = L )
374		0p1e1 10650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 1 ) = 1
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( 0 + 1 ) = 1 )
376	375	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
377	372, 373, 376	3eltr4d 2544	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
378		0zd 10879	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> 0 e. ZZ )
379	131, 192	zsubcld 10976	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( L - 1 ) e. ZZ )
380		fzaddel 11724	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
382	377, 381	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( L - 1 ) e. ( 0 ... N ) )
383		rabexg 4584	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
384	33, 383	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
385		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) )
386	385	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
387	386	breq2d 4446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
388	387	rabbidv 3085	. . . . . . . . . . . . . . . . . . . . . . . . 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 5936	. . . . . . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
391	364, 390	neleqtrd 2553	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
392		nfcv 2603	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
393	47, 48, 392	nfbr 4478	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
394	51	breq1d 4444	. . . . . . . . . . . . . . . . . . . . . . 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 3239	. . . . . . . . . . . . . . . . . . . . . 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 304	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
397		ianor 488	. . . . . . . . . . . . . . . . . . . . 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 196	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
399		olc 384	. . . . . . . . . . . . . . . . . . . . 21 |- ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
400	399	anim1i 568	. . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . 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 387	. . . . . . . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . . . . . . . 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 196	. . . . . . . . . . . . . . . . . 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 925	. . . . . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
407	323, 321	ltnled 9732	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
408	406, 407	mpbird 232	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
409	320, 323, 321, 363, 408	lttrd 9743	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
410	320, 321, 409	ltled 9733	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
411	410	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
412	299, 304, 309, 317, 411	letrd 9739	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
413		nfcv 2603	. . . . . . . . . . . . . 14 |- F/_ t ( ( i + ( 1 / 3 ) ) x. E )
414	413, 48, 47	nfbr 4478	. . . . . . . . . . . . 13 |- F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
415	51	breq2d 4446	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
416	44, 45, 414, 415	elrabf 3239	. . . . . . . . . . . 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 664	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
418		rabexg 4584	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
419	33, 418	syl 16	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
420	419	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
421		oveq1 6285	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
422	421	oveq1d 6293	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
423	422	breq1d 4444	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
424	423	rabbidv 3085	. . . . . . . . . . . . 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 5936	. . . . . . . . . . . 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 661	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
428	417, 427	eleqtrrd 2532	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
429	151	3ad2ant1 1016	. . . . . . . . . . . . . 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 212	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) )
431	430, 154	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
432		simp2 996	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
433	431, 432	sseldd 3488	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
434		elex 3102	. . . . . . . . . . . . 13 |- ( S e. ( B ` i ) -> S e. _V )
435	434	3ad2ant3 1018	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
436		nfcv 2603	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( 0 ... N )
437		nfrab1 3022	. . . . . . . . . . . . . . . . . . 19 |- F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
438	436, 437	nfmpt 4522	. . . . . . . . . . . . . . . . . 18 |- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
439	425, 438	nfcxfr 2601	. . . . . . . . . . . . . . . . 17 |- F/_ t B
440		nfcv 2603	. . . . . . . . . . . . . . . . 17 |- F/_ t i
441	439, 440	nffv 5860	. . . . . . . . . . . . . . . 16 |- F/_ t ( B ` i )
442	441	nfel2 2621	. . . . . . . . . . . . . . 15 |- F/ t S e. ( B ` i )
443	94, 95, 442	nf3an 1914	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
444		nfv 1692	. . . . . . . . . . . . . 14 |- F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
445	443, 444	nfim 1904	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
446		eleq1 2513	. . . . . . . . . . . . . . 15 |- ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
447	446	3anbi3d 1304	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
448	99	breq2d 4446	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
449	447, 448	imbi12d 320	. . . . . . . . . . . . 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 3150	. . . . . . . . . . . 12 |- ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
452	435, 451	mpcom 36	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
453	433, 452	syld3an2 1274	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
454	428, 453	mpd3an3 1324	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
455	454	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
456	285, 287, 288, 291, 455	fsumlt 13590	. . . . . . 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 4456	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
458	127	adantr 465	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
459	158	adantr 465	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
460	313	adantr 465	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
461		ltmul2 10396	. . . . . . 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 1227	. . . . . 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 210	. . . . 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 9743	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
465	156, 58	syldan 470	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
466	465	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
467	466	recnd 9622	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
468	285, 467	fsumcl 13531	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
469	468	addid1d 9780	. . . . . 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 9597	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 e. RR )
471		fzfid 12059	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
472	14	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
473		0red 9597	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
474	126	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
475		elfzelz 11694	. . . . . . . . . . . . . . 15 |- ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
476	475	zred 10971	. . . . . . . . . . . . . 14 |- ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
477	476	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
478		1m1e0 10607	. . . . . . . . . . . . . . 15 |- ( 1 - 1 ) = 0
479	122, 114, 122, 365	lesub1dd 10171	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
480	478, 479	syl5eqbrr 4468	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( L - 1 ) )
481	480	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
482		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
483	475	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
484	379	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
485	135	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
486		elfz 11684	. . . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
488	482, 487	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
489	488	simpld 459	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
490	473, 474, 477, 481, 489	letrd 9739	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
491		elfzle2 11696	. . . . . . . . . . . . 13 |- ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
492	491	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
493		0zd 10879	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
494		elfz 11684	. . . . . . . . . . . . 13 |- ( ( i e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
495	483, 493, 485, 494	syl3anc 1227	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
496	490, 492, 495	mpbir2and 920	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
497	496, 57	syldan 470	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
498	472, 497	remulcld 9624	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
499	498	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
500	471, 499	fsumrecl 13532	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
501	285, 466	fsumrecl 13532	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
502		fzfid 12059	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) ... N ) e. Fin )
503	182	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
504	503	mul01d 9779	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
505	496, 106	syldan 470	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
506	313	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
507		lemul2 10398	. . . . . . . . . . . 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 1227	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
509	505, 508	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
510	504, 509	eqbrtrrd 4456	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
511	502, 498, 510	fsumge0 13585	. . . . . . . 8 |- ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
512	511	adantr 465	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
513	470, 500, 501, 512	leadd2dd 10170	. . . . . 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 4456	. . . . 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 9622	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
516	130, 182, 515	fsummulc2 13575	. . . . . 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 465	. . . . 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 11694	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
520	519	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
521	520	zred 10971	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
522	318	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
523	126	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
524		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
525		0zd 10879	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
526	134	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
527		elfz 11684	. . . . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
529	524, 528	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
530	529	simprd 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
531	122, 138, 114	ltsub2d 10165	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
532	355, 531	mpbii 211	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) < ( L - 1 ) )
533	532	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
534	521, 522, 523, 530, 533	lelttrd 9740	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
535	521, 523	ltnled 9732	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) )
536	534, 535	mpbid 210	. . . . . . . . . . . 12 |- (