Theorem stoweidlem26 37832

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 9655	. . . . . . . 8 |- 1 e. RR
2		eleq1 2496	. . . . . . . 8 |- ( L = 1 -> ( L e. RR <-> 1 e. RR ) )
3	1, 2	mpbiri 237	. . . . . . 7 |- ( L = 1 -> L e. RR )
4	3	adantl 468	. . . . . 6 |- ( ( ph /\ L = 1 ) -> L e. RR )
5		4re 10699	. . . . . . . 8 |- 4 e. RR
6	5	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 4 e. RR )
7		3re 10696	. . . . . . . 8 |- 3 e. RR
8	7	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 e. RR )
9		3ne0 10717	. . . . . . . 8 |- 3 =/= 0
10	9	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 =/= 0 )
11	6, 8, 10	redivcld 10448	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
12	4, 11	resubcld 10060	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
13		stoweidlem26.11	. . . . . . 7 |- ( ph -> E e. RR+ )
14	13	rpred 11354	. . . . . 6 |- ( ph -> E e. RR )
15	14	adantr 467	. . . . 5 |- ( ( ph /\ L = 1 ) -> E e. RR )
16	12, 15	remulcld 9684	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
17		0red 9657	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 e. RR )
18		fzfid 12198	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
19	14	adantr 467	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> E e. RR )
20		stoweidlem26.13	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )
21		stoweidlem26.9	. . . . . . . . . . . . . 14 |- ( ph -> S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) )
22		eldif 3452	. . . . . . . . . . . . . 14 |- ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
23	21, 22	sylib 200	. . . . . . . . . . . . 13 |- ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
24	23	simpld 461	. . . . . . . . . . . 12 |- ( ph -> S e. ( D ` L ) )
25		1e0p1 11092	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
26	25	oveq1i 6321	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) = ( ( 0 + 1 ) ... N )
27		0z 10961	. . . . . . . . . . . . . . . 16 |- 0 e. ZZ
28		fzp1ss 11860	. . . . . . . . . . . . . . . 16 |- ( 0 e. ZZ -> ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) )
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( 0 + 1 ) ... N ) C_ ( 0 ... N )
30	26, 29	eqsstri 3500	. . . . . . . . . . . . . 14 |- ( 1 ... N ) C_ ( 0 ... N )
31		stoweidlem26.8	. . . . . . . . . . . . . 14 |- ( ph -> L e. ( 1 ... N ) )
32	30, 31	sseldi 3468	. . . . . . . . . . . . 13 |- ( ph -> L e. ( 0 ... N ) )
33		stoweidlem26.7	. . . . . . . . . . . . . 14 |- ( ph -> T e. _V )
34		rabexg 4580	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
35	33, 34	syl 17	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V )
36		oveq1 6318	. . . . . . . . . . . . . . . . 17 |- ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) )
37	36	oveq1d 6326	. . . . . . . . . . . . . . . 16 |- ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) )
38	37	breq2d 4441	. . . . . . . . . . . . . . 15 |- ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
39	38	rabbidv 3076	. . . . . . . . . . . . . 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 5968	. . . . . . . . . . . . 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 666	. . . . . . . . . . . 12 |- ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
43	24, 42	eleqtrd 2514	. . . . . . . . . . 11 |- ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
44		nfcv 2585	. . . . . . . . . . . 12 |- F/_ t S
45		nfcv 2585	. . . . . . . . . . . 12 |- F/_ t T
46		stoweidlem26.1	. . . . . . . . . . . . . 14 |- F/_ t F
47	46, 44	nffv 5894	. . . . . . . . . . . . 13 |- F/_ t ( F ` S )
48		nfcv 2585	. . . . . . . . . . . . 13 |- F/_ t <_
49		nfcv 2585	. . . . . . . . . . . . 13 |- F/_ t ( ( L - ( 1 / 3 ) ) x. E )
50	47, 48, 49	nfbr 4474	. . . . . . . . . . . 12 |- F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E )
51		fveq2 5887	. . . . . . . . . . . . 13 |- ( t = S -> ( F ` t ) = ( F ` S ) )
52	51	breq1d 4439	. . . . . . . . . . . 12 |- ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
53	44, 45, 50, 52	elrabf 3232	. . . . . . . . . . 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 200	. . . . . . . . . 10 |- ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
55	54	simpld 461	. . . . . . . . 9 |- ( ph -> S e. T )
56	55	adantr 467	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T )
57	20, 56	ffvelrnd 6044	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
58	19, 57	remulcld 9684	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
59	18, 58	fsumrecl 13805	. . . . 5 |- ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
60	59	adantr 467	. . . 4 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
61	5, 7, 9	redivcli 10387	. . . . . . 7 |- ( 4 / 3 ) e. RR
62	61	a1i 11	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
63	4, 62	resubcld 10060	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
64	4	recnd 9682	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> L e. CC )
65	64	subid1d 9988	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) = L )
66		3cn 10697	. . . . . . . . . 10 |- 3 e. CC
67	66, 9	dividi 10353	. . . . . . . . 9 |- ( 3 / 3 ) = 1
68		3lt4 10792	. . . . . . . . . 10 |- 3 < 4
69		3pos 10716	. . . . . . . . . . 11 |- 0 < 3
70	7, 5, 7, 69	ltdiv1ii 10549	. . . . . . . . . 10 |- ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) )
71	68, 70	mpbi 212	. . . . . . . . 9 |- ( 3 / 3 ) < ( 4 / 3 )
72	67, 71	eqbrtrri 4451	. . . . . . . 8 |- 1 < ( 4 / 3 )
73		breq1 4432	. . . . . . . . 9 |- ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
74	73	adantl 468	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
75	72, 74	mpbiri 237	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) )
76	65, 75	eqbrtrd 4450	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) )
77	4, 17, 62, 76	ltsub23d 10231	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 )
78	13	rpgt0d 11357	. . . . . 6 |- ( ph -> 0 < E )
79	78	adantr 467	. . . . 5 |- ( ( ph /\ L = 1 ) -> 0 < E )
80		mulltgt0 37322	. . . . 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 1266	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
82		0cn 9648	. . . . . . . 8 |- 0 e. CC
83		fsumconst 13856	. . . . . . . 8 |- ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
84	18, 82, 83	sylancl 667	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
85		hashcl 12550	. . . . . . . . 9 |- ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 )
86		nn0cn 10892	. . . . . . . . 9 |- ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC )
87	18, 85, 86	3syl 18	. . . . . . . 8 |- ( ph -> ( # ` ( 0 ... N ) ) e. CC )
88	87	mul01d 9845	. . . . . . 7 |- ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 )
89	84, 88	eqtrd 2464	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 )
90	89	adantr 467	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 )
91		0red 9657	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR )
92	13	rpge0d 11358	. . . . . . . . 9 |- ( ph -> 0 <_ E )
93	92	adantr 467	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E )
94		stoweidlem26.3	. . . . . . . . . . . 12 |- F/ t ph
95		nfv 1756	. . . . . . . . . . . 12 |- F/ t i e. ( 0 ... N )
96	94, 95	nfan 1989	. . . . . . . . . . 11 |- F/ t ( ph /\ i e. ( 0 ... N ) )
97		nfv 1756	. . . . . . . . . . 11 |- F/ t 0 <_ ( ( X ` i ) ` S )
98	96, 97	nfim 1981	. . . . . . . . . 10 |- F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
99		fveq2 5887	. . . . . . . . . . . 12 |- ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) )
100	99	breq2d 4441	. . . . . . . . . . 11 |- ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) )
101	100	imbi2d 318	. . . . . . . . . 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 1208	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) )
104	103	com12 33	. . . . . . . . . 10 |- ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) )
105	44, 98, 101, 104	vtoclgaf 3150	. . . . . . . . 9 |- ( S e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) )
106	56, 105	mpcom 38	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
107	19, 57, 93, 106	mulge0d 10203	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
108	18, 91, 58, 107	fsumle 13864	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
109	108	adantr 467	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
110	90, 109	eqbrtrrd 4452	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
111	16, 17, 60, 81, 110	ltletrd 9808	. . 3 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
112		elfzelz 11813	. . . . . . . . 9 |- ( L e. ( 1 ... N ) -> L e. ZZ )
113		zre 10954	. . . . . . . . 9 |- ( L e. ZZ -> L e. RR )
114	31, 112, 113	3syl 18	. . . . . . . 8 |- ( ph -> L e. RR )
115	5	a1i 11	. . . . . . . . 9 |- ( ph -> 4 e. RR )
116	7	a1i 11	. . . . . . . . 9 |- ( ph -> 3 e. RR )
117	9	a1i 11	. . . . . . . . 9 |- ( ph -> 3 =/= 0 )
118	115, 116, 117	redivcld 10448	. . . . . . . 8 |- ( ph -> ( 4 / 3 ) e. RR )
119	114, 118	resubcld 10060	. . . . . . 7 |- ( ph -> ( L - ( 4 / 3 ) ) e. RR )
120	119, 14	remulcld 9684	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
121	120	adantr 467	. . . . 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 10671	. . . . . . . . 9 |- ( ph -> ( E / N ) e. RR )
125	122, 124	resubcld 10060	. . . . . . . 8 |- ( ph -> ( 1 - ( E / N ) ) e. RR )
126	114, 122	resubcld 10060	. . . . . . . 8 |- ( ph -> ( L - 1 ) e. RR )
127	125, 126	remulcld 9684	. . . . . . 7 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
128	14, 127	remulcld 9684	. . . . . 6 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
129	128	adantr 467	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
130		fzfid 12198	. . . . . . . 8 |- ( ph -> ( 0 ... ( L - 2 ) ) e. Fin )
131	31, 112	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> L e. ZZ )
132		2z 10982	. . . . . . . . . . . . . . 15 |- 2 e. ZZ
133	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. ZZ )
134	131, 133	zsubcld 11058	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) e. ZZ )
135	123	nnzd 11052	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
136	131	zred 11053	. . . . . . . . . . . . . . 15 |- ( ph -> L e. RR )
137		2re 10692	. . . . . . . . . . . . . . . 16 |- 2 e. RR
138	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. RR )
139	136, 138	resubcld 10060	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. RR )
140	123	nnred 10637	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
141		0le2 10713	. . . . . . . . . . . . . . . 16 |- 0 <_ 2
142		0red 9657	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. RR )
143	142, 138, 136	lesub2d 10234	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) )
144	141, 143	mpbii 215	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) <_ ( L - 0 ) )
145	131	zcnd 11054	. . . . . . . . . . . . . . . 16 |- ( ph -> L e. CC )
146	145	subid1d 9988	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 0 ) = L )
147	144, 146	breqtrd 4454	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) <_ L )
148		elfzle2 11816	. . . . . . . . . . . . . . 15 |- ( L e. ( 1 ... N ) -> L <_ N )
149	31, 148	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
150	139, 136, 140, 147, 149	letrd 9805	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) <_ N )
151	134, 135, 150	3jca 1186	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
152		eluz2 11178	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
153	151, 152	sylibr 216	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) )
154		fzss2 11851	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` ( L - 2 ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
155	153, 154	syl 17	. . . . . . . . . 10 |- ( ph -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
156	155	sselda 3470	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
157	156, 57	syldan 473	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
158	130, 157	fsumrecl 13805	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
159	14, 158	remulcld 9684	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
160	159	adantr 467	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
161	14, 126	remulcld 9684	. . . . . . . . 9 |- ( ph -> ( E x. ( L - 1 ) ) e. RR )
162	14, 14	remulcld 9684	. . . . . . . . 9 |- ( ph -> ( E x. E ) e. RR )
163	161, 162	resubcld 10060	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR )
164	126, 123	nndivred 10671	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) / N ) e. RR )
165	162, 164	remulcld 9684	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR )
166	161, 165	resubcld 10060	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR )
167	126, 14	resubcld 10060	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) - E ) e. RR )
168	122, 14	readdcld 9683	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) e. RR )
169	1, 7, 9	redivcli 10387	. . . . . . . . . . . . . . 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 9807	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) )
173		ax-1cn 9610	. . . . . . . . . . . . . . 15 |- 1 e. CC
174	66, 173, 66, 9	divdiri 10377	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
175		3p1e4 10748	. . . . . . . . . . . . . . 15 |- ( 3 + 1 ) = 4
176	175	oveq1i 6321	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
177	67	oveq1i 6321	. . . . . . . . . . . . . 14 |- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
178	174, 176, 177	3eqtr3ri 2461	. . . . . . . . . . . . 13 |- ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
179	172, 178	syl6breq 4469	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) < ( 4 / 3 ) )
180	168, 118, 114, 179	ltsub2dd 10239	. . . . . . . . . . 11 |- ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) )
181	173	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. CC )
182	13	rpcnd 11356	. . . . . . . . . . . 12 |- ( ph -> E e. CC )
183	145, 181, 182	subsub4d 10030	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) )
184	180, 183	breqtrrd 4456	. . . . . . . . . 10 |- ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) )
185	119, 167, 13, 184	ltmul1dd 11406	. . . . . . . . 9 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) )
186	145, 181	subcld 9999	. . . . . . . . . . . 12 |- ( ph -> ( L - 1 ) e. CC )
187	186, 182	subcld 9999	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) e. CC )
188	182, 187	mulcomd 9677	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) )
189	182, 186, 182	subdid 10087	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
190	188, 189	eqtr3d 2466	. . . . . . . . 9 |- ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
191	185, 190	breqtrd 4454	. . . . . . . 8 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
192		1zzd 10981	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. ZZ )
193		elfz 11803	. . . . . . . . . . . . . . . . 17 |- ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
194	131, 192, 135, 193	syl3anc 1265	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
195	31, 194	mpbid 214	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 <_ L /\ L <_ N ) )
196	195	simprd 465	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
197		zlem1lt 11001	. . . . . . . . . . . . . . 15 |- ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
198	131, 135, 197	syl2anc 666	. . . . . . . . . . . . . 14 |- ( ph -> ( L <_ N <-> ( L - 1 ) < N ) )
199	196, 198	mpbid 214	. . . . . . . . . . . . 13 |- ( ph -> ( L - 1 ) < N )
200	123	nngt0d 10666	. . . . . . . . . . . . . 14 |- ( ph -> 0 < N )
201		ltdiv1 10482	. . . . . . . . . . . . . 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 1269	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
203	199, 202	mpbid 214	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 1 ) / N ) < ( N / N ) )
204	123	nncnd 10638	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
205	123	nnne0d 10667	. . . . . . . . . . . . 13 |- ( ph -> N =/= 0 )
206	204, 205	dividd 10394	. . . . . . . . . . . 12 |- ( ph -> ( N / N ) = 1 )
207	203, 206	breqtrd 4454	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) < 1 )
208	14, 14, 78, 78	mulgt0d 9803	. . . . . . . . . . . 12 |- ( ph -> 0 < ( E x. E ) )
209		ltmul2 10469	. . . . . . . . . . . 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 1269	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
211	207, 210	mpbid 214	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) )
212	182, 182	mulcld 9676	. . . . . . . . . . 11 |- ( ph -> ( E x. E ) e. CC )
213	212	mulid1d 9673	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) )
214	211, 213	breqtrd 4454	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) )
215	165, 162, 161, 214	ltsub2dd 10239	. . . . . . . 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 9809	. . . . . . 7 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
217	182, 204, 205	divcld 10396	. . . . . . . . . . 11 |- ( ph -> ( E / N ) e. CC )
218	181, 217, 186	subdird 10088	. . . . . . . . . 10 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) )
219	186	mulid2d 9674	. . . . . . . . . . 11 |- ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) )
220	219	oveq1d 6326	. . . . . . . . . 10 |- ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
221	218, 220	eqtrd 2464	. . . . . . . . 9 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
222	221	oveq2d 6327	. . . . . . . 8 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) )
223	217, 186	mulcld 9676	. . . . . . . . 9 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC )
224	182, 186, 223	subdid 10087	. . . . . . . 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 10419	. . . . . . . . . . 11 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) )
226	225	oveq2d 6327	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
227	186, 204, 205	divcld 10396	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) e. CC )
228	182, 182, 227	mulassd 9679	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
229	226, 228	eqtr4d 2467	. . . . . . . . 9 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) )
230	229	oveq2d 6327	. . . . . . . 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 2468	. . . . . . 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 4456	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
233	232	adantr 467	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
234	181, 217	subcld 9999	. . . . . . . . . 10 |- ( ph -> ( 1 - ( E / N ) ) e. CC )
235		fsumconst 13856	. . . . . . . . . 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 666	. . . . . . . . 9 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
237	236	adantr 467	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
238		0zd 10962	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 e. ZZ )
239	31	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 1 ... N ) )
240	239, 112	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> L e. ZZ )
241	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 e. ZZ )
242	240, 241	zsubcld 11058	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ )
243		elnnuz 11208	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
244	123, 243	sylib 200	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ( ZZ>= ` 1 ) )
245		elfzp12 11886	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( ZZ>= ` 1 ) -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) )
247	31, 246	mpbid 214	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) )
248	247	orcanai 922	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) )
249		1p1e2 10736	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
250	249	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 )
251	250	oveq1d 6326	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
252	248, 251	eleqtrd 2514	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) )
253		elfzle1 11815	. . . . . . . . . . . . . . 15 |- ( L e. ( 2 ... N ) -> 2 <_ L )
254	252, 253	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 <_ L )
255	114	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. RR )
256	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> 2 e. RR )
257	255, 256	subge0d 10216	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) )
258	254, 257	mpbird 236	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) )
259	238, 242, 258	3jca 1186	. . . . . . . . . . . 12 |- ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
260		eluz2 11178	. . . . . . . . . . . 12 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
261	259, 260	sylibr 216	. . . . . . . . . . 11 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) )
262		hashfz 12609	. . . . . . . . . . 11 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
263	261, 262	syl 17	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) )
264		2cn 10693	. . . . . . . . . . . . . . . 16 |- 2 e. CC
265	264	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. CC )
266	145, 265	subcld 9999	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. CC )
267	266	subid1d 9988	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) )
268	267	oveq1d 6326	. . . . . . . . . . . 12 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) )
269	145, 265, 181	subadd23d 10021	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) )
270	264, 173	negsubdi2i 9974	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = ( 1 - 2 )
271		2m1e1 10737	. . . . . . . . . . . . . . . . 17 |- ( 2 - 1 ) = 1
272	271	negeqi 9881	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = -u 1
273	270, 272	eqtr3i 2454	. . . . . . . . . . . . . . 15 |- ( 1 - 2 ) = -u 1
274	273	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 - 2 ) = -u 1 )
275	274	oveq2d 6327	. . . . . . . . . . . . 13 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) )
276	145, 181	negsubd 10005	. . . . . . . . . . . . 13 |- ( ph -> ( L + -u 1 ) = ( L - 1 ) )
277	275, 276	eqtrd 2464	. . . . . . . . . . . 12 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) )
278	268, 269, 277	3eqtrd 2468	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
279	278	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
280	263, 279	eqtrd 2464	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) )
281	280	oveq1d 6326	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) )
282	186, 234	mulcomd 9677	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
283	282	adantr 467	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
284	237, 281, 283	3eqtrd 2468	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
285		fzfid 12198	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin )
286		fzn0 11826	. . . . . . . . 9 |- ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) )
287	261, 286	sylibr 216	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) )
288	125	ad2antrr 731	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR )
289		simpll 759	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph )
290	156	adantlr 720	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
291	289, 290, 57	syl2anc 666	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
292	55	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T )
293		elfzelz 11813	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ )
294	293	zred 11053	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR )
295	294	adantl 468	. . . . . . . . . . . . . . 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 9683	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR )
298	14	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR )
299	297, 298	remulcld 9684	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR )
300	114	adantr 467	. . . . . . . . . . . . . . . 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 10060	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
303	302, 296	readdcld 9683	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
304	303, 298	remulcld 9684	. . . . . . . . . . . . 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 535	. . . . . . . . . . . . . . 15 |- ( ph -> ( F : T --> RR /\ S e. T ) )
307	306	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) )
308		ffvelrn 6041	. . . . . . . . . . . . . 14 |- ( ( F : T --> RR /\ S e. T ) -> ( F ` S ) e. RR )
309	307, 308	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F ` S ) e. RR )
310		elfzle2 11816	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) )
311	310	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) )
312	295, 302, 296, 311	leadd1dd 10240	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) )
313	14, 78	jca 535	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E e. RR /\ 0 < E ) )
314	313	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) )
315		lemul1 10470	. . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . 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 214	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) )
318	114, 138	resubcld 10060	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L - 2 ) e. RR )
319	318, 170	readdcld 9683	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
320	319, 14	remulcld 9684	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
321	305, 55	ffvelrnd 6044	. . . . . . . . . . . . . . 15 |- ( ph -> ( F ` S ) e. RR )
322	126, 170	resubcld 10060	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR )
323	322, 14	remulcld 9684	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR )
324		addid1 9826	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 e. CC -> ( 1 + 0 ) = 1 )
325	324	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 e. CC -> 1 = ( 1 + 0 ) )
326	173, 325	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> 1 = ( 1 + 0 ) )
327	181	subidd 9987	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( 1 - 1 ) = 0 )
328	327	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 0 = ( 1 - 1 ) )
329	328	oveq2d 6327	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) )
330		addsubass 9898	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) )
331	330	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
332	181, 181, 181, 331	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
333	326, 329, 332	3eqtrd 2468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 1 = ( ( 1 + 1 ) - 1 ) )
334	333	oveq2d 6327	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) )
335	249	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 1 ) = 2 )
336	335	oveq1d 6326	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) )
337	336	oveq2d 6327	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) )
338	145, 265, 181	subsubd 10027	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) )
339	334, 337, 338	3eqtrd 2468	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) )
340	339	oveq1d 6326	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) )
341	264, 66, 9	divcli 10362	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 3 ) e. CC
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 / 3 ) e. CC )
343	266, 181, 342	addsubassd 10019	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) )
344	173, 66, 9	divcli 10362	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / 3 ) e. CC
345		df-3 10682	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 3 = ( 2 + 1 )
346	345	oveq1i 6321	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
347	264, 173, 66, 9	divdiri 10377	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
348	346, 67, 347	3eqtr3ri 2461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
349	173, 341, 344, 348	subaddrii 9977	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - ( 2 / 3 ) ) = ( 1 / 3 )
350	349	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) )
351	350	oveq2d 6327	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
352	340, 343, 351	3eqtrd 2468	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
353	137, 7, 9	redivcli 10387	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 / 3 ) e. RR
354	353	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 / 3 ) e. RR )
355		1lt2 10789	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
356	7, 69	pm3.2i 457	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 e. RR /\ 0 < 3 )
357	1, 137, 356	3pm3.2i 1184	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) )
358		ltdiv1 10482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
359	357, 358	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) )
360	355, 359	mpbii 215	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 / 3 ) < ( 2 / 3 ) )
361	170, 354, 126, 360	ltsub2dd 10239	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
362	352, 361	eqbrtrrd 4452	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
363	319, 322, 13, 362	ltmul1dd 11406	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
364	23	simprd 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. S e. ( D ` ( L - 1 ) ) )
365	195	simpld 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> 1 <_ L )
366	140, 122	readdcld 9683	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. RR )
367	140	lep1d 10551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> N <_ ( N + 1 ) )
368	114, 140, 366, 196, 367	letrd 9805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> L <_ ( N + 1 ) )
369	135	peano2zd 11056	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. ZZ )
370		elfz 11803	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
372	365, 368, 371	mpbir2and 931	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> L e. ( 1 ... ( N + 1 ) ) )
373	145, 181	npcand 10003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( L - 1 ) + 1 ) = L )
374		0p1e1 10734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 1 ) = 1
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( 0 + 1 ) = 1 )
376	375	oveq1d 6326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
377	372, 373, 376	3eltr4d 2527	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
378		0zd 10962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> 0 e. ZZ )
379	131, 192	zsubcld 11058	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( L - 1 ) e. ZZ )
380		fzaddel 11846	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1266	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
382	377, 381	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( L - 1 ) e. ( 0 ... N ) )
383		rabexg 4580	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
384	33, 383	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V )
385		oveq1 6318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) )
386	385	oveq1d 6326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
387	386	breq2d 4441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
388	387	rabbidv 3076	. . . . . . . . . . . . . . . . . . . . . . . . 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 5968	. . . . . . . . . . . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
391	364, 390	neleqtrd 2535	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
392		nfcv 2585	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
393	47, 48, 392	nfbr 4474	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
394	51	breq1d 4439	. . . . . . . . . . . . . . . . . . . . . . 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 3232	. . . . . . . . . . . . . . . . . . . . . 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 306	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
397		ianor 491	. . . . . . . . . . . . . . . . . . . . 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 200	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
399		olc 386	. . . . . . . . . . . . . . . . . . . . 21 |- ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
400	399	anim1i 571	. . . . . . . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . . . . . . 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 389	. . . . . . . . . . . . . . . . . . . 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 699	. . . . . . . . . . . . . . . . . . 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 200	. . . . . . . . . . . . . . . . . 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 936	. . . . . . . . . . . . . . . . . 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 216	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
407	323, 321	ltnled 9795	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
408	406, 407	mpbird 236	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
409	320, 323, 321, 363, 408	lttrd 9809	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
410	320, 321, 409	ltled 9796	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
411	410	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
412	299, 304, 309, 317, 411	letrd 9805	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
413		nfcv 2585	. . . . . . . . . . . . . 14 |- F/_ t ( ( i + ( 1 / 3 ) ) x. E )
414	413, 48, 47	nfbr 4474	. . . . . . . . . . . . 13 |- F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
415	51	breq2d 4441	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
416	44, 45, 414, 415	elrabf 3232	. . . . . . . . . . . 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 669	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
418		rabexg 4580	. . . . . . . . . . . . . 14 |- ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
419	33, 418	syl 17	. . . . . . . . . . . . 13 |- ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
420	419	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
421		oveq1 6318	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
422	421	oveq1d 6326	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
423	422	breq1d 4439	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
424	423	rabbidv 3076	. . . . . . . . . . . . 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 5968	. . . . . . . . . . . 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 666	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
428	417, 427	eleqtrrd 2515	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
429	151	3ad2ant1 1027	. . . . . . . . . . . . . 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 216	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) )
431	430, 154	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) )
432		simp2 1007	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
433	431, 432	sseldd 3471	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
434		elex 3094	. . . . . . . . . . . . 13 |- ( S e. ( B ` i ) -> S e. _V )
435	434	3ad2ant3 1029	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
436		nfcv 2585	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( 0 ... N )
437		nfrab1 3011	. . . . . . . . . . . . . . . . . . 19 |- F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
438	436, 437	nfmpt 4518	. . . . . . . . . . . . . . . . . 18 |- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
439	425, 438	nfcxfr 2583	. . . . . . . . . . . . . . . . 17 |- F/_ t B
440		nfcv 2585	. . . . . . . . . . . . . . . . 17 |- F/_ t i
441	439, 440	nffv 5894	. . . . . . . . . . . . . . . 16 |- F/_ t ( B ` i )
442	441	nfel2 2603	. . . . . . . . . . . . . . 15 |- F/ t S e. ( B ` i )
443	94, 95, 442	nf3an 1991	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
444		nfv 1756	. . . . . . . . . . . . . 14 |- F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
445	443, 444	nfim 1981	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
446		eleq1 2496	. . . . . . . . . . . . . . 15 |- ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
447	446	3anbi3d 1342	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
448	99	breq2d 4441	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
449	447, 448	imbi12d 322	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) ) )
450		stoweidlem26.15	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )
451	445, 449, 450	vtoclg1f 3144	. . . . . . . . . . . 12 |- ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
452	435, 451	mpcom 38	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
453	433, 452	syld3an2 1312	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
454	428, 453	mpd3an3 1362	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
455	454	adantlr 720	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
456	285, 287, 288, 291, 455	fsumlt 13865	. . . . . . 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 4452	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
458	127	adantr 467	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
459	158	adantr 467	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
460	313	adantr 467	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
461		ltmul2 10469	. . . . . . 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 1265	. . . . . 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 214	. . . . 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 9809	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
465	156, 58	syldan 473	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
466	465	adantlr 720	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
467	466	recnd 9682	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
468	285, 467	fsumcl 13804	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
469	468	addid1d 9846	. . . . . 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 9657	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 e. RR )
471		fzfid 12198	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
472	14	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
473		0red 9657	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
474	126	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
475		elfzelz 11813	. . . . . . . . . . . . . . 15 |- ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
476	475	zred 11053	. . . . . . . . . . . . . 14 |- ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
477	476	adantl 468	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
478		1m1e0 10691	. . . . . . . . . . . . . . 15 |- ( 1 - 1 ) = 0
479	122, 114, 122, 365	lesub1dd 10242	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
480	478, 479	syl5eqbrr 4464	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( L - 1 ) )
481	480	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
482		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
483	475	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
484	379	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
485	135	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
486		elfz 11803	. . . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
488	482, 487	mpbid 214	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
489	488	simpld 461	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
490	473, 474, 477, 481, 489	letrd 9805	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
491		elfzle2 11816	. . . . . . . . . . . . 13 |- ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
492	491	adantl 468	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
493		0zd 10962	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
494		elfz 11803	. . . . . . . . . . . . 13 |- ( ( i e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
495	483, 493, 485, 494	syl3anc 1265	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
496	490, 492, 495	mpbir2and 931	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
497	496, 57	syldan 473	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
498	472, 497	remulcld 9684	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
499	498	adantlr 720	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
500	471, 499	fsumrecl 13805	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
501	285, 466	fsumrecl 13805	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
502		fzfid 12198	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) ... N ) e. Fin )
503	182	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
504	503	mul01d 9845	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
505	496, 106	syldan 473	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
506	313	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
507		lemul2 10471	. . . . . . . . . . . 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 1265	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
509	505, 508	mpbid 214	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
510	504, 509	eqbrtrrd 4452	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
511	502, 498, 510	fsumge0 13860	. . . . . . . 8 |- ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
512	511	adantr 467	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
513	470, 500, 501, 512	leadd2dd 10241	. . . . . 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 4452	. . . . 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 9682	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
516	130, 182, 515	fsummulc2 13850	. . . . . 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 467	. . . . 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 11813	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
520	519	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
521	520	zred 11053	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
522	318	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
523	126	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
524		simpr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
525		0zd 10962	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
526	134	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
527		elfz 11803	. . . . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
529	524, 528	mpbid 214	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
530	529	simprd 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
531	122, 138, 114	ltsub2d 10236	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
532	355, 531	mpbii 215	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) < ( L - 1 ) )
533	532	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
534	521, 522, 523, 530, 533	lelttrd 9806	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
535	521, 523	ltnled 9795	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) )
536	534, 535	mpbid 214	. . . . . . . . . . . 12 |- ( ( ph