Theorem stoweidlem26 40243

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 10039	. . . . . . . 8 |- 1 e. RR
2		eleq1 2689	. . . . . . . 8 |- ( L = 1 -> ( L e. RR <-> 1 e. RR ) )
3	1, 2	mpbiri 248	. . . . . . 7 |- ( L = 1 -> L e. RR )
4	3	adantl 482	. . . . . 6 |- ( ( ph /\ L = 1 ) -> L e. RR )
5		4re 11097	. . . . . . . 8 |- 4 e. RR
6	5	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 4 e. RR )
7		3re 11094	. . . . . . . 8 |- 3 e. RR
8	7	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 e. RR )
9		3ne0 11115	. . . . . . . 8 |- 3 =/= 0
10	9	a1i 11	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> 3 =/= 0 )
11	6, 8, 10	redivcld 10853	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
12	4, 11	resubcld 10458	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
13		stoweidlem26.11	. . . . . . 7 |- ( ph -> E e. RR+ )
14	13	rpred 11872	. . . . . 6 |- ( ph -> E e. RR )
15	14	adantr 481	. . . . 5 |- ( ( ph /\ L = 1 ) -> E e. RR )
16	12, 15	remulcld 10070	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
17		0red 10041	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 e. RR )
18		fzfid 12772	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
19	14	adantr 481	. . . . . . 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 3584	. . . . . . . . . . . . . 14 |- ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
23	21, 22	sylib 208	. . . . . . . . . . . . 13 |- ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) )
24	23	simpld 475	. . . . . . . . . . . 12 |- ( ph -> S e. ( D ` L ) )
25		1e0p1 11552	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
26	25	oveq1i 6660	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) = ( ( 0 + 1 ) ... N )
27		0z 11388	. . . . . . . . . . . . . . . 16 |- 0 e. ZZ
28		fzp1ss 12392	. . . . . . . . . . . . . . . 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 3635	. . . . . . . . . . . . . 14 |- ( 1 ... N ) C_ ( 0 ... N )
31		stoweidlem26.8	. . . . . . . . . . . . . 14 |- ( ph -> L e. ( 1 ... N ) )
32	30, 31	sseldi 3601	. . . . . . . . . . . . 13 |- ( ph -> L e. ( 0 ... N ) )
33		stoweidlem26.7	. . . . . . . . . . . . . 14 |- ( ph -> T e. _V )
34		rabexg 4812	. . . . . . . . . . . . . 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 6657	. . . . . . . . . . . . . . . . 17 |- ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) )
37	36	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) )
38	37	breq2d 4665	. . . . . . . . . . . . . . 15 |- ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
39	38	rabbidv 3189	. . . . . . . . . . . . . 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 6280	. . . . . . . . . . . . 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 693	. . . . . . . . . . . 12 |- ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
43	24, 42	eleqtrd 2703	. . . . . . . . . . 11 |- ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } )
44		nfcv 2764	. . . . . . . . . . . 12 |- F/_ t S
45		nfcv 2764	. . . . . . . . . . . 12 |- F/_ t T
46		stoweidlem26.1	. . . . . . . . . . . . . 14 |- F/_ t F
47	46, 44	nffv 6198	. . . . . . . . . . . . 13 |- F/_ t ( F ` S )
48		nfcv 2764	. . . . . . . . . . . . 13 |- F/_ t <_
49		nfcv 2764	. . . . . . . . . . . . 13 |- F/_ t ( ( L - ( 1 / 3 ) ) x. E )
50	47, 48, 49	nfbr 4699	. . . . . . . . . . . 12 |- F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E )
51		fveq2 6191	. . . . . . . . . . . . 13 |- ( t = S -> ( F ` t ) = ( F ` S ) )
52	51	breq1d 4663	. . . . . . . . . . . 12 |- ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
53	44, 45, 50, 52	elrabf 3360	. . . . . . . . . . 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 208	. . . . . . . . . 10 |- ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) )
55	54	simpld 475	. . . . . . . . 9 |- ( ph -> S e. T )
56	55	adantr 481	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T )
57	20, 56	ffvelrnd 6360	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
58	19, 57	remulcld 10070	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
59	18, 58	fsumrecl 14465	. . . . 5 |- ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
60	59	adantr 481	. . . 4 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
61	5, 7, 9	redivcli 10792	. . . . . . 7 |- ( 4 / 3 ) e. RR
62	61	a1i 11	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR )
63	4, 62	resubcld 10458	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR )
64	4	recnd 10068	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> L e. CC )
65	64	subid1d 10381	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) = L )
66		3cn 11095	. . . . . . . . . 10 |- 3 e. CC
67	66, 9	dividi 10758	. . . . . . . . 9 |- ( 3 / 3 ) = 1
68		3lt4 11197	. . . . . . . . . 10 |- 3 < 4
69		3pos 11114	. . . . . . . . . . 11 |- 0 < 3
70	7, 5, 7, 69	ltdiv1ii 10953	. . . . . . . . . 10 |- ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) )
71	68, 70	mpbi 220	. . . . . . . . 9 |- ( 3 / 3 ) < ( 4 / 3 )
72	67, 71	eqbrtrri 4676	. . . . . . . 8 |- 1 < ( 4 / 3 )
73		breq1 4656	. . . . . . . . 9 |- ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
74	73	adantl 482	. . . . . . . 8 |- ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) )
75	72, 74	mpbiri 248	. . . . . . 7 |- ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) )
76	65, 75	eqbrtrd 4675	. . . . . 6 |- ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) )
77	4, 17, 62, 76	ltsub23d 10632	. . . . 5 |- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 )
78	13	rpgt0d 11875	. . . . . 6 |- ( ph -> 0 < E )
79	78	adantr 481	. . . . 5 |- ( ( ph /\ L = 1 ) -> 0 < E )
80		mulltgt0 39181	. . . . 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 1327	. . . 4 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 )
82		0cn 10032	. . . . . . . 8 |- 0 e. CC
83		fsumconst 14522	. . . . . . . 8 |- ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
84	18, 82, 83	sylancl 694	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) )
85		hashcl 13147	. . . . . . . . 9 |- ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 )
86		nn0cn 11302	. . . . . . . . 9 |- ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC )
87	18, 85, 86	3syl 18	. . . . . . . 8 |- ( ph -> ( # ` ( 0 ... N ) ) e. CC )
88	87	mul01d 10235	. . . . . . 7 |- ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 )
89	84, 88	eqtrd 2656	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 )
90	89	adantr 481	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 )
91		0red 10041	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR )
92	13	rpge0d 11876	. . . . . . . . 9 |- ( ph -> 0 <_ E )
93	92	adantr 481	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E )
94		stoweidlem26.3	. . . . . . . . . . . 12 |- F/ t ph
95		nfv 1843	. . . . . . . . . . . 12 |- F/ t i e. ( 0 ... N )
96	94, 95	nfan 1828	. . . . . . . . . . 11 |- F/ t ( ph /\ i e. ( 0 ... N ) )
97		nfv 1843	. . . . . . . . . . 11 |- F/ t 0 <_ ( ( X ` i ) ` S )
98	96, 97	nfim 1825	. . . . . . . . . 10 |- F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
99		fveq2 6191	. . . . . . . . . . . 12 |- ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) )
100	99	breq2d 4665	. . . . . . . . . . 11 |- ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) )
101	100	imbi2d 330	. . . . . . . . . 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 1267	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) )
104	103	com12 32	. . . . . . . . . 10 |- ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) )
105	44, 98, 101, 104	vtoclgaf 3271	. . . . . . . . 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 10604	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
108	18, 91, 58, 107	fsumle 14531	. . . . . 6 |- ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
109	108	adantr 481	. . . . 5 |- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
110	90, 109	eqbrtrrd 4677	. . . 4 |- ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
111	16, 17, 60, 81, 110	ltletrd 10197	. . 3 |- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
112		elfzelz 12342	. . . . . . . . 9 |- ( L e. ( 1 ... N ) -> L e. ZZ )
113		zre 11381	. . . . . . . . 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 10853	. . . . . . . 8 |- ( ph -> ( 4 / 3 ) e. RR )
119	114, 118	resubcld 10458	. . . . . . 7 |- ( ph -> ( L - ( 4 / 3 ) ) e. RR )
120	119, 14	remulcld 10070	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR )
121	120	adantr 481	. . . . 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 11069	. . . . . . . . 9 |- ( ph -> ( E / N ) e. RR )
125	122, 124	resubcld 10458	. . . . . . . 8 |- ( ph -> ( 1 - ( E / N ) ) e. RR )
126	114, 122	resubcld 10458	. . . . . . . 8 |- ( ph -> ( L - 1 ) e. RR )
127	125, 126	remulcld 10070	. . . . . . 7 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
128	14, 127	remulcld 10070	. . . . . 6 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
129	128	adantr 481	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR )
130		fzfid 12772	. . . . . . . 8 |- ( ph -> ( 0 ... ( L - 2 ) ) e. Fin )
131	31, 112	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> L e. ZZ )
132		2z 11409	. . . . . . . . . . . . . . 15 |- 2 e. ZZ
133	132	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. ZZ )
134	131, 133	zsubcld 11487	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) e. ZZ )
135	123	nnzd 11481	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
136	131	zred 11482	. . . . . . . . . . . . . . 15 |- ( ph -> L e. RR )
137		2re 11090	. . . . . . . . . . . . . . . 16 |- 2 e. RR
138	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. RR )
139	136, 138	resubcld 10458	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. RR )
140	123	nnred 11035	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
141		0le2 11111	. . . . . . . . . . . . . . . 16 |- 0 <_ 2
142		0red 10041	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 e. RR )
143	142, 138, 136	lesub2d 10635	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) )
144	141, 143	mpbii 223	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) <_ ( L - 0 ) )
145	131	zcnd 11483	. . . . . . . . . . . . . . . 16 |- ( ph -> L e. CC )
146	145	subid1d 10381	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 0 ) = L )
147	144, 146	breqtrd 4679	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) <_ L )
148		elfzle2 12345	. . . . . . . . . . . . . . 15 |- ( L e. ( 1 ... N ) -> L <_ N )
149	31, 148	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
150	139, 136, 140, 147, 149	letrd 10194	. . . . . . . . . . . . 13 |- ( ph -> ( L - 2 ) <_ N )
151	134, 135, 150	3jca 1242	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
152		eluz2 11693	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) )
153	151, 152	sylibr 224	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) )
154		fzss2 12381	. . . . . . . . . . 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 3603	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
157	156, 57	syldan 487	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
158	130, 157	fsumrecl 14465	. . . . . . 7 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
159	14, 158	remulcld 10070	. . . . . 6 |- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
160	159	adantr 481	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR )
161	14, 126	remulcld 10070	. . . . . . . . 9 |- ( ph -> ( E x. ( L - 1 ) ) e. RR )
162	14, 14	remulcld 10070	. . . . . . . . 9 |- ( ph -> ( E x. E ) e. RR )
163	161, 162	resubcld 10458	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR )
164	126, 123	nndivred 11069	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) / N ) e. RR )
165	162, 164	remulcld 10070	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR )
166	161, 165	resubcld 10458	. . . . . . . 8 |- ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR )
167	126, 14	resubcld 10458	. . . . . . . . . 10 |- ( ph -> ( ( L - 1 ) - E ) e. RR )
168	122, 14	readdcld 10069	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) e. RR )
169	1, 7, 9	redivcli 10792	. . . . . . . . . . . . . . 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 10196	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) )
173		ax-1cn 9994	. . . . . . . . . . . . . . 15 |- 1 e. CC
174	66, 173, 66, 9	divdiri 10782	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
175		3p1e4 11153	. . . . . . . . . . . . . . 15 |- ( 3 + 1 ) = 4
176	175	oveq1i 6660	. . . . . . . . . . . . . 14 |- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
177	67	oveq1i 6660	. . . . . . . . . . . . . 14 |- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
178	174, 176, 177	3eqtr3ri 2653	. . . . . . . . . . . . 13 |- ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
179	172, 178	syl6breq 4694	. . . . . . . . . . . 12 |- ( ph -> ( 1 + E ) < ( 4 / 3 ) )
180	168, 118, 114, 179	ltsub2dd 10640	. . . . . . . . . . 11 |- ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) )
181	173	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. CC )
182	13	rpcnd 11874	. . . . . . . . . . . 12 |- ( ph -> E e. CC )
183	145, 181, 182	subsub4d 10423	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) )
184	180, 183	breqtrrd 4681	. . . . . . . . . 10 |- ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) )
185	119, 167, 13, 184	ltmul1dd 11927	. . . . . . . . 9 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) )
186	145, 181	subcld 10392	. . . . . . . . . . . 12 |- ( ph -> ( L - 1 ) e. CC )
187	186, 182	subcld 10392	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) - E ) e. CC )
188	182, 187	mulcomd 10061	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) )
189	182, 186, 182	subdid 10486	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
190	188, 189	eqtr3d 2658	. . . . . . . . 9 |- ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
191	185, 190	breqtrd 4679	. . . . . . . 8 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) )
192		1zzd 11408	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. ZZ )
193		elfz 12332	. . . . . . . . . . . . . . . . 17 |- ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
194	131, 192, 135, 193	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) )
195	31, 194	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 <_ L /\ L <_ N ) )
196	195	simprd 479	. . . . . . . . . . . . . 14 |- ( ph -> L <_ N )
197		zlem1lt 11429	. . . . . . . . . . . . . . 15 |- ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
198	131, 135, 197	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( L <_ N <-> ( L - 1 ) < N ) )
199	196, 198	mpbid 222	. . . . . . . . . . . . 13 |- ( ph -> ( L - 1 ) < N )
200	123	nngt0d 11064	. . . . . . . . . . . . . 14 |- ( ph -> 0 < N )
201		ltdiv1 10887	. . . . . . . . . . . . . 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 1330	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) )
203	199, 202	mpbid 222	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 1 ) / N ) < ( N / N ) )
204	123	nncnd 11036	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
205	123	nnne0d 11065	. . . . . . . . . . . . 13 |- ( ph -> N =/= 0 )
206	204, 205	dividd 10799	. . . . . . . . . . . 12 |- ( ph -> ( N / N ) = 1 )
207	203, 206	breqtrd 4679	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) < 1 )
208	14, 14, 78, 78	mulgt0d 10192	. . . . . . . . . . . 12 |- ( ph -> 0 < ( E x. E ) )
209		ltmul2 10874	. . . . . . . . . . . 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 1330	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) )
211	207, 210	mpbid 222	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) )
212	182, 182	mulcld 10060	. . . . . . . . . . 11 |- ( ph -> ( E x. E ) e. CC )
213	212	mulid1d 10057	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) )
214	211, 213	breqtrd 4679	. . . . . . . . 9 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) )
215	165, 162, 161, 214	ltsub2dd 10640	. . . . . . . 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 10198	. . . . . . 7 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) )
217	182, 204, 205	divcld 10801	. . . . . . . . . . 11 |- ( ph -> ( E / N ) e. CC )
218	181, 217, 186	subdird 10487	. . . . . . . . . 10 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) )
219	186	mulid2d 10058	. . . . . . . . . . 11 |- ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) )
220	219	oveq1d 6665	. . . . . . . . . 10 |- ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
221	218, 220	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) )
222	221	oveq2d 6666	. . . . . . . 8 |- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) )
223	217, 186	mulcld 10060	. . . . . . . . 9 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC )
224	182, 186, 223	subdid 10486	. . . . . . . 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 10824	. . . . . . . . . . 11 |- ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) )
226	225	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
227	186, 204, 205	divcld 10801	. . . . . . . . . . 11 |- ( ph -> ( ( L - 1 ) / N ) e. CC )
228	182, 182, 227	mulassd 10063	. . . . . . . . . 10 |- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) )
229	226, 228	eqtr4d 2659	. . . . . . . . 9 |- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) )
230	229	oveq2d 6666	. . . . . . . 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 2660	. . . . . . 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 4681	. . . . . 6 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
233	232	adantr 481	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) )
234	181, 217	subcld 10392	. . . . . . . . . 10 |- ( ph -> ( 1 - ( E / N ) ) e. CC )
235		fsumconst 14522	. . . . . . . . . 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 693	. . . . . . . . 9 |- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
237	236	adantr 481	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) )
238		0zd 11389	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 e. ZZ )
239	31	adantr 481	. . . . . . . . . . . . . . 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 11487	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ )
243		elnnuz 11724	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
244	123, 243	sylib 208	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ( ZZ>= ` 1 ) )
245		elfzp12 12419	. . . . . . . . . . . . . . . . . . 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 222	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) )
248	247	orcanai 952	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) )
249		1p1e2 11134	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
250	249	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 )
251	250	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
252	248, 251	eleqtrd 2703	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) )
253		elfzle1 12344	. . . . . . . . . . . . . . 15 |- ( L e. ( 2 ... N ) -> 2 <_ L )
254	252, 253	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> 2 <_ L )
255	114	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> L e. RR )
256	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. L = 1 ) -> 2 e. RR )
257	255, 256	subge0d 10617	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) )
258	254, 257	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) )
259	238, 242, 258	3jca 1242	. . . . . . . . . . . 12 |- ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
260		eluz2 11693	. . . . . . . . . . . 12 |- ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) )
261	259, 260	sylibr 224	. . . . . . . . . . 11 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) )
262		hashfz 13214	. . . . . . . . . . 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 11091	. . . . . . . . . . . . . . . 16 |- 2 e. CC
265	264	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. CC )
266	145, 265	subcld 10392	. . . . . . . . . . . . . 14 |- ( ph -> ( L - 2 ) e. CC )
267	266	subid1d 10381	. . . . . . . . . . . . 13 |- ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) )
268	267	oveq1d 6665	. . . . . . . . . . . 12 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) )
269	145, 265, 181	subadd23d 10414	. . . . . . . . . . . 12 |- ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) )
270	264, 173	negsubdi2i 10367	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = ( 1 - 2 )
271		2m1e1 11135	. . . . . . . . . . . . . . . . 17 |- ( 2 - 1 ) = 1
272	271	negeqi 10274	. . . . . . . . . . . . . . . 16 |- -u ( 2 - 1 ) = -u 1
273	270, 272	eqtr3i 2646	. . . . . . . . . . . . . . 15 |- ( 1 - 2 ) = -u 1
274	273	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 - 2 ) = -u 1 )
275	274	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) )
276	145, 181	negsubd 10398	. . . . . . . . . . . . 13 |- ( ph -> ( L + -u 1 ) = ( L - 1 ) )
277	275, 276	eqtrd 2656	. . . . . . . . . . . 12 |- ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) )
278	268, 269, 277	3eqtrd 2660	. . . . . . . . . . 11 |- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
279	278	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) )
280	263, 279	eqtrd 2656	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) )
281	280	oveq1d 6665	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) )
282	186, 234	mulcomd 10061	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
283	282	adantr 481	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
284	237, 281, 283	3eqtrd 2660	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) )
285		fzfid 12772	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin )
286		fzn0 12355	. . . . . . . . 9 |- ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) )
287	261, 286	sylibr 224	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) )
288	125	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR )
289		simpll 790	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph )
290	156	adantlr 751	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) )
291	289, 290, 57	syl2anc 693	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR )
292	55	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T )
293		elfzelz 12342	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ )
294	293	zred 11482	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR )
295	294	adantl 482	. . . . . . . . . . . . . . 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 10069	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR )
298	14	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR )
299	297, 298	remulcld 10070	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR )
300	114	adantr 481	. . . . . . . . . . . . . . . 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 10458	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
303	302, 296	readdcld 10069	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
304	303, 298	remulcld 10070	. . . . . . . . . . . . 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 554	. . . . . . . . . . . . . . 15 |- ( ph -> ( F : T --> RR /\ S e. T ) )
307	306	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) )
308		ffvelrn 6357	. . . . . . . . . . . . . 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 12345	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) )
311	310	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) )
312	295, 302, 296, 311	leadd1dd 10641	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) )
313	14, 78	jca 554	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E e. RR /\ 0 < E ) )
314	313	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) )
315		lemul1 10875	. . . . . . . . . . . . . . 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 1326	. . . . . . . . . . . . . 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 222	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) )
318	114, 138	resubcld 10458	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L - 2 ) e. RR )
319	318, 170	readdcld 10069	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR )
320	319, 14	remulcld 10070	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR )
321	305, 55	ffvelrnd 6360	. . . . . . . . . . . . . . 15 |- ( ph -> ( F ` S ) e. RR )
322	126, 170	resubcld 10458	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR )
323	322, 14	remulcld 10070	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR )
324		addid1 10216	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 e. CC -> ( 1 + 0 ) = 1 )
325	324	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 e. CC -> 1 = ( 1 + 0 ) )
326	173, 325	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> 1 = ( 1 + 0 ) )
327	181	subidd 10380	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( 1 - 1 ) = 0 )
328	327	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 0 = ( 1 - 1 ) )
329	328	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) )
330		addsubass 10291	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) )
331	330	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
332	181, 181, 181, 331	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) )
333	326, 329, 332	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 1 = ( ( 1 + 1 ) - 1 ) )
334	333	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) )
335	249	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 + 1 ) = 2 )
336	335	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) )
337	336	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) )
338	145, 265, 181	subsubd 10420	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) )
339	334, 337, 338	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) )
340	339	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) )
341	264, 66, 9	divcli 10767	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 3 ) e. CC
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 / 3 ) e. CC )
343	266, 181, 342	addsubassd 10412	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) )
344	173, 66, 9	divcli 10767	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / 3 ) e. CC
345		df-3 11080	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 3 = ( 2 + 1 )
346	345	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
347	264, 173, 66, 9	divdiri 10782	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
348	346, 67, 347	3eqtr3ri 2653	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
349	173, 341, 344, 348	subaddrii 10370	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - ( 2 / 3 ) ) = ( 1 / 3 )
350	349	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) )
351	350	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
352	340, 343, 351	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) )
353	137, 7, 9	redivcli 10792	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 / 3 ) e. RR
354	353	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 / 3 ) e. RR )
355		1lt2 11194	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
356	7, 69	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 e. RR /\ 0 < 3 )
357	1, 137, 356	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) )
358		ltdiv1 10887	. . . . . . . . . . . . . . . . . . . . 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 223	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 / 3 ) < ( 2 / 3 ) )
361	170, 354, 126, 360	ltsub2dd 10640	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
362	352, 361	eqbrtrrd 4677	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) )
363	319, 322, 13, 362	ltmul1dd 11927	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
364	23	simprd 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. S e. ( D ` ( L - 1 ) ) )
365	195	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> 1 <_ L )
366	140, 122	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. RR )
367	140	lep1d 10955	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> N <_ ( N + 1 ) )
368	114, 140, 366, 196, 367	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> L <_ ( N + 1 ) )
369	135	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( N + 1 ) e. ZZ )
370		elfz 12332	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( L e. ( 1 ... ( N + 1 ) ) <-> ( 1 <_ L /\ L <_ ( N + 1 ) ) ) )
372	365, 368, 371	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> L e. ( 1 ... ( N + 1 ) ) )
373	145, 181	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( L - 1 ) + 1 ) = L )
374		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 0 + 1 ) = 1
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( 0 + 1 ) = 1 )
376	375	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
377	372, 373, 376	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
378		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> 0 e. ZZ )
379	131, 192	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( L - 1 ) e. ZZ )
380		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1327	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
382	377, 381	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( L - 1 ) e. ( 0 ... N ) )
383		rabexg 4812	. . . . . . . . . . . . . . . . . . . . . . . . 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 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) )
386	385	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
387	386	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
388	387	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . 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 6280	. . . . . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
391	364, 390	neleqtrd 2722	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } )
392		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
393	47, 48, 392	nfbr 4699	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E )
394	51	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 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 3360	. . . . . . . . . . . . . . . . . . . . . 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 318	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
397		ianor 509	. . . . . . . . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
399		olc 399	. . . . . . . . . . . . . . . . . . . . 21 |- ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) )
400	399	anim1i 592	. . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . 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 402	. . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . . . . 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 968	. . . . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) )
407	323, 321	ltnled 10184	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) )
408	406, 407	mpbird 247	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) )
409	320, 323, 321, 363, 408	lttrd 10198	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) )
410	320, 321, 409	ltled 10185	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
411	410	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
412	299, 304, 309, 317, 411	letrd 10194	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) )
413		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ t ( ( i + ( 1 / 3 ) ) x. E )
414	413, 48, 47	nfbr 4699	. . . . . . . . . . . . 13 |- F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S )
415	51	breq2d 4665	. . . . . . . . . . . . 13 |- ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) )
416	44, 45, 414, 415	elrabf 3360	. . . . . . . . . . . 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 698	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
418		rabexg 4812	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
421		oveq1 6657	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) )
422	421	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) )
423	422	breq1d 4663	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
424	423	rabbidv 3189	. . . . . . . . . . . . 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 6280	. . . . . . . . . . . 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 693	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
428	417, 427	eleqtrrd 2704	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) )
429	151	3ad2ant1 1082	. . . . . . . . . . . . . 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 224	. . . . . . . . . . . . 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 1062	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) )
433	431, 432	sseldd 3604	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) )
434		elex 3212	. . . . . . . . . . . . 13 |- ( S e. ( B ` i ) -> S e. _V )
435	434	3ad2ant3 1084	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V )
436		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( 0 ... N )
437		nfrab1 3122	. . . . . . . . . . . . . . . . . . 19 |- F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
438	436, 437	nfmpt 4746	. . . . . . . . . . . . . . . . . 18 |- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
439	425, 438	nfcxfr 2762	. . . . . . . . . . . . . . . . 17 |- F/_ t B
440		nfcv 2764	. . . . . . . . . . . . . . . . 17 |- F/_ t i
441	439, 440	nffv 6198	. . . . . . . . . . . . . . . 16 |- F/_ t ( B ` i )
442	441	nfel2 2781	. . . . . . . . . . . . . . 15 |- F/ t S e. ( B ` i )
443	94, 95, 442	nf3an 1831	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) )
444		nfv 1843	. . . . . . . . . . . . . 14 |- F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S )
445	443, 444	nfim 1825	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
446		eleq1 2689	. . . . . . . . . . . . . . 15 |- ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) )
447	446	3anbi3d 1405	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) )
448	99	breq2d 4665	. . . . . . . . . . . . . 14 |- ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) )
449	447, 448	imbi12d 334	. . . . . . . . . . . . 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 3265	. . . . . . . . . . . 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 1373	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
454	428, 453	mpd3an3 1425	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
455	454	adantlr 751	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) )
456	285, 287, 288, 291, 455	fsumlt 14532	. . . . . . 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 4677	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) )
458	127	adantr 481	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR )
459	158	adantr 481	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR )
460	313	adantr 481	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) )
461		ltmul2 10874	. . . . . . 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 1326	. . . . . 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 222	. . . . 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 10198	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) )
465	156, 58	syldan 487	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
466	465	adantlr 751	. . . . . . . . 9 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
467	466	recnd 10068	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
468	285, 467	fsumcl 14464	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC )
469	468	addid1d 10236	. . . . . 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 10041	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 e. RR )
471		fzfid 12772	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin )
472	14	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR )
473		0red 10041	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR )
474	126	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR )
475		elfzelz 12342	. . . . . . . . . . . . . . 15 |- ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ )
476	475	zred 11482	. . . . . . . . . . . . . 14 |- ( i e. ( ( L - 1 ) ... N ) -> i e. RR )
477	476	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR )
478		1m1e0 11089	. . . . . . . . . . . . . . 15 |- ( 1 - 1 ) = 0
479	122, 114, 122, 365	lesub1dd 10643	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 - 1 ) <_ ( L - 1 ) )
480	478, 479	syl5eqbrr 4689	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( L - 1 ) )
481	480	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) )
482		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) )
483	475	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ )
484	379	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ )
485	135	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ )
486		elfz 12332	. . . . . . . . . . . . . . . 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 1326	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) )
488	482, 487	mpbid 222	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) )
489	488	simpld 475	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i )
490	473, 474, 477, 481, 489	letrd 10194	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i )
491		elfzle2 12345	. . . . . . . . . . . . 13 |- ( i e. ( ( L - 1 ) ... N ) -> i <_ N )
492	491	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N )
493		0zd 11389	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ )
494		elfz 12332	. . . . . . . . . . . . 13 |- ( ( i e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
495	483, 493, 485, 494	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( 0 ... N ) <-> ( 0 <_ i /\ i <_ N ) ) )
496	490, 492, 495	mpbir2and 957	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) )
497	496, 57	syldan 487	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR )
498	472, 497	remulcld 10070	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
499	498	adantlr 751	. . . . . . . 8 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR )
500	471, 499	fsumrecl 14465	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
501	285, 466	fsumrecl 14465	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR )
502		fzfid 12772	. . . . . . . . 9 |- ( ph -> ( ( L - 1 ) ... N ) e. Fin )
503	182	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC )
504	503	mul01d 10235	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 )
505	496, 106	syldan 487	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) )
506	313	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) )
507		lemul2 10876	. . . . . . . . . . . 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 1326	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) )
509	505, 508	mpbid 222	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) )
510	504, 509	eqbrtrrd 4677	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) )
511	502, 498, 510	fsumge0 14527	. . . . . . . 8 |- ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
512	511	adantr 481	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) )
513	470, 500, 501, 512	leadd2dd 10642	. . . . . 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 4677	. . . . 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 10068	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC )
516	130, 182, 515	fsummulc2 14516	. . . . . 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 481	. . . . 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 12342	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ )
520	519	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ )
521	520	zred 11482	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR )
522	318	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR )
523	126	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR )
524		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) )
525		0zd 11389	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ )
526	134	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ )
527		elfz 12332	. . . . . . . . . . . . . . . . 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 1326	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) )
529	524, 528	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) )
530	529	simprd 479	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) )
531	122, 138, 114	ltsub2d 10637	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) )
532	355, 531	mpbii 223	. . . . . . . . . . . . . . 15 |- ( ph -> ( L - 2 ) < ( L - 1 ) )
533	532	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) )
534	521, 522, 523, 530, 533	lelttrd 10195	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) )
535	521, 523	ltnled 10184	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) )
536	534, 535	mpbid 222	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( L - 1 ) <_ j )
537	536	intnanrd 963	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( ( L - 1 ) <_ j /\ j <_ N ) )
538	379	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. ZZ )
539	135	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> N e. ZZ )
540		elfz 12332	. . . . . . . . . . . 12 |- ( ( j e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) )
541	520, 538, 539, 540	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) )
542	537, 541	mtbird 315	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. j e. ( ( L - 1 ) ... N ) )
543	542	ex 450	. . . . . . . . 9 |- ( ph -> ( j e. ( 0 ... ( L - 2 ) ) -> -. j e. ( ( L - 1 ) ... N ) ) )
544	518, 543	ralrimi 2957	. . . . . . . 8 |- ( ph -> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) )
545		disj 4017	. . . . . . . 8 |- ( ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) <-> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) )
546	544, 545	sylibr 224	. . . . . . 7 |- ( ph -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) )
547	546	adantr 481	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) )
548	150	adantr 481	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) <_ N )
549	134, 378, 135	3jca 1242	. . . . . . . . . . 11 |- ( ph -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) )
550	549	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) )
551		elfz 12332	. . . . . . . . . 10 |- ( ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) )
552	550, 551	syl 17	. . . . . . . . 9 |- ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) )
553	258, 548, 552	mpbir2and 957	. . . . . . . 8 |- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( 0 ... N ) )
554		fzsplit 12367	. . . . . . . 8 |- ( ( L - 2 ) e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) )
555	553, 554	syl 17	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) )
556	269, 275, 276	3eqtrd 2660	. . . . . . . . . 10 |- ( ph -> ( ( L - 2 ) + 1 ) = ( L - 1 ) )
557	556	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( ( L - 2 ) + 1 ) ... N ) = ( ( L - 1 ) ... N ) )
558	557	uneq2d 3767	. . . . . . . 8 |- ( ph -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
559	558	adantr 481	. . . . . . 7 |- ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
560	555, 559	eqtrd 2656	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) )
561		fzfid 12772	. . . . . 6 |- ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) e. Fin )
562	182	adantr 481	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> E e. CC )
563	57	recnd 10068	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. CC )
564	562, 563	mulcld 10060	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
565	564	adantlr 751	. . . . . 6 |- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC )
566	547, 560, 561, 565	fsumsplit 14471	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... N ) ( 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 ) ) ) )
567	514, 517, 566	3brtr4d 4685	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
568	120, 159, 59	3jca 1242	. . . . . 6 |- ( ph -> ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) )
569	568	adantr 481	. . . . 5 |- ( ( ph /\ -. L = 1 ) -> ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) )
570		ltletr 10129	. . . . 5 |- ( ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) -> ( ( ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) )
571	569, 570	syl 17	. . . 4 |- ( ( ph /\ -. L = 1 ) -> ( ( ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) )
572	464, 567, 571	mp2and 715	. . 3 |- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
573	111, 572	pm2.61dan 832	. 2 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
574		sumex 14418	. . 3 |- sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V
575	99	oveq2d 6666	. . . . 5 |- ( t = S -> ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` i ) ` S ) ) )
576	575	sumeq2sdv 14435	. . . 4 |- ( t = S -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
577		eqid 2622	. . . 4 |- ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) )
578	576, 577	fvmptg 6280	. . 3 |- ( ( S e. T /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V ) -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
579	55, 574, 578	sylancl 694	. 2 |- ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) )
580	573, 579	breqtrrd 4681	1 |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) )

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

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

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

This theorem is referenced by:  stoweidlem34  40251