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	sseldi	$⊢ φ \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	ffvelrnd	$⊢ (φ \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 112	syl	$⊢ φ \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	mulid1d	$⊢ φ \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	mulid2d	$⊢ φ \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 112	syl	$⊢ (φ \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		ffvelrn	$⊢ (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	ffvelrnd	$⊢ φ \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		addid1	$⊢ 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	193	simpld	$⊢ φ \to 1 \leq L$
367	139 122	readdcld	$⊢ φ \to N + 1 \in ℝ$
368	139	lep1d	$⊢ φ \to N \leq N + 1$
369	114 139 367 194 368	letrd	$⊢ φ \to L \leq N + 1$
370	134	peano2zd	$⊢ φ \to N + 1 \in ℤ$
371		elfz	$⊢ (L \in ℤ \land 1 \in ℤ \land N + 1 \in ℤ) \to (L \in (1 \dots N + 1) \leftrightarrow (1 \leq L \land L \leq N + 1))$
372	130 190 370 371	syl3anc	$⊢ φ \to (L \in (1 \dots N + 1) \leftrightarrow (1 \leq L \land L \leq N + 1))$
373	366 369 372	mpbir2and	$⊢ φ \to L \in (1 \dots N + 1)$
374	144 179	npcand	$⊢ φ \to L - 1 + 1 = L$
375		0p1e1	$⊢ 0 + 1 = 1$
376	375	a1i	$⊢ φ \to 0 + 1 = 1$
377	376	oveq1d	$⊢ φ \to (0 + 1 \dots N + 1) = (1 \dots N + 1)$
378	373 374 377	3eltr4d	$⊢ φ \to L - 1 + 1 \in (0 + 1 \dots N + 1)$
379		0zd	$⊢ φ \to 0 \in ℤ$
380	130 190	zsubcld	$⊢ φ \to L - 1 \in ℤ$
381		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))$
382	379 134 380 190 381	syl22anc	$⊢ φ \to (L - 1 \in (0 \dots N) \leftrightarrow L - 1 + 1 \in (0 + 1 \dots N + 1))$
383	378 382	mpbird	$⊢ φ \to L - 1 \in (0 \dots N)$
384		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\} \in V$
385	7 384	syl	$⊢ φ \to \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\} \in V$
386	4 365 383 385	fvmptd3	$⊢ φ \to D (L - 1) = \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\}$
387	361 386	neleqtrd	$⊢ φ \to \neg S \in \{t \in T \| F (t) \leq (L - 1 - (\frac{1}{3})) E\}$
388		nfcv	$⊢ \underline{Ⅎ} t (L - 1 - (\frac{1}{3})) E$
389	49 50 388	nfbr	$⊢ Ⅎ t F (S) \leq (L - 1 - (\frac{1}{3})) E$
390	53	breq1d	$⊢ t = S \to (F (t) \leq (L - 1 - (\frac{1}{3})) E \leftrightarrow F (S) \leq (L - 1 - (\frac{1}{3})) E)$
391	47 48 389 390	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)$
392	387 391	sylnib	$⊢ φ \to \neg (S \in T \land F (S) \leq (L - 1 - (\frac{1}{3})) E)$
393		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)$
394	392 393	sylib	$⊢ φ \to (\neg S \in T \lor \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)$
395		olc	$⊢ S \in T \to (\neg F (S) \leq (L - 1 - (\frac{1}{3})) E \lor S \in T)$
396	395	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))$
397	57 394 396	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))$
398		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)$
399	398	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))$
400	397 399	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))$
401		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))$
402	400 401	sylibr	$⊢ φ \to \neg F (S) \leq (L - 1 - (\frac{1}{3})) E$
403	320 318	ltnled	$⊢ φ \to ((L - 1 - (\frac{1}{3})) E < F (S) \leftrightarrow \neg F (S) \leq (L - 1 - (\frac{1}{3})) E)$
404	402 403	mpbird	$⊢ φ \to (L - 1 - (\frac{1}{3})) E < F (S)$
405	317 320 318 360 404	lttrd	$⊢ φ \to (L - 2 + (\frac{1}{3})) E < F (S)$
406	317 318 405	ltled	$⊢ φ \to (L - 2 + (\frac{1}{3})) E \leq F (S)$
407	406	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to (L - 2 + (\frac{1}{3})) E \leq F (S)$
408	297 302 306 314 407	letrd	$⊢ (φ \land i \in (0 \dots L - 2)) \to (i + (\frac{1}{3})) E \leq F (S)$
409		nfcv	$⊢ \underline{Ⅎ} t (i + (\frac{1}{3})) E$
410	409 50 49	nfbr	$⊢ Ⅎ t (i + (\frac{1}{3})) E \leq F (S)$
411	53	breq2d	$⊢ t = S \to ((i + (\frac{1}{3})) E \leq F (t) \leftrightarrow (i + (\frac{1}{3})) E \leq F (S))$
412	47 48 410 411	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))$
413	290 408 412	sylanbrc	$⊢ (φ \land i \in (0 \dots L - 2)) \to S \in \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\}$
414		oveq1	$⊢ j = i \to j + (\frac{1}{3}) = i + (\frac{1}{3})$
415	414	oveq1d	$⊢ j = i \to (j + (\frac{1}{3})) E = (i + (\frac{1}{3})) E$
416	415	breq1d	$⊢ j = i \to ((j + (\frac{1}{3})) E \leq F (t) \leftrightarrow (i + (\frac{1}{3})) E \leq F (t))$
417	416	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)\}$
418		rabexg	$⊢ T \in V \to \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \in V$
419	7 418	syl	$⊢ φ \to \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \in V$
420	419	adantr	$⊢ (φ \land i \in (0 \dots L - 2)) \to \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\} \in V$
421	5 417 155 420	fvmptd3	$⊢ (φ \land i \in (0 \dots L - 2)) \to B (i) = \{t \in T \| (i + (\frac{1}{3})) E \leq F (t)\}$
422	413 421	eleqtrrd	$⊢ (φ \land i \in (0 \dots L - 2)) \to S \in B (i)$
423	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)$
424	423 151	sylibr	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to N \in ℤ_{\geq (L - 2)}$
425	424 153	syl	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to (0 \dots L - 2) \subseteq (0 \dots N)$
426		simp2	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to i \in (0 \dots L - 2)$
427	425 426	sseldd	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to i \in (0 \dots N)$
428		elex	$⊢ S \in B (i) \to S \in V$
429	428	3ad2ant3	$⊢ (φ \land i \in (0 \dots N) \land S \in B (i)) \to S \in V$
430		nfcv	$⊢ \underline{Ⅎ} t (0 \dots N)$
431		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
432	430 431	nfmpt	$⊢ \underline{Ⅎ} t (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
433	5 432	nfcxfr	$⊢ \underline{Ⅎ} t B$
434		nfcv	$⊢ \underline{Ⅎ} t i$
435	433 434	nffv	$⊢ \underline{Ⅎ} t B (i)$
436	435	nfel2	$⊢ Ⅎ t S \in B (i)$
437	3 96 436	nf3an	$⊢ Ⅎ t (φ \land i \in (0 \dots N) \land S \in B (i))$
438		nfv	$⊢ Ⅎ t 1 - (\frac{E}{N}) < X (i) (S)$
439	437 438	nfim	$⊢ Ⅎ t ((φ \land i \in (0 \dots N) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S))$
440		eleq1	$⊢ t = S \to (t \in B (i) \leftrightarrow S \in B (i))$
441	440	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)))$
442	100	breq2d	$⊢ t = S \to (1 - (\frac{E}{N}) < X (i) (t) \leftrightarrow 1 - (\frac{E}{N}) < X (i) (S))$
443	441 442	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)))$
444	439 443 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))$
445	429 444	mpcom	$⊢ (φ \land i \in (0 \dots N) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S)$
446	427 445	syld3an2	$⊢ (φ \land i \in (0 \dots L - 2) \land S \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (S)$
447	422 446	mpd3an3	$⊢ (φ \land i \in (0 \dots L - 2)) \to 1 - (\frac{E}{N}) < X (i) (S)$
448	447	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to 1 - (\frac{E}{N}) < X (i) (S)$
449	283 285 286 289 448	fsumlt	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} (1 - (\frac{E}{N})) < \sum_{i = 0}^{L - 2} X (i) (S)$
450	282 449	eqbrtrrd	$⊢ (φ \land \neg L = 1) \to (1 - (\frac{E}{N})) (L - 1) < \sum_{i = 0}^{L - 2} X (i) (S)$
451	126	adantr	$⊢ (φ \land \neg L = 1) \to (1 - (\frac{E}{N})) (L - 1) \in ℝ$
452	157	adantr	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} X (i) (S) \in ℝ$
453	310	adantr	$⊢ (φ \land \neg L = 1) \to (E \in ℝ \land 0 < E)$
454		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))$
455	451 452 453 454	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))$
456	450 455	mpbid	$⊢ (φ \land \neg L = 1) \to E (1 - (\frac{E}{N})) (L - 1) < E \sum_{i = 0}^{L - 2} X (i) (S)$
457	121 128 159 231 456	lttrd	$⊢ (φ \land \neg L = 1) \to (L - (\frac{4}{3})) E < E \sum_{i = 0}^{L - 2} X (i) (S)$
458	155 60	syldan	$⊢ (φ \land i \in (0 \dots L - 2)) \to E X (i) (S) \in ℝ$
459	458	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to E X (i) (S) \in ℝ$
460	459	recnd	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots L - 2)) \to E X (i) (S) \in ℂ$
461	283 460	fsumcl	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) \in ℂ$
462	461	addid1d	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) + 0 = \sum_{i = 0}^{L - 2} E X (i) (S)$
463		0red	$⊢ (φ \land \neg L = 1) \to 0 \in ℝ$
464		fzfid	$⊢ (φ \land \neg L = 1) \to (L - 1 \dots N) \in Fin$
465	28	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \in ℝ$
466		0red	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \in ℝ$
467	125	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to L - 1 \in ℝ$
468		elfzelz	$⊢ i \in (L - 1 \dots N) \to i \in ℤ$
469	468	zred	$⊢ i \in (L - 1 \dots N) \to i \in ℝ$
470	469	adantl	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in ℝ$
471		1m1e0	$⊢ 1 - 1 = 0$
472	122 114 122 366	lesub1dd	$⊢ φ \to 1 - 1 \leq L - 1$
473	471 472	eqbrtrrid	$⊢ φ \to 0 \leq L - 1$
474	473	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq L - 1$
475		simpr	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in (L - 1 \dots N)$
476	468	adantl	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in ℤ$
477	380	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to L - 1 \in ℤ$
478	134	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to N \in ℤ$
479		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))$
480	476 477 478 479	syl3anc	$⊢ (φ \land i \in (L - 1 \dots N)) \to (i \in (L - 1 \dots N) \leftrightarrow (L - 1 \leq i \land i \leq N))$
481	475 480	mpbid	$⊢ (φ \land i \in (L - 1 \dots N)) \to (L - 1 \leq i \land i \leq N)$
482	481	simpld	$⊢ (φ \land i \in (L - 1 \dots N)) \to L - 1 \leq i$
483	466 467 470 474 482	letrd	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq i$
484		elfzle2	$⊢ i \in (L - 1 \dots N) \to i \leq N$
485	484	adantl	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \leq N$
486		0zd	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \in ℤ$
487		elfz	$⊢ (i \in ℤ \land 0 \in ℤ \land N \in ℤ) \to (i \in (0 \dots N) \leftrightarrow (0 \leq i \land i \leq N))$
488	476 486 478 487	syl3anc	$⊢ (φ \land i \in (L - 1 \dots N)) \to (i \in (0 \dots N) \leftrightarrow (0 \leq i \land i \leq N))$
489	483 485 488	mpbir2and	$⊢ (φ \land i \in (L - 1 \dots N)) \to i \in (0 \dots N)$
490	489 59	syldan	$⊢ (φ \land i \in (L - 1 \dots N)) \to X (i) (S) \in ℝ$
491	465 490	remulcld	$⊢ (φ \land i \in (L - 1 \dots N)) \to E X (i) (S) \in ℝ$
492	491	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (L - 1 \dots N)) \to E X (i) (S) \in ℝ$
493	464 492	fsumrecl	$⊢ (φ \land \neg L = 1) \to \sum_{i = L - 1}^{N} E X (i) (S) \in ℝ$
494	283 459	fsumrecl	$⊢ (φ \land \neg L = 1) \to \sum_{i = 0}^{L - 2} E X (i) (S) \in ℝ$
495		fzfid	$⊢ φ \to (L - 1 \dots N) \in Fin$
496	180	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \in ℂ$
497	496	mul01d	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \cdot 0 = 0$
498	489 106	syldan	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq X (i) (S)$
499	310	adantr	$⊢ (φ \land i \in (L - 1 \dots N)) \to (E \in ℝ \land 0 < E)$
500		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))$
501	466 490 499 500	syl3anc	$⊢ (φ \land i \in (L - 1 \dots N)) \to (0 \leq X (i) (S) \leftrightarrow E \cdot 0 \leq E X (i) (S))$
502	498 501	mpbid	$⊢ (φ \land i \in (L - 1 \dots N)) \to E \cdot 0 \leq E X (i) (S)$
503	497 502	eqbrtrrd	$⊢ (φ \land i \in (L - 1 \dots N)) \to 0 \leq E X (i) (S)$
504	495 491 503	fsumge0	$⊢ φ \to 0 \leq \sum_{i = L - 1}^{N} E X (i) (S)$
505	504	adantr	$⊢ (φ \land \neg L = 1) \to 0 \leq \sum_{i = L - 1}^{N} E X (i) (S)$
506	463 493 494 505	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)$
507	462 506	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)$
508	156	recnd	$⊢ (φ \land i \in (0 \dots L - 2)) \to X (i) (S) \in ℂ$
509	129 180 508	fsummulc2	$⊢ φ \to E \sum_{i = 0}^{L - 2} X (i) (S) = \sum_{i = 0}^{L - 2} E X (i) (S)$
510	509	adantr	$⊢ (φ \land \neg L = 1) \to E \sum_{i = 0}^{L - 2} X (i) (S) = \sum_{i = 0}^{L - 2} E X (i) (S)$
511		elfzelz	$⊢ j \in (0 \dots L - 2) \to j \in ℤ$
512	511	adantl	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \in ℤ$
513	512	zred	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \in ℝ$
514	315	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 2 \in ℝ$
515	125	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 1 \in ℝ$
516		simpr	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \in (0 \dots L - 2)$
517		0zd	$⊢ (φ \land j \in (0 \dots L - 2)) \to 0 \in ℤ$
518	133	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 2 \in ℤ$
519		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))$
520	512 517 518 519	syl3anc	$⊢ (φ \land j \in (0 \dots L - 2)) \to (j \in (0 \dots L - 2) \leftrightarrow (0 \leq j \land j \leq L - 2))$
521	516 520	mpbid	$⊢ (φ \land j \in (0 \dots L - 2)) \to (0 \leq j \land j \leq L - 2)$
522	521	simprd	$⊢ (φ \land j \in (0 \dots L - 2)) \to j \leq L - 2$
523	122 137 114	ltsub2d	$⊢ φ \to (1 < 2 \leftrightarrow L - 2 < L - 1)$
524	352 523	mpbii	$⊢ φ \to L - 2 < L - 1$
525	524	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 2 < L - 1$
526	513 514 515 522 525	lelttrd	$⊢ (φ \land j \in (0 \dots L - 2)) \to j < L - 1$
527	513 515	ltnled	$⊢ (φ \land j \in (0 \dots L - 2)) \to (j < L - 1 \leftrightarrow \neg L - 1 \leq j)$
528	526 527	mpbid	$⊢ (φ \land j \in (0 \dots L - 2)) \to \neg L - 1 \leq j$
529	528	intnanrd	$⊢ (φ \land j \in (0 \dots L - 2)) \to \neg (L - 1 \leq j \land j \leq N)$
530	380	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to L - 1 \in ℤ$
531	134	adantr	$⊢ (φ \land j \in (0 \dots L - 2)) \to N \in ℤ$
532		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))$
533	512 530 531 532	syl3anc	$⊢ (φ \land j \in (0 \dots L - 2)) \to (j \in (L - 1 \dots N) \leftrightarrow (L - 1 \leq j \land j \leq N))$
534	529 533	mtbird	$⊢ (φ \land j \in (0 \dots L - 2)) \to \neg j \in (L - 1 \dots N)$
535	534	ex	$⊢ φ \to (j \in (0 \dots L - 2) \to \neg j \in (L - 1 \dots N))$
536	2 535	ralrimi	$⊢ φ \to \forall j \in (0 \dots L - 2) \neg j \in (L - 1 \dots N)$
537		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)$
538	536 537	sylibr	$⊢ φ \to (0 \dots L - 2) \cap (L - 1 \dots N) = \emptyset$
539	538	adantr	$⊢ (φ \land \neg L = 1) \to (0 \dots L - 2) \cap (L - 1 \dots N) = \emptyset$
540	149	adantr	$⊢ (φ \land \neg L = 1) \to L - 2 \leq N$
541	133 379 134	3jca	$⊢ φ \to (L - 2 \in ℤ \land 0 \in ℤ \land N \in ℤ)$
542	541	adantr	$⊢ (φ \land \neg L = 1) \to (L - 2 \in ℤ \land 0 \in ℤ \land N \in ℤ)$
543		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))$
544	542 543	syl	$⊢ (φ \land \neg L = 1) \to (L - 2 \in (0 \dots N) \leftrightarrow (0 \leq L - 2 \land L - 2 \leq N))$
545	256 540 544	mpbir2and	$⊢ (φ \land \neg L = 1) \to L - 2 \in (0 \dots N)$
546		fzsplit	$⊢ L - 2 \in (0 \dots N) \to (0 \dots N) = (0 \dots L - 2) \cup (L - 2 + 1 \dots N)$
547	545 546	syl	$⊢ (φ \land \neg L = 1) \to (0 \dots N) = (0 \dots L - 2) \cup (L - 2 + 1 \dots N)$
548	267 273 274	3eqtrd	$⊢ φ \to L - 2 + 1 = L - 1$
549	548	oveq1d	$⊢ φ \to (L - 2 + 1 \dots N) = (L - 1 \dots N)$
550	549	uneq2d	$⊢ φ \to (0 \dots L - 2) \cup (L - 2 + 1 \dots N) = (0 \dots L - 2) \cup (L - 1 \dots N)$
551	550	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)$
552	547 551	eqtrd	$⊢ (φ \land \neg L = 1) \to (0 \dots N) = (0 \dots L - 2) \cup (L - 1 \dots N)$
553		fzfid	$⊢ (φ \land \neg L = 1) \to (0 \dots N) \in Fin$
554	180	adantr	$⊢ (φ \land i \in (0 \dots N)) \to E \in ℂ$
555	59	recnd	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (S) \in ℂ$
556	554 555	mulcld	$⊢ (φ \land i \in (0 \dots N)) \to E X (i) (S) \in ℂ$
557	556	adantlr	$⊢ ((φ \land \neg L = 1) \land i \in (0 \dots N)) \to E X (i) (S) \in ℂ$
558	539 552 553 557	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)$
559	507 510 558	3brtr4d	$⊢ (φ \land \neg L = 1) \to E \sum_{i = 0}^{L - 2} X (i) (S) \leq \sum_{i = 0}^{N} E X (i) (S)$
560	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 ℝ)$
561	560	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 ℝ)$
562		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))$
563	561 562	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))$
564	457 559 563	mp2and	$⊢ (φ \land \neg L = 1) \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S)$
565	111 564	pm2.61dan	$⊢ φ \to (L - (\frac{4}{3})) E < \sum_{i = 0}^{N} E X (i) (S)$
566		sumex	$⊢ \sum_{i = 0}^{N} E X (i) (S) \in V$
567	100	oveq2d	$⊢ t = S \to E X (i) (t) = E X (i) (S)$
568	567	sumeq2sdv	$⊢ t = S \to \sum_{i = 0}^{N} E X (i) (t) = \sum_{i = 0}^{N} E X (i) (S)$
569		eqid	$⊢ (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) = (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t))$
570	568 569	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)$
571	57 566 570	sylancl	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (S) = \sum_{i = 0}^{N} E X (i) (S)$
572	565 571	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