stoweidlem26

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)

	Ref	Expression
Hypotheses	stoweidlem26.1	$⊢ \underline{Ⅎ} t F$
	stoweidlem26.2	$⊢ Ⅎ j φ$
	stoweidlem26.3	$⊢ Ⅎ t φ$
	stoweidlem26.4	$⊢ D = (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
	stoweidlem26.5	$⊢ B = (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
	stoweidlem26.6	$⊢ φ \to N \in ℕ$
	stoweidlem26.7	$⊢ φ \to T \in V$
	stoweidlem26.8	$⊢ φ \to L \in (1 \dots N)$
	stoweidlem26.9	$⊢ φ \to S \in (D (L) ∖ D (L - 1))$
	stoweidlem26.10	$⊢ φ \to F : T ⟶ ℝ$
	stoweidlem26.11	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem26.12	$⊢ φ \to E < \frac{1}{3}$
	stoweidlem26.13	$⊢ (φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
	stoweidlem26.14	$⊢ (φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t)$
	stoweidlem26.15	$⊢ (φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)$
Assertion	stoweidlem26	$⊢ φ \to (L - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (S)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem26.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem26.2	$⊢ Ⅎ j φ$
3		stoweidlem26.3	$⊢ Ⅎ t φ$
4		stoweidlem26.4	$⊢ D = (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
5		stoweidlem26.5	$⊢ B = (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
6		stoweidlem26.6	$⊢ φ \to N \in ℕ$
7		stoweidlem26.7	$⊢ φ \to T \in V$
8		stoweidlem26.8	$⊢ φ \to L \in (1 \dots N)$
9		stoweidlem26.9	$⊢ φ \to S \in (D (L) ∖ D (L - 1))$
10		stoweidlem26.10	$⊢ φ \to F : T ⟶ ℝ$
11		stoweidlem26.11	$⊢ φ \to E \in ℝ^{+}$
12		stoweidlem26.12	$⊢ φ \to E < \frac{1}{3}$
13		stoweidlem26.13	$⊢ (φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
14		stoweidlem26.14	$⊢ (φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t)$
15		stoweidlem26.15	$⊢ (φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)$
16		1re	$⊢ 1 \in ℝ$
17		eleq1	$⊢ L = 1 \to (L \in ℝ \leftrightarrow 1 \in ℝ)$
18	16 17	mpbiri	$⊢ L = 1 \to L \in ℝ$
19	18	adantl	$⊢ (φ \land L = 1) \to L \in ℝ$
20		4re	$⊢ 4 \in ℝ$
21	20	a1i	$⊢ (φ \land L = 1) \to 4 \in ℝ$
22		3re	$⊢ 3 \in ℝ$
23	22	a1i	$⊢ (φ \land L = 1) \to 3 \in ℝ$
24		3ne0	$⊢ 3 \neq 0$
25	24	a1i	$⊢ (φ \land L = 1) \to 3 \neq 0$
26	21 23 25	redivcld	$⊢ (φ \land L = 1) \to \frac{4}{3} \in ℝ$
27	19 26	resubcld	$⊢ (φ \land L = 1) \to L - (\frac{4}{3}) \in ℝ$
28	11	rpred	$⊢ φ \to E \in ℝ$
29	28	adantr	$⊢ (φ \land L = 1) \to E \in ℝ$
30	27 29	remulcld	$⊢ (φ \land L = 1) \to (L - (\frac{4}{3})) E \in ℝ$
31		0red	$⊢ (φ \land L = 1) \to 0 \in ℝ$
32		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
33	28	adantr	$⊢ (φ \land i \in (0 \dots N)) \to E \in ℝ$
34		eldif	$⊢ S \in (D (L) ∖ D (L - 1)) \leftrightarrow (S \in D (L) \land \neg S \in D (L - 1))$
35	9 34	sylib	$⊢ φ \to (S \in D (L) \land \neg S \in D (L - 1))$
36	35	simpld	$⊢ φ \to S \in D (L)$
37		oveq1	$⊢ j = L \to j - (\frac{1}{3}) = L - (\frac{1}{3})$
38	37	oveq1d	$⊢ j = L \to (j - (\frac{1}{3})) E = (L - (\frac{1}{3})) E$
39	38	breq2d	$⊢ j = L \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (L - (\frac{1}{3})) E)$
40	39	rabbidv	$⊢ j = L \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (L - (\frac{1}{3})) E\}$
41		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
42	41 8	sselid	$⊢ φ \to L \in (0 \dots N)$
43		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (L - (\frac{1}{3})) E\} \in V$
44	7 43	syl	$⊢ φ \to \{t \in T \| F (t) \leq (L - (\frac{1}{3})) E\} \in V$
45	4 40 42 44	fvmptd3	$⊢ φ \to D (L) = \{t \in T \| F (t) \leq (L - (\frac{1}{3})) E\}$
46	36 45	eleqtrd	$⊢ φ \to S \in \{t \in T \| F (t) \leq (L - (\frac{1}{3})) E\}$
47		nfcv	$⊢ \underline{Ⅎ} t S$
48		nfcv	$⊢ \underline{Ⅎ} t T$
49	1 47	nffv	$⊢ \underline{Ⅎ} t F (S)$
50		nfcv	$⊢ \underline{Ⅎ} t \leq$
51		nfcv	$⊢ \underline{Ⅎ} t (L - (\frac{1}{3})) E$
52	49 50 51	nfbr	$⊢ Ⅎ t F (S) \leq (L - (\frac{1}{3})) E$
53		fveq2	$⊢ t = S \to F (t) = F (S)$
54	53	breq1d	$⊢ t = S \to (F (t) \leq (L - (\frac{1}{3})) E \leftrightarrow F (S) \leq (L - (\frac{1}{3})) E)$
55	47 48 52 54	elrabf	$⊢ S \in \{t \in T \| F (t) \leq (L - (\frac{1}{3})) E\} \leftrightarrow (S \in T \land F (S) \leq (L - (\frac{1}{3})) E)$
56	46 55	sylib	$⊢ φ \to (S \in T \land F (S) \leq (L - (\frac{1}{3})) E)$
57	56	simpld	$⊢ φ \to S \in T$
58	57	adantr	$⊢ (φ \land i \in (0 \dots N)) \to S \in T$
59	13 58	ffvelcdmd	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (S) \in ℝ$
60	33 59	remulcld	$⊢ (φ \land i \in (0 \dots N)) \to E X (i) (S) \in ℝ$
61	32 60	fsumrecl	$⊢ φ \to \sum_{i = 0}^{N} E X (i) (S) \in ℝ$
62	61	adantr	$⊢ (φ \land L = 1) \to \sum_{i = 0}^{N} E X (i) (S) \in ℝ$
63	20 22 24	redivcli	$⊢ \frac{4}{3} \in ℝ$
64	63	a1i	$⊢ (φ \land L = 1) \to \frac{4}{3} \in ℝ$
65	19 64	resubcld	$⊢ (φ \land L = 1) \to L - (\frac{4}{3}) \in ℝ$
66	19	recnd	$⊢ (φ \land L = 1) \to L \in ℂ$
67	66	subid1d	$⊢ (φ \land L = 1) \to L - 0 = L$
68		3cn	$⊢ 3 \in ℂ$
69	68 24	dividi	$⊢ \frac{3}{3} = 1$
70		3lt4	$⊢ 3 < 4$
71		3pos	$⊢ 0 < 3$
72	22 20 22 71	ltdiv1ii	$⊢ 3 < 4 \leftrightarrow \frac{3}{3} < \frac{4}{3}$
73	70 72	mpbi	$⊢ \frac{3}{3} < \frac{4}{3}$
74	69 73	eqbrtrri	$⊢ 1 < \frac{4}{3}$
75		breq1	$⊢ L = 1 \to (L < \frac{4}{3} \leftrightarrow 1 < \frac{4}{3})$
76	75	adantl	$⊢ (φ \land L = 1) \to (L < \frac{4}{3} \leftrightarrow 1 < \frac{4}{3})$
77	74 76	mpbiri	$⊢ (φ \land L = 1) \to L < \frac{4}{3}$
78	67 77	eqbrtrd	$⊢ (φ \land L = 1) \to L - 0 < \frac{4}{3}$
79	19 31 64 78	ltsub23d	$⊢ (φ \land L = 1) \to L - (\frac{4}{3}) < 0$
80	11	rpgt0d	$⊢ φ \to 0 < E$
81	80	adantr	$⊢ (φ \land L = 1) \to 0 < E$
82		mulltgt0	$⊢ ((L - (\frac{4}{3}) \in ℝ \land L - (\frac{4}{3}) < 0) \land (E \in ℝ \land 0 < E)) \to (L - (\frac{4}{3})) E < 0$
83	65 79 29 81 82	syl22anc	$⊢ (φ \land L = 1) \to (L - (\frac{4}{3})) E < 0$
84		0cn	$⊢ 0 \in ℂ$
85		fsumconst	$⊢ ((0 \dots N) \in Fin \land 0 \in ℂ) \to \sum_{i = 0}^{N} 0 = \|(0 \dots N)\| \cdot 0$
86	32 84 85	sylancl	$⊢ φ \to \sum_{i = 0}^{N} 0 = \|(0 \dots N)\| \cdot 0$
87		hashcl	$⊢ (0 \dots N) \in Fin \to \|(0 \dots N)\| \in ℕ_{0}$
88		nn0cn	$⊢ \|(0 \dots N)\| \in ℕ_{0} \to \|(0 \dots N)\| \in ℂ$
89	32 87 88	3syl	$⊢ φ \to \|(0 \dots N)\| \in ℂ$
90	89	mul01d	$⊢ φ \to \|(0 \dots N)\| \cdot 0 = 0$
91	86 90	eqtrd	$⊢ φ \to \sum_{i = 0}^{N} 0 = 0$
92	91	adantr	$⊢ (φ \land L = 1) \to \sum_{i = 0}^{N} 0 = 0$
93		0red	$⊢ (φ \land i \in (0 \dots N)) \to 0 \in ℝ$
94	11	rpge0d	$⊢ φ \to 0 \leq E$
95	94	adantr	$⊢ (φ \land i \in (0 \dots N)) \to 0 \leq E$
96		nfv	$⊢ Ⅎ t i \in (0 \dots N)$
97	3 96	nfan	$⊢ Ⅎ t (φ \land i \in (0 \dots N))$
98		nfv	$⊢ Ⅎ t 0 \leq X (i) (S)$
99	97 98	nfim	$⊢ Ⅎ t ((φ \land i \in (0 \dots N)) \to 0 \leq X (i) (S))$
100		fveq2	$⊢ t = S \to X (i) (t) = X (i) (S)$
101	100	breq2d	$⊢ t = S \to (0 \leq X (i) (t) \leftrightarrow 0 \leq X (i) (S))$
102	101	imbi2d	$⊢ t = S \to (((φ \land i \in (0 \dots N)) \to 0 \leq X (i) (t)) \leftrightarrow ((φ \land i \in (0 \dots N)) \to 0 \leq X (i) (S)))$
103	14	3expia	$⊢ (φ \land i \in (0 \dots N)) \to (t \in T \to 0 \leq X (i) (t))$
104	103	com12	$⊢ t \in T \to ((φ \land i \in (0 \dots N)) \to 0 \leq X (i) (t))$
105	47 99 102 104	vtoclgaf	$⊢ S \in T \to ((φ \land i \in (0 \dots N)) \to 0 \leq X (i) (S))$
106	58 105	mpcom	$⊢ (φ \land i \in (0 \dots N)) \to 0 \leq X (i) (S)$
107	33 59 95 106	mulge0d	$⊢ (φ \land i \in (0 \dots N)) \to 0 \leq E X (i) (S)$
108	32 93 60 107	fsumle	$⊢ φ \to \sum_{i = 0}^{N} 0 \leq \sum_{i = 0}^{N} E X (i) (S)$
109	108	adantr	$⊢ (φ \land L = 1) \to \sum_{i = 0}^{N} 0 \leq \sum_{i = 0}^{N} E X (i) (S)$
110	92 109	eqbrtrrd	$⊢ (φ \land L = 1) \to 0 \leq \sum_{i = 0}^{N} E X (i) (S)$
111	30 31 62 83 110	ltletrd	$⊢ (φ \land L = 1) \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S)$
112		elfzelz	$⊢ L \in (1 \dots N) \to L \in ℤ$
113		zre	$⊢ L \in ℤ \to L \in ℝ$
114	8 112 113	3syl	$⊢ φ \to L \in ℝ$
115	20	a1i	$⊢ φ \to 4 \in ℝ$
116	22	a1i	$⊢ φ \to 3 \in ℝ$
117	24	a1i	$⊢ φ \to 3 \neq 0$
118	115 116 117	redivcld	$⊢ φ \to \frac{4}{3} \in ℝ$
119	114 118	resubcld	$⊢ φ \to L - (\frac{4}{3}) \in ℝ$
120	119 28	remulcld	$⊢ φ \to (L - (\frac{4}{3})) E \in ℝ$
121	120	adantr	$⊢ (φ \land \neg L = 1) \to (L - (\frac{4}{3})) E \in ℝ$
122	16	a1i	$⊢ φ \to 1 \in ℝ$
123	28 6	nndivred	$⊢ φ \to \frac{E}{N} \in ℝ$
124	122 123	resubcld	$⊢ φ \to 1 - (\frac{E}{N}) \in ℝ$
125	114 122	resubcld	$⊢ φ \to L - 1 \in ℝ$
126	124 125	remulcld	$⊢ φ \to (1 - (\frac{E}{N})) (L - 1) \in ℝ$
127	28 126	remulcld	$⊢ φ \to E (1 - (\frac{E}{N})) (L - 1) \in ℝ$
128	127	adantr	$⊢ (φ \land \neg L = 1) \to E (1 - (\frac{E}{N})) (L - 1) \in ℝ$
129		fzfid	$⊢ φ \to (0 \dots L - 2) \in Fin$
130	8	elfzelzd	$⊢ φ \to L \in ℤ$
131		2z	$⊢ 2 \in ℤ$
132	131	a1i	$⊢ φ \to 2 \in ℤ$
133	130 132	zsubcld	$⊢ φ \to L - 2 \in ℤ$
134	6	nnzd	$⊢ φ \to N \in ℤ$
135	130	zred	$⊢ φ \to L \in ℝ$
136		2re	$⊢ 2 \in ℝ$
137	136	a1i	$⊢ φ \to 2 \in ℝ$
138	135 137	resubcld	$⊢ φ \to L - 2 \in ℝ$
139	6	nnred	$⊢ φ \to N \in ℝ$
140		0le2	$⊢ 0 \leq 2$
141		0red	$⊢ φ \to 0 \in ℝ$
142	141 137 135	lesub2d	$⊢ φ \to (0 \leq 2 \leftrightarrow L - 2 \leq L - 0)$
143	140 142	mpbii	$⊢ φ \to L - 2 \leq L - 0$
144	130	zcnd	$⊢ φ \to L \in ℂ$
145	144	subid1d	$⊢ φ \to L - 0 = L$
146	143 145	breqtrd	$⊢ φ \to L - 2 \leq L$
147		elfzle2	$⊢ L \in (1 \dots N) \to L \leq N$
148	8 147	syl	$⊢ φ \to L \leq N$
149	138 135 139 146 148	letrd	$⊢ φ \to L - 2 \leq N$
150	133 134 149	3jca	$⊢ φ \to (L - 2 \in ℤ \land N \in ℤ \land L - 2 \leq N)$
151		eluz2	$⊢ N \in ℤ_{\geq (L - 2)} \leftrightarrow (L - 2 \in ℤ \land N \in ℤ \land L - 2 \leq N)$
152	150 151	sylibr	$⊢ φ \to N \in ℤ_{\geq (L - 2)}$
153		fzss2	$⊢ N \in ℤ_{\geq (L - 2)} \to (0 \dots L - 2) \subseteq (0 \dots N)$
154	152 153	syl	$⊢ φ \to (0 \dots L - 2) \subseteq (0 \dots N)$
155	154	sselda	$⊢ (φ \land i \in (0 \dots L - 2)) \to i \in (0 \dots N)$
156	155 59	syldan	$⊢ (φ \land i \in (0 \dots L - 2)) \to X (i) (S) \in ℝ$
157	129 156	fsumrecl	$⊢ φ \to \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ$
158	28 157	remulcld	$⊢ φ \to E \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ$
159	158	adantr	$⊢ (φ \land \neg L = 1) \to E \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ$
160	28 125	remulcld	$⊢ φ \to E (L - 1) \in ℝ$
161	28 28	remulcld	$⊢ φ \to E E \in ℝ$
162	160 161	resubcld	$⊢ φ \to E (L - 1) - E E \in ℝ$
163	125 6	nndivred	$⊢ φ \to \frac{L - 1}{N} \in ℝ$
164	161 163	remulcld	$⊢ φ \to E E (\frac{L - 1}{N}) \in ℝ$
165	160 164	resubcld	$⊢ φ \to E (L - 1) - E E (\frac{L - 1}{N}) \in ℝ$
166	125 28	resubcld	$⊢ φ \to L - 1 - E \in ℝ$
167	122 28	readdcld	$⊢ φ \to 1 + E \in ℝ$
168	16 22 24	redivcli	$⊢ \frac{1}{3} \in ℝ$
169	168	a1i	$⊢ φ \to \frac{1}{3} \in ℝ$
170	28 169 122 12	ltadd2dd	$⊢ φ \to 1 + E < 1 + (\frac{1}{3})$
171		ax-1cn	$⊢ 1 \in ℂ$
172	68 171 68 24	divdiri	$⊢ \frac{3 + 1}{3} = (\frac{3}{3}) + (\frac{1}{3})$
173		3p1e4	$⊢ 3 + 1 = 4$
174	173	oveq1i	$⊢ \frac{3 + 1}{3} = \frac{4}{3}$
175	69	oveq1i	$⊢ (\frac{3}{3}) + (\frac{1}{3}) = 1 + (\frac{1}{3})$
176	172 174 175	3eqtr3ri	$⊢ 1 + (\frac{1}{3}) = \frac{4}{3}$
177	170 176	breqtrdi	$⊢ φ \to 1 + E < \frac{4}{3}$
178	167 118 114 177	ltsub2dd	$⊢ φ \to L - (\frac{4}{3}) < L - (1 + E)$
179	171	a1i	$⊢ φ \to 1 \in ℂ$
180	11	rpcnd	$⊢ φ \to E \in ℂ$
181	144 179 180	subsub4d	$⊢ φ \to L - 1 - E = L - (1 + E)$
182	178 181	breqtrrd	$⊢ φ \to L - (\frac{4}{3}) < L - 1 - E$
183	119 166 11 182	ltmul1dd	$⊢ φ \to (L - (\frac{4}{3})) E < (L - 1 - E) E$
184	144 179	subcld	$⊢ φ \to L - 1 \in ℂ$
185	184 180	subcld	$⊢ φ \to L - 1 - E \in ℂ$
186	180 185	mulcomd	$⊢ φ \to E (L - 1 - E) = (L - 1 - E) E$
187	180 184 180	subdid	$⊢ φ \to E (L - 1 - E) = E (L - 1) - E E$
188	186 187	eqtr3d	$⊢ φ \to (L - 1 - E) E = E (L - 1) - E E$
189	183 188	breqtrd	$⊢ φ \to (L - (\frac{4}{3})) E < E (L - 1) - E E$
190		1zzd	$⊢ φ \to 1 \in ℤ$
191		elfz	$⊢ (L \in ℤ \land 1 \in ℤ \land N \in ℤ) \to (L \in (1 \dots N) \leftrightarrow (1 \leq L \land L \leq N))$
192	130 190 134 191	syl3anc	$⊢ φ \to (L \in (1 \dots N) \leftrightarrow (1 \leq L \land L \leq N))$
193	8 192	mpbid	$⊢ φ \to (1 \leq L \land L \leq N)$
194	193	simprd	$⊢ φ \to L \leq N$
195		zlem1lt	$⊢ (L \in ℤ \land N \in ℤ) \to (L \leq N \leftrightarrow L - 1 < N)$
196	130 134 195	syl2anc	$⊢ φ \to (L \leq N \leftrightarrow L - 1 < N)$
197	194 196	mpbid	$⊢ φ \to L - 1 < N$
198	6	nngt0d	$⊢ φ \to 0 < N$
199		ltdiv1	$⊢ (L - 1 \in ℝ \land N \in ℝ \land (N \in ℝ \land 0 < N)) \to (L - 1 < N \leftrightarrow \frac{L - 1}{N} < \frac{N}{N})$
200	125 139 139 198 199	syl112anc	$⊢ φ \to (L - 1 < N \leftrightarrow \frac{L - 1}{N} < \frac{N}{N})$
201	197 200	mpbid	$⊢ φ \to \frac{L - 1}{N} < \frac{N}{N}$
202	6	nncnd	$⊢ φ \to N \in ℂ$
203	6	nnne0d	$⊢ φ \to N \neq 0$
204	202 203	dividd	$⊢ φ \to \frac{N}{N} = 1$
205	201 204	breqtrd	$⊢ φ \to \frac{L - 1}{N} < 1$
206	28 28 80 80	mulgt0d	$⊢ φ \to 0 < E E$
207		ltmul2	$⊢ (\frac{L - 1}{N} \in ℝ \land 1 \in ℝ \land (E E \in ℝ \land 0 < E E)) \to (\frac{L - 1}{N} < 1 \leftrightarrow E E (\frac{L - 1}{N}) < E E \cdot 1)$
208	163 122 161 206 207	syl112anc	$⊢ φ \to (\frac{L - 1}{N} < 1 \leftrightarrow E E (\frac{L - 1}{N}) < E E \cdot 1)$
209	205 208	mpbid	$⊢ φ \to E E (\frac{L - 1}{N}) < E E \cdot 1$
210	180 180	mulcld	$⊢ φ \to E E \in ℂ$
211	210	mulridd	$⊢ φ \to E E \cdot 1 = E E$
212	209 211	breqtrd	$⊢ φ \to E E (\frac{L - 1}{N}) < E E$
213	164 161 160 212	ltsub2dd	$⊢ φ \to E (L - 1) - E E < E (L - 1) - E E (\frac{L - 1}{N})$
214	120 162 165 189 213	lttrd	$⊢ φ \to (L - (\frac{4}{3})) E < E (L - 1) - E E (\frac{L - 1}{N})$
215	180 202 203	divcld	$⊢ φ \to \frac{E}{N} \in ℂ$
216	179 215 184	subdird	$⊢ φ \to (1 - (\frac{E}{N})) (L - 1) = 1 (L - 1) - (\frac{E}{N}) (L - 1)$
217	184	mullidd	$⊢ φ \to 1 (L - 1) = L - 1$
218	217	oveq1d	$⊢ φ \to 1 (L - 1) - (\frac{E}{N}) (L - 1) = L - 1 - (\frac{E}{N}) (L - 1)$
219	216 218	eqtrd	$⊢ φ \to (1 - (\frac{E}{N})) (L - 1) = L - 1 - (\frac{E}{N}) (L - 1)$
220	219	oveq2d	$⊢ φ \to E (1 - (\frac{E}{N})) (L - 1) = E (L - 1 - (\frac{E}{N}) (L - 1))$
221	215 184	mulcld	$⊢ φ \to (\frac{E}{N}) (L - 1) \in ℂ$
222	180 184 221	subdid	$⊢ φ \to E (L - 1 - (\frac{E}{N}) (L - 1)) = E (L - 1) - E (\frac{E}{N}) (L - 1)$
223	180 202 184 203	div32d	$⊢ φ \to (\frac{E}{N}) (L - 1) = E (\frac{L - 1}{N})$
224	223	oveq2d	$⊢ φ \to E (\frac{E}{N}) (L - 1) = E E (\frac{L - 1}{N})$
225	184 202 203	divcld	$⊢ φ \to \frac{L - 1}{N} \in ℂ$
226	180 180 225	mulassd	$⊢ φ \to E E (\frac{L - 1}{N}) = E E (\frac{L - 1}{N})$
227	224 226	eqtr4d	$⊢ φ \to E (\frac{E}{N}) (L - 1) = E E (\frac{L - 1}{N})$
228	227	oveq2d	$⊢ φ \to E (L - 1) - E (\frac{E}{N}) (L - 1) = E (L - 1) - E E (\frac{L - 1}{N})$
229	220 222 228	3eqtrd	$⊢ φ \to E (1 - (\frac{E}{N})) (L - 1) = E (L - 1) - E E (\frac{L - 1}{N})$
230	214 229	breqtrrd	$⊢ φ \to (L - (\frac{4}{3})) E < E (1 - (\frac{E}{N})) (L - 1)$
231	230	adantr	$⊢ (φ \land \neg L = 1) \to (L - (\frac{4}{3})) E < E (1 - (\frac{E}{N})) (L - 1)$
232	179 215	subcld	$⊢ φ \to 1 - (\frac{E}{N}) \in ℂ$
233		fsumconst	$⊢ ((0 \dots L - 2) \in Fin \land 1 - (\frac{E}{N}) \in ℂ) \to \sum_{i = 0}^{L - 2} (1 - (\frac{E}{N})) = \|(0 \dots L - 2)\| (1 - (\frac{E}{N}))$
234	129 232 233	syl2anc	$⊢ φ \to \sum_{i = 0}^{L - 2} (1 - (\frac{E}{N})) = \|(0 \dots L - 2)\| (1 - (\frac{E}{N}))$
235	234	adantr	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} (1 - (\frac{E}{N})) = \|(0 \dots L - 2)\| (1 - (\frac{E}{N}))$
236		0zd	$⊢ (φ \land \neg L = 1) \to 0 \in ℤ$
237	8	adantr	$⊢ (φ \land \neg L = 1) \to L \in (1 \dots N)$
238	237	elfzelzd	$⊢ (φ \land \neg L = 1) \to L \in ℤ$
239	131	a1i	$⊢ (φ \land \neg L = 1) \to 2 \in ℤ$
240	238 239	zsubcld	$⊢ (φ \land \neg L = 1) \to L - 2 \in ℤ$
241		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
242	6 241	sylib	$⊢ φ \to N \in ℤ_{\geq 1}$
243		elfzp12	$⊢ N \in ℤ_{\geq 1} \to (L \in (1 \dots N) \leftrightarrow (L = 1 \lor L \in (1 + 1 \dots N)))$
244	242 243	syl	$⊢ φ \to (L \in (1 \dots N) \leftrightarrow (L = 1 \lor L \in (1 + 1 \dots N)))$
245	8 244	mpbid	$⊢ φ \to (L = 1 \lor L \in (1 + 1 \dots N))$
246	245	orcanai	$⊢ (φ \land \neg L = 1) \to L \in (1 + 1 \dots N)$
247		1p1e2	$⊢ 1 + 1 = 2$
248	247	a1i	$⊢ (φ \land \neg L = 1) \to 1 + 1 = 2$
249	248	oveq1d	$⊢ (φ \land \neg L = 1) \to (1 + 1 \dots N) = (2 \dots N)$
250	246 249	eleqtrd	$⊢ (φ \land \neg L = 1) \to L \in (2 \dots N)$
251		elfzle1	$⊢ L \in (2 \dots N) \to 2 \leq L$
252	250 251	syl	$⊢ (φ \land \neg L = 1) \to 2 \leq L$
253	114	adantr	$⊢ (φ \land \neg L = 1) \to L \in ℝ$
254	136	a1i	$⊢ (φ \land \neg L = 1) \to 2 \in ℝ$
255	253 254	subge0d	$⊢ (φ \land \neg L = 1) \to (0 \leq L - 2 \leftrightarrow 2 \leq L)$
256	252 255	mpbird	$⊢ (φ \land \neg L = 1) \to 0 \leq L - 2$
257	236 240 256	3jca	$⊢ (φ \land \neg L = 1) \to (0 \in ℤ \land L - 2 \in ℤ \land 0 \leq L - 2)$
258		eluz2	$⊢ L - 2 \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land L - 2 \in ℤ \land 0 \leq L - 2)$
259	257 258	sylibr	$⊢ (φ \land \neg L = 1) \to L - 2 \in ℤ_{\geq 0}$
260		hashfz	$⊢ L - 2 \in ℤ_{\geq 0} \to \|(0 \dots L - 2)\| = (L - 2) - 0 + 1$
261	259 260	syl	$⊢ (φ \land \neg L = 1) \to \|(0 \dots L - 2)\| = (L - 2) - 0 + 1$
262		2cn	$⊢ 2 \in ℂ$
263	262	a1i	$⊢ φ \to 2 \in ℂ$
264	144 263	subcld	$⊢ φ \to L - 2 \in ℂ$
265	264	subid1d	$⊢ φ \to L - 2 - 0 = L - 2$
266	265	oveq1d	$⊢ φ \to (L - 2) - 0 + 1 = L - 2 + 1$
267	144 263 179	subadd23d	$⊢ φ \to L - 2 + 1 = L + 1 - 2$
268	262 171	negsubdi2i	$⊢ - (2 - 1) = 1 - 2$
269		2m1e1	$⊢ 2 - 1 = 1$
270	269	negeqi	$⊢ - (2 - 1) = - 1$
271	268 270	eqtr3i	$⊢ 1 - 2 = - 1$
272	271	a1i	$⊢ φ \to 1 - 2 = - 1$
273	272	oveq2d	$⊢ φ \to L + 1 - 2 = L + -1$
274	144 179	negsubd	$⊢ φ \to L + -1 = L - 1$
275	273 274	eqtrd	$⊢ φ \to L + 1 - 2 = L - 1$
276	266 267 275	3eqtrd	$⊢ φ \to (L - 2) - 0 + 1 = L - 1$
277	276	adantr	$⊢ (φ \land \neg L = 1) \to (L - 2) - 0 + 1 = L - 1$
278	261 277	eqtrd	$⊢ (φ \land \neg L = 1) \to \|(0 \dots L - 2)\| = L - 1$
279	278	oveq1d	$⊢ (φ \land \neg L = 1) \to \|(0 \dots L - 2)\| (1 - (\frac{E}{N})) = (L - 1) (1 - (\frac{E}{N}))$
280	184 232	mulcomd	$⊢ φ \to (L - 1) (1 - (\frac{E}{N})) = (1 - (\frac{E}{N})) (L - 1)$
281	280	adantr	$⊢ (φ \land \neg L = 1) \to (L - 1) (1 - (\frac{E}{N})) = (1 - (\frac{E}{N})) (L - 1)$
282	235 279 281	3eqtrd	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} (1 - (\frac{E}{N})) = (1 - (\frac{E}{N})) (L - 1)$
283		fzfid	$⊢ (φ \land \neg L = 1) \to (0 \dots L - 2) \in Fin$
284		fzn0	$⊢ (0 \dots L - 2) \neq \emptyset \leftrightarrow L - 2 \in ℤ_{\geq 0}$
285	259 284	sylibr	$⊢ (φ \land \neg L = 1) \to (0 \dots L - 2) \neq \emptyset$
286	124	ad2antrr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to 1 - (\frac{E}{N}) \in ℝ$
287		simpll	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to φ$
288	155	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to i \in (0 \dots N)$
289	287 288 59	syl2anc	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to X (i) (S) \in ℝ$
290	57	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to S \in T$
291		elfzelz	$⊢ i \in (0 \dots L - 2) \to i \in ℤ$
292	291	zred	$⊢ i \in (0 \dots L - 2) \to i \in ℝ$
293	292	adantl	$⊢ (φ \land i \in (0 \dots L - 2)) \to i \in ℝ$
294	168	a1i	$⊢ (φ \land i \in (0 \dots L - 2)) \to \frac{1}{3} \in ℝ$
295	293 294	readdcld	$⊢ (φ \land i \in (0 \dots L - 2)) \to i + (\frac{1}{3}) \in ℝ$
296	28	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to E \in ℝ$
297	295 296	remulcld	$⊢ (φ \land i \in (0 \dots L - 2)) \to (i + (\frac{1}{3})) E \in ℝ$
298	114	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to L \in ℝ$
299	136	a1i	$⊢ (φ \land i \in (0 \dots L - 2)) \to 2 \in ℝ$
300	298 299	resubcld	$⊢ (φ \land i \in (0 \dots L - 2)) \to L - 2 \in ℝ$
301	300 294	readdcld	$⊢ (φ \land i \in (0 \dots L - 2)) \to L - 2 + (\frac{1}{3}) \in ℝ$
302	301 296	remulcld	$⊢ (φ \land i \in (0 \dots L - 2)) \to (L - 2 + (\frac{1}{3})) E \in ℝ$
303	10 57	jca	$⊢ φ \to (F : T ⟶ ℝ \land S \in T)$
304	303	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to (F : T ⟶ ℝ \land S \in T)$
305		ffvelcdm	$⊢ (F : T ⟶ ℝ \land S \in T) \to F (S) \in ℝ$
306	304 305	syl	$⊢ (φ \land i \in (0 \dots L - 2)) \to F (S) \in ℝ$
307		elfzle2	$⊢ i \in (0 \dots L - 2) \to i \leq L - 2$
308	307	adantl	$⊢ (φ \land i \in (0 \dots L - 2)) \to i \leq L - 2$
309	293 300 294 308	leadd1dd	$⊢ (φ \land i \in (0 \dots L - 2)) \to i + (\frac{1}{3}) \leq L - 2 + (\frac{1}{3})$
310	28 80	jca	$⊢ φ \to (E \in ℝ \land 0 < E)$
311	310	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to (E \in ℝ \land 0 < E)$
312		lemul1	$⊢ (i + (\frac{1}{3}) \in ℝ \land L - 2 + (\frac{1}{3}) \in ℝ \land (E \in ℝ \land 0 < E)) \to (i + (\frac{1}{3}) \leq L - 2 + (\frac{1}{3}) \leftrightarrow (i + (\frac{1}{3})) E \leq (L - 2 + (\frac{1}{3})) E)$
313	295 301 311 312	syl3anc	$⊢ (φ \land i \in (0 \dots L - 2)) \to (i + (\frac{1}{3}) \leq L - 2 + (\frac{1}{3}) \leftrightarrow (i + (\frac{1}{3})) E \leq (L - 2 + (\frac{1}{3})) E)$
314	309 313	mpbid	$⊢ (φ \land i \in (0 \dots L - 2)) \to (i + (\frac{1}{3})) E \leq (L - 2 + (\frac{1}{3})) E$
315	114 137	resubcld	$⊢ φ \to L - 2 \in ℝ$
316	315 169	readdcld	$⊢ φ \to L - 2 + (\frac{1}{3}) \in ℝ$
317	316 28	remulcld	$⊢ φ \to (L - 2 + (\frac{1}{3})) E \in ℝ$
318	10 57	ffvelcdmd	$⊢ φ \to F (S) \in ℝ$
319	125 169	resubcld	$⊢ φ \to L - 1 - (\frac{1}{3}) \in ℝ$
320	319 28	remulcld	$⊢ φ \to (L - 1 - (\frac{1}{3})) E \in ℝ$
321		addrid	$⊢ 1 \in ℂ \to 1 + 0 = 1$
322	321	eqcomd	$⊢ 1 \in ℂ \to 1 = 1 + 0$
323	171 322	mp1i	$⊢ φ \to 1 = 1 + 0$
324	179	subidd	$⊢ φ \to 1 - 1 = 0$
325	324	eqcomd	$⊢ φ \to 0 = 1 - 1$
326	325	oveq2d	$⊢ φ \to 1 + 0 = 1 + 1 - 1$
327		addsubass	$⊢ (1 \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to 1 + 1 - 1 = 1 + 1 - 1$
328	327	eqcomd	$⊢ (1 \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to 1 + 1 - 1 = 1 + 1 - 1$
329	179 179 179 328	syl3anc	$⊢ φ \to 1 + 1 - 1 = 1 + 1 - 1$
330	323 326 329	3eqtrd	$⊢ φ \to 1 = 1 + 1 - 1$
331	330	oveq2d	$⊢ φ \to L - 1 = L - (1 + 1 - 1)$
332	247	a1i	$⊢ φ \to 1 + 1 = 2$
333	332	oveq1d	$⊢ φ \to 1 + 1 - 1 = 2 - 1$
334	333	oveq2d	$⊢ φ \to L - (1 + 1 - 1) = L - (2 - 1)$
335	144 263 179	subsubd	$⊢ φ \to L - (2 - 1) = L - 2 + 1$
336	331 334 335	3eqtrd	$⊢ φ \to L - 1 = L - 2 + 1$
337	336	oveq1d	$⊢ φ \to L - 1 - (\frac{2}{3}) = (L - 2) + 1 - (\frac{2}{3})$
338	262 68 24	divcli	$⊢ \frac{2}{3} \in ℂ$
339	338	a1i	$⊢ φ \to \frac{2}{3} \in ℂ$
340	264 179 339	addsubassd	$⊢ φ \to (L - 2) + 1 - (\frac{2}{3}) = (L - 2) + 1 - (\frac{2}{3})$
341	171 68 24	divcli	$⊢ \frac{1}{3} \in ℂ$
342		df-3	$⊢ 3 = 2 + 1$
343	342	oveq1i	$⊢ \frac{3}{3} = \frac{2 + 1}{3}$
344	262 171 68 24	divdiri	$⊢ \frac{2 + 1}{3} = (\frac{2}{3}) + (\frac{1}{3})$
345	343 69 344	3eqtr3ri	$⊢ (\frac{2}{3}) + (\frac{1}{3}) = 1$
346	171 338 341 345	subaddrii	$⊢ 1 - (\frac{2}{3}) = \frac{1}{3}$
347	346	a1i	$⊢ φ \to 1 - (\frac{2}{3}) = \frac{1}{3}$
348	347	oveq2d	$⊢ φ \to (L - 2) + 1 - (\frac{2}{3}) = L - 2 + (\frac{1}{3})$
349	337 340 348	3eqtrd	$⊢ φ \to L - 1 - (\frac{2}{3}) = L - 2 + (\frac{1}{3})$
350	136 22 24	redivcli	$⊢ \frac{2}{3} \in ℝ$
351	350	a1i	$⊢ φ \to \frac{2}{3} \in ℝ$
352		1lt2	$⊢ 1 < 2$
353	22 71	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
354	16 136 353	3pm3.2i	$⊢ (1 \in ℝ \land 2 \in ℝ \land (3 \in ℝ \land 0 < 3))$
355		ltdiv1	$⊢ (1 \in ℝ \land 2 \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (1 < 2 \leftrightarrow \frac{1}{3} < \frac{2}{3})$
356	354 355	mp1i	$⊢ φ \to (1 < 2 \leftrightarrow \frac{1}{3} < \frac{2}{3})$
357	352 356	mpbii	$⊢ φ \to \frac{1}{3} < \frac{2}{3}$
358	169 351 125 357	ltsub2dd	$⊢ φ \to L - 1 - (\frac{2}{3}) < L - 1 - (\frac{1}{3})$
359	349 358	eqbrtrrd	$⊢ φ \to L - 2 + (\frac{1}{3}) < L - 1 - (\frac{1}{3})$
360	316 319 11 359	ltmul1dd	$⊢ φ \to (L - 2 + (\frac{1}{3})) E < (L - 1 - (\frac{1}{3})) E$
361	35	simprd	$⊢ φ \to \neg S \in D (L - 1)$
362		oveq1	$⊢ j = L - 1 \to j - (\frac{1}{3}) = L - 1 - (\frac{1}{3})$
363	362	oveq1d	$⊢ j = L - 1 \to (j - (\frac{1}{3})) E = (L - 1 - (\frac{1}{3})) E$
364	363	breq2d	$⊢ j = L - 1 \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (L - 1 - (\frac{1}{3})) E)$
365	364	rabbidv	$⊢ j = L - 1 \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\}$
366	134	peano2zd	$⊢ φ \to N + 1 \in ℤ$
367	193	simpld	$⊢ φ \to 1 \leq L$
368	139 122	readdcld	$⊢ φ \to N + 1 \in ℝ$
369	139	lep1d	$⊢ φ \to N \leq N + 1$
370	114 139 368 194 369	letrd	$⊢ φ \to L \leq N + 1$
371	190 366 130 367 370	elfzd	$⊢ φ \to L \in (1 \dots N + 1)$
372	144 179	npcand	$⊢ φ \to L - 1 + 1 = L$
373		0p1e1	$⊢ 0 + 1 = 1$
374	373	a1i	$⊢ φ \to 0 + 1 = 1$
375	374	oveq1d	$⊢ φ \to (0 + 1 \dots N + 1) = (1 \dots N + 1)$
376	371 372 375	3eltr4d	$⊢ φ \to L - 1 + 1 \in (0 + 1 \dots N + 1)$
377		0zd	$⊢ φ \to 0 \in ℤ$
378	130 190	zsubcld	$⊢ φ \to L - 1 \in ℤ$
379		fzaddel	$⊢ ((0 \in ℤ \land N \in ℤ) \land (L - 1 \in ℤ \land 1 \in ℤ)) \to (L - 1 \in (0 \dots N) \leftrightarrow L - 1 + 1 \in (0 + 1 \dots N + 1))$
380	377 134 378 190 379	syl22anc	$⊢ φ \to (L - 1 \in (0 \dots N) \leftrightarrow L - 1 + 1 \in (0 + 1 \dots N + 1))$
381	376 380	mpbird	$⊢ φ \to L - 1 \in (0 \dots N)$
382		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\} \in V$
383	7 382	syl	$⊢ φ \to \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\} \in V$
384	4 365 381 383	fvmptd3	$⊢ φ \to D (L - 1) = \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\}$
385	361 384	neleqtrd	$⊢ φ \to \neg S \in \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\}$
386		nfcv	$⊢ \underline{Ⅎ} t (L - 1 - (\frac{1}{3})) E$
387	49 50 386	nfbr	$⊢ Ⅎ t F (S) \leq (L - 1 - (\frac{1}{3})) E$
388	53	breq1d	$⊢ t = S \to (F (t) \leq (L - 1 - (\frac{1}{3})) E \leftrightarrow F (S) \leq (L - 1 - (\frac{1}{3})) E)$
389	47 48 387 388	elrabf	$⊢ S \in \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\} \leftrightarrow (S \in T \land F (S) \leq (L - 1 - (\frac{1}{3})) E)$
390	385 389	sylnib	$⊢ φ \to \neg (S \in T \land F (S) \leq (L - 1 - (\frac{1}{3})) E)$
391		ianor	$⊢ \neg (S \in T \land F (S) \leq (L - 1 - (\frac{1}{3})) E) \leftrightarrow (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)$
392	390 391	sylib	$⊢ φ \to (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)$
393		olc	$⊢ S \in T \to (\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T)$
394	393	anim1i	$⊢ (S \in T \land (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)) \to ((\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T) \land (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E))$
395	57 392 394	syl2anc	$⊢ φ \to ((\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T) \land (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E))$
396		orcom	$⊢ (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E) \leftrightarrow (\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor \neg S \in T)$
397	396	anbi2i	$⊢ ((\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T) \land (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)) \leftrightarrow ((\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T) \land (\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor \neg S \in T))$
398	395 397	sylib	$⊢ φ \to ((\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T) \land (\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor \neg S \in T))$
399		pm4.43	$⊢ \neg F (S) \leq (L - 1 - (\frac{1}{3})) E \leftrightarrow ((\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T) \land (\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor \neg S \in T))$
400	398 399	sylibr	$⊢ φ \to \neg F (S) \leq (L - 1 - (\frac{1}{3})) E$
401	320 318	ltnled	$⊢ φ \to ((L - 1 - (\frac{1}{3})) E < F (S) \leftrightarrow \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)$
402	400 401	mpbird	$⊢ φ \to (L - 1 - (\frac{1}{3})) E < F (S)$
403	317 320 318 360 402	lttrd	$⊢ φ \to (L - 2 + (\frac{1}{3})) E < F (S)$
404	317 318 403	ltled	$⊢ φ \to (L - 2 + (\frac{1}{3})) E \leq F (S)$
405	404	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to (L - 2 + (\frac{1}{3})) E \leq F (S)$
406	297 302 306 314 405	letrd	$⊢ (φ \land i \in (0 \dots L - 2)) \to (i + (\frac{1}{3})) E \leq F (S)$
407		nfcv	$⊢ \underline{Ⅎ} t (i + (\frac{1}{3})) E$
408	407 50 49	nfbr	$⊢ Ⅎ t (i + (\frac{1}{3})) E \leq F (S)$
409	53	breq2d	$⊢ t = S \to ((i + (\frac{1}{3})) E \leq F (t) \leftrightarrow (i + (\frac{1}{3})) E \leq F (S))$
410	47 48 408 409	elrabf	$⊢ S \in \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \leftrightarrow (S \in T \land (i + (\frac{1}{3})) E \leq F (S))$
411	290 406 410	sylanbrc	$⊢ (φ \land i \in (0 \dots L - 2)) \to S \in \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\}$
412		oveq1	$⊢ j = i \to j + (\frac{1}{3}) = i + (\frac{1}{3})$
413	412	oveq1d	$⊢ j = i \to (j + (\frac{1}{3})) E = (i + (\frac{1}{3})) E$
414	413	breq1d	$⊢ j = i \to ((j + (\frac{1}{3})) E \leq F (t) \leftrightarrow (i + (\frac{1}{3})) E \leq F (t))$
415	414	rabbidv	$⊢ j = i \to \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} = \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\}$
416		rabexg	$⊢ T \in V \to \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \in V$
417	7 416	syl	$⊢ φ \to \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \in V$
418	417	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \in V$
419	5 415 155 418	fvmptd3	$⊢ (φ \land i \in (0 \dots L - 2)) \to B (i) = \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\}$
420	411 419	eleqtrrd	$⊢ (φ \land i \in (0 \dots L - 2)) \to S \in B (i)$
421	150	3ad2ant1	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to (L - 2 \in ℤ \land N \in ℤ \land L - 2 \leq N)$
422	421 151	sylibr	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to N \in ℤ_{\geq (L - 2)}$
423	422 153	syl	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to (0 \dots L - 2) \subseteq (0 \dots N)$
424		simp2	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to i \in (0 \dots L - 2)$
425	423 424	sseldd	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to i \in (0 \dots N)$
426		elex	$⊢ S \in B (i) \to S \in V$
427	426	3ad2ant3	$⊢ (φ \land i \in (0 \dots N) \land S \in B (i)) \to S \in V$
428		nfcv	$⊢ \underline{Ⅎ} t (0 \dots N)$
429		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
430	428 429	nfmpt	$⊢ \underline{Ⅎ} t (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
431	5 430	nfcxfr	$⊢ \underline{Ⅎ} t B$
432		nfcv	$⊢ \underline{Ⅎ} t i$
433	431 432	nffv	$⊢ \underline{Ⅎ} t B (i)$
434	433	nfel2	$⊢ Ⅎ t S \in B (i)$
435	3 96 434	nf3an	$⊢ Ⅎ t (φ \land i \in (0 \dots N) \land S \in B (i))$
436		nfv	$⊢ Ⅎ t 1 - (\frac{E}{N}) < X (i) (S)$
437	435 436	nfim	$⊢ Ⅎ t ((φ \land i \in (0 \dots N) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S))$
438		eleq1	$⊢ t = S \to (t \in B (i) \leftrightarrow S \in B (i))$
439	438	3anbi3d	$⊢ t = S \to ((φ \land i \in (0 \dots N) \land t \in B (i)) \leftrightarrow (φ \land i \in (0 \dots N) \land S \in B (i)))$
440	100	breq2d	$⊢ t = S \to (1 - (\frac{E}{N}) < X (i) (t) \leftrightarrow 1 - (\frac{E}{N}) < X (i) (S))$
441	439 440	imbi12d	$⊢ t = S \to (((φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)) \leftrightarrow ((φ \land i \in (0 \dots N) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S)))$
442	437 441 15	vtoclg1f	$⊢ S \in V \to ((φ \land i \in (0 \dots N) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S))$
443	427 442	mpcom	$⊢ (φ \land i \in (0 \dots N) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S)$
444	425 443	syld3an2	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S)$
445	420 444	mpd3an3	$⊢ (φ \land i \in (0 \dots L - 2)) \to 1 - (\frac{E}{N}) < X (i) (S)$
446	445	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to 1 - (\frac{E}{N}) < X (i) (S)$
447	283 285 286 289 446	fsumlt	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} (1 - (\frac{E}{N})) < \sum_{i = 0}^{L - 2} X (i) (S)$
448	282 447	eqbrtrrd	$⊢ (φ \land \neg L = 1) \to (1 - (\frac{E}{N})) (L - 1) < \sum_{i = 0}^{L - 2} X (i) (S)$
449	126	adantr	$⊢ (φ \land \neg L = 1) \to (1 - (\frac{E}{N})) (L - 1) \in ℝ$
450	157	adantr	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ$
451	310	adantr	$⊢ (φ \land \neg L = 1) \to (E \in ℝ \land 0 < E)$
452		ltmul2	$⊢ ((1 - (\frac{E}{N})) (L - 1) \in ℝ \land \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ \land (E \in ℝ \land 0 < E)) \to ((1 - (\frac{E}{N})) (L - 1) < \sum_{i = 0}^{L - 2} X (i) (S) \leftrightarrow E (1 - (\frac{E}{N})) (L - 1) < E \sum_{i = 0}^{L - 2} X (i) (S))$
453	449 450 451 452	syl3anc	$⊢ (φ \land \neg L = 1) \to ((1 - (\frac{E}{N})) (L - 1) < \sum_{i = 0}^{L - 2} X (i) (S) \leftrightarrow E (1 - (\frac{E}{N})) (L - 1) < E \sum_{i = 0}^{L - 2} X (i) (S))$
454	448 453	mpbid	$⊢ (φ \land \neg L = 1) \to E (1 - (\frac{E}{N})) (L - 1) < E \sum_{i = 0}^{L - 2} X (i) (S)$
455	121 128 159 231 454	lttrd	$⊢ (φ \land \neg L = 1) \to (L - (\frac{4}{3})) E < E \sum_{i = 0}^{L - 2} X (i) (S)$
456	155 60	syldan	$⊢ (φ \land i \in (0 \dots L - 2)) \to E X (i) (S) \in ℝ$
457	456	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to E X (i) (S) \in ℝ$
458	457	recnd	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to E X (i) (S) \in ℂ$
459	283 458	fsumcl	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) \in ℂ$
460	459	addridd	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) + 0 = \sum_{i = 0}^{L - 2} E X (i) (S)$
461		0red	$⊢ (φ \land \neg L = 1) \to 0 \in ℝ$
462		fzfid	$⊢ (φ \land \neg L = 1) \to (L - 1 \dots N) \in Fin$
463	28	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \in ℝ$
464		0zd	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \in ℤ$
465	134	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to N \in ℤ$
466		elfzelz	$⊢ i \in (L - 1 \dots N) \to i \in ℤ$
467	466	adantl	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in ℤ$
468		0red	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \in ℝ$
469	125	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to L - 1 \in ℝ$
470	466	zred	$⊢ i \in (L - 1 \dots N) \to i \in ℝ$
471	470	adantl	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in ℝ$
472		1m1e0	$⊢ 1 - 1 = 0$
473	122 114 122 367	lesub1dd	$⊢ φ \to 1 - 1 \leq L - 1$
474	472 473	eqbrtrrid	$⊢ φ \to 0 \leq L - 1$
475	474	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq L - 1$
476		simpr	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in (L - 1 \dots N)$
477	378	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to L - 1 \in ℤ$
478		elfz	$⊢ (i \in ℤ \land L - 1 \in ℤ \land N \in ℤ) \to (i \in (L - 1 \dots N) \leftrightarrow (L - 1 \leq i \land i \leq N))$
479	467 477 465 478	syl3anc	$⊢ (φ \land i \in (L - 1 \dots N)) \to (i \in (L - 1 \dots N) \leftrightarrow (L - 1 \leq i \land i \leq N))$
480	476 479	mpbid	$⊢ (φ \land i \in (L - 1 \dots N)) \to (L - 1 \leq i \land i \leq N)$
481	480	simpld	$⊢ (φ \land i \in (L - 1 \dots N)) \to L - 1 \leq i$
482	468 469 471 475 481	letrd	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq i$
483		elfzle2	$⊢ i \in (L - 1 \dots N) \to i \leq N$
484	483	adantl	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \leq N$
485	464 465 467 482 484	elfzd	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in (0 \dots N)$
486	485 59	syldan	$⊢ (φ \land i \in (L - 1 \dots N)) \to X (i) (S) \in ℝ$
487	463 486	remulcld	$⊢ (φ \land i \in (L - 1 \dots N)) \to E X (i) (S) \in ℝ$
488	487	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (L - 1 \dots N)) \to E X (i) (S) \in ℝ$
489	462 488	fsumrecl	$⊢ (φ \land \neg L = 1) \to \sum_{i = L - 1}^{N} E X (i) (S) \in ℝ$
490	283 457	fsumrecl	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) \in ℝ$
491		fzfid	$⊢ φ \to (L - 1 \dots N) \in Fin$
492	180	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \in ℂ$
493	492	mul01d	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \cdot 0 = 0$
494	485 106	syldan	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq X (i) (S)$
495	310	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to (E \in ℝ \land 0 < E)$
496		lemul2	$⊢ (0 \in ℝ \land X (i) (S) \in ℝ \land (E \in ℝ \land 0 < E)) \to (0 \leq X (i) (S) \leftrightarrow E \cdot 0 \leq E X (i) (S))$
497	468 486 495 496	syl3anc	$⊢ (φ \land i \in (L - 1 \dots N)) \to (0 \leq X (i) (S) \leftrightarrow E \cdot 0 \leq E X (i) (S))$
498	494 497	mpbid	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \cdot 0 \leq E X (i) (S)$
499	493 498	eqbrtrrd	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq E X (i) (S)$
500	491 487 499	fsumge0	$⊢ φ \to 0 \leq \sum_{i = L - 1}^{N} E X (i) (S)$
501	500	adantr	$⊢ (φ \land \neg L = 1) \to 0 \leq \sum_{i = L - 1}^{N} E X (i) (S)$
502	461 489 490 501	leadd2dd	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) + 0 \leq \sum_{i = 0}^{L - 2} E X (i) (S) + \sum_{i = L - 1}^{N} E X (i) (S)$
503	460 502	eqbrtrrd	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) \leq \sum_{i = 0}^{L - 2} E X (i) (S) + \sum_{i = L - 1}^{N} E X (i) (S)$
504	156	recnd	$⊢ (φ \land i \in (0 \dots L - 2)) \to X (i) (S) \in ℂ$
505	129 180 504	fsummulc2	$⊢ φ \to E \sum_{i = 0}^{L - 2} X (i) (S) = \sum_{i = 0}^{L - 2} E X (i) (S)$
506	505	adantr	$⊢ (φ \land \neg L = 1) \to E \sum_{i = 0}^{L - 2} X (i) (S) = \sum_{i = 0}^{L - 2} E X (i) (S)$
507		elfzelz	$⊢ j \in (0 \dots L - 2) \to j \in ℤ$
508	507	adantl	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \in ℤ$
509	508	zred	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \in ℝ$
510	315	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 2 \in ℝ$
511	125	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 1 \in ℝ$
512		simpr	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \in (0 \dots L - 2)$
513		0zd	$⊢ (φ \land j \in (0 \dots L - 2)) \to 0 \in ℤ$
514	133	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 2 \in ℤ$
515		elfz	$⊢ (j \in ℤ \land 0 \in ℤ \land L - 2 \in ℤ) \to (j \in (0 \dots L - 2) \leftrightarrow (0 \leq j \land j \leq L - 2))$
516	508 513 514 515	syl3anc	$⊢ (φ \land j \in (0 \dots L - 2)) \to (j \in (0 \dots L - 2) \leftrightarrow (0 \leq j \land j \leq L - 2))$
517	512 516	mpbid	$⊢ (φ \land j \in (0 \dots L - 2)) \to (0 \leq j \land j \leq L - 2)$
518	517	simprd	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \leq L - 2$
519	122 137 114	ltsub2d	$⊢ φ \to (1 < 2 \leftrightarrow L - 2 < L - 1)$
520	352 519	mpbii	$⊢ φ \to L - 2 < L - 1$
521	520	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 2 < L - 1$
522	509 510 511 518 521	lelttrd	$⊢ (φ \land j \in (0 \dots L - 2)) \to j < L - 1$
523	509 511	ltnled	$⊢ (φ \land j \in (0 \dots L - 2)) \to (j < L - 1 \leftrightarrow \neg L - 1 \leq j)$
524	522 523	mpbid	$⊢ (φ \land j \in (0 \dots L - 2)) \to \neg L - 1 \leq j$
525	524	intnanrd	$⊢ (φ \land j \in (0 \dots L - 2)) \to \neg (L - 1 \leq j \land j \leq N)$
526	378	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 1 \in ℤ$
527	134	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to N \in ℤ$
528		elfz	$⊢ (j \in ℤ \land L - 1 \in ℤ \land N \in ℤ) \to (j \in (L - 1 \dots N) \leftrightarrow (L - 1 \leq j \land j \leq N))$
529	508 526 527 528	syl3anc	$⊢ (φ \land j \in (0 \dots L - 2)) \to (j \in (L - 1 \dots N) \leftrightarrow (L - 1 \leq j \land j \leq N))$
530	525 529	mtbird	$⊢ (φ \land j \in (0 \dots L - 2)) \to \neg j \in (L - 1 \dots N)$
531	530	ex	$⊢ φ \to (j \in (0 \dots L - 2) \to \neg j \in (L - 1 \dots N))$
532	2 531	ralrimi	$⊢ φ \to \forall j \in (0 \dots L - 2) \neg j \in (L - 1 \dots N)$
533		disj	$⊢ (0 \dots L - 2) \cap (L - 1 \dots N) = \emptyset \leftrightarrow \forall j \in (0 \dots L - 2) \neg j \in (L - 1 \dots N)$
534	532 533	sylibr	$⊢ φ \to (0 \dots L - 2) \cap (L - 1 \dots N) = \emptyset$
535	534	adantr	$⊢ (φ \land \neg L = 1) \to (0 \dots L - 2) \cap (L - 1 \dots N) = \emptyset$
536	149	adantr	$⊢ (φ \land \neg L = 1) \to L - 2 \leq N$
537	133 377 134	3jca	$⊢ φ \to (L - 2 \in ℤ \land 0 \in ℤ \land N \in ℤ)$
538	537	adantr	$⊢ (φ \land \neg L = 1) \to (L - 2 \in ℤ \land 0 \in ℤ \land N \in ℤ)$
539		elfz	$⊢ (L - 2 \in ℤ \land 0 \in ℤ \land N \in ℤ) \to (L - 2 \in (0 \dots N) \leftrightarrow (0 \leq L - 2 \land L - 2 \leq N))$
540	538 539	syl	$⊢ (φ \land \neg L = 1) \to (L - 2 \in (0 \dots N) \leftrightarrow (0 \leq L - 2 \land L - 2 \leq N))$
541	256 536 540	mpbir2and	$⊢ (φ \land \neg L = 1) \to L - 2 \in (0 \dots N)$
542		fzsplit	$⊢ L - 2 \in (0 \dots N) \to (0 \dots N) = (0 \dots L - 2) \cup (L - 2 + 1 \dots N)$
543	541 542	syl	$⊢ (φ \land \neg L = 1) \to (0 \dots N) = (0 \dots L - 2) \cup (L - 2 + 1 \dots N)$
544	267 273 274	3eqtrd	$⊢ φ \to L - 2 + 1 = L - 1$
545	544	oveq1d	$⊢ φ \to (L - 2 + 1 \dots N) = (L - 1 \dots N)$
546	545	uneq2d	$⊢ φ \to (0 \dots L - 2) \cup (L - 2 + 1 \dots N) = (0 \dots L - 2) \cup (L - 1 \dots N)$
547	546	adantr	$⊢ (φ \land \neg L = 1) \to (0 \dots L - 2) \cup (L - 2 + 1 \dots N) = (0 \dots L - 2) \cup (L - 1 \dots N)$
548	543 547	eqtrd	$⊢ (φ \land \neg L = 1) \to (0 \dots N) = (0 \dots L - 2) \cup (L - 1 \dots N)$
549		fzfid	$⊢ (φ \land \neg L = 1) \to (0 \dots N) \in Fin$
550	180	adantr	$⊢ (φ \land i \in (0 \dots N)) \to E \in ℂ$
551	59	recnd	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (S) \in ℂ$
552	550 551	mulcld	$⊢ (φ \land i \in (0 \dots N)) \to E X (i) (S) \in ℂ$
553	552	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots N)) \to E X (i) (S) \in ℂ$
554	535 548 549 553	fsumsplit	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{N} E X (i) (S) = \sum_{i = 0}^{L - 2} E X (i) (S) + \sum_{i = L - 1}^{N} E X (i) (S)$
555	503 506 554	3brtr4d	$⊢ (φ \land \neg L = 1) \to E \sum_{i = 0}^{L - 2} X (i) (S) \leq \sum_{i = 0}^{N} E X (i) (S)$
556	120 158 61	3jca	$⊢ φ \to ((L - (\frac{4}{3})) E \in ℝ \land E \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ \land \sum_{i = 0}^{N} E X (i) (S) \in ℝ)$
557	556	adantr	$⊢ (φ \land \neg L = 1) \to ((L - (\frac{4}{3})) E \in ℝ \land E \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ \land \sum_{i = 0}^{N} E X (i) (S) \in ℝ)$
558		ltletr	$⊢ ((L - (\frac{4}{3})) E \in ℝ \land E \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ \land \sum_{i = 0}^{N} E X (i) (S) \in ℝ) \to (((L - (\frac{4}{3})) E < E \sum_{i = 0}^{L - 2} X (i) (S) \land E \sum_{i = 0}^{L - 2} X (i) (S) \leq \sum_{i = 0}^{N} E X (i) (S)) \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S))$
559	557 558	syl	$⊢ (φ \land \neg L = 1) \to (((L - (\frac{4}{3})) E < E \sum_{i = 0}^{L - 2} X (i) (S) \land E \sum_{i = 0}^{L - 2} X (i) (S) \leq \sum_{i = 0}^{N} E X (i) (S)) \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S))$
560	455 555 559	mp2and	$⊢ (φ \land \neg L = 1) \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S)$
561	111 560	pm2.61dan	$⊢ φ \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S)$
562		sumex	$⊢ \sum_{i = 0}^{N} E X (i) (S) \in V$
563	100	oveq2d	$⊢ t = S \to E X (i) (t) = E X (i) (S)$
564	563	sumeq2sdv	$⊢ t = S \to \sum_{i = 0}^{N} E X (i) (t) = \sum_{i = 0}^{N} E X (i) (S)$
565		eqid	$⊢ (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) = (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t))$
566	564 565	fvmptg	$⊢ (S \in T \land \sum_{i = 0}^{N} E X (i) (S) \in V) \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (S) = \sum_{i = 0}^{N} E X (i) (S)$
567	57 562 566	sylancl	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (S) = \sum_{i = 0}^{N} E X (i) (S)$
568	561 567	breqtrrd	$⊢ φ \to (L - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (S)$

Metamath Proof Explorer

Theorem stoweidlem26

Proof