stoweidlem11

Description: This lemma is used to prove that there is a function g as in the proof of BrosowskiDeutsh p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem11.1	$⊢ φ \to N \in ℕ$
	stoweidlem11.2	$⊢ φ \to t \in T$
	stoweidlem11.3	$⊢ φ \to j \in (1 \dots N)$
	stoweidlem11.4	$⊢ (φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
	stoweidlem11.5	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (t) \leq 1$
	stoweidlem11.6	$⊢ (φ \land i \in (j \dots N)) \to X (i) (t) < \frac{E}{N}$
	stoweidlem11.7	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem11.8	$⊢ φ \to E < \frac{1}{3}$
Assertion	stoweidlem11	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem11.1	$⊢ φ \to N \in ℕ$
2		stoweidlem11.2	$⊢ φ \to t \in T$
3		stoweidlem11.3	$⊢ φ \to j \in (1 \dots N)$
4		stoweidlem11.4	$⊢ (φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
5		stoweidlem11.5	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (t) \leq 1$
6		stoweidlem11.6	$⊢ (φ \land i \in (j \dots N)) \to X (i) (t) < \frac{E}{N}$
7		stoweidlem11.7	$⊢ φ \to E \in ℝ^{+}$
8		stoweidlem11.8	$⊢ φ \to E < \frac{1}{3}$
9		sumex	$⊢ \sum_{i = 0}^{N} E X (i) (t) \in V$
10		eqid	$⊢ (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) = (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t))$
11	10	fvmpt2	$⊢ (t \in T \land \sum_{i = 0}^{N} E X (i) (t) \in V) \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) = \sum_{i = 0}^{N} E X (i) (t)$
12	2 9 11	sylancl	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) = \sum_{i = 0}^{N} E X (i) (t)$
13		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
14	7	rpred	$⊢ φ \to E \in ℝ$
15	14	adantr	$⊢ (φ \land i \in (0 \dots N)) \to E \in ℝ$
16	2	adantr	$⊢ (φ \land i \in (0 \dots N)) \to t \in T$
17	4 16	ffvelrnd	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (t) \in ℝ$
18	15 17	remulcld	$⊢ (φ \land i \in (0 \dots N)) \to E X (i) (t) \in ℝ$
19	13 18	fsumrecl	$⊢ φ \to \sum_{i = 0}^{N} E X (i) (t) \in ℝ$
20	3	elfzelzd	$⊢ φ \to j \in ℤ$
21	20	zred	$⊢ φ \to j \in ℝ$
22	14 21	remulcld	$⊢ φ \to E j \in ℝ$
23	1	nnred	$⊢ φ \to N \in ℝ$
24	23 21	resubcld	$⊢ φ \to N - j \in ℝ$
25		1red	$⊢ φ \to 1 \in ℝ$
26	24 25	readdcld	$⊢ φ \to N - j + 1 \in ℝ$
27	14 1	nndivred	$⊢ φ \to \frac{E}{N} \in ℝ$
28	14 27	remulcld	$⊢ φ \to E (\frac{E}{N}) \in ℝ$
29	26 28	remulcld	$⊢ φ \to (N - j + 1) E (\frac{E}{N}) \in ℝ$
30	22 29	readdcld	$⊢ φ \to E j + (N - j + 1) E (\frac{E}{N}) \in ℝ$
31		3re	$⊢ 3 \in ℝ$
32	31	a1i	$⊢ φ \to 3 \in ℝ$
33		3ne0	$⊢ 3 \neq 0$
34	33	a1i	$⊢ φ \to 3 \neq 0$
35	32 34	rereccld	$⊢ φ \to \frac{1}{3} \in ℝ$
36	21 35	readdcld	$⊢ φ \to j + (\frac{1}{3}) \in ℝ$
37	36 14	remulcld	$⊢ φ \to (j + (\frac{1}{3})) E \in ℝ$
38		fzfid	$⊢ φ \to (0 \dots j - 1) \in Fin$
39	14	adantr	$⊢ (φ \land i \in (0 \dots j - 1)) \to E \in ℝ$
40		elfzelz	$⊢ j \in (1 \dots N) \to j \in ℤ$
41		peano2zm	$⊢ j \in ℤ \to j - 1 \in ℤ$
42	3 40 41	3syl	$⊢ φ \to j - 1 \in ℤ$
43	1	nnzd	$⊢ φ \to N \in ℤ$
44	21 25	resubcld	$⊢ φ \to j - 1 \in ℝ$
45	21	lem1d	$⊢ φ \to j - 1 \leq j$
46		elfzuz3	$⊢ j \in (1 \dots N) \to N \in ℤ_{\geq j}$
47		eluzle	$⊢ N \in ℤ_{\geq j} \to j \leq N$
48	3 46 47	3syl	$⊢ φ \to j \leq N$
49	44 21 23 45 48	letrd	$⊢ φ \to j - 1 \leq N$
50		eluz2	$⊢ N \in ℤ_{\geq (j - 1)} \leftrightarrow (j - 1 \in ℤ \land N \in ℤ \land j - 1 \leq N)$
51	42 43 49 50	syl3anbrc	$⊢ φ \to N \in ℤ_{\geq (j - 1)}$
52		fzss2	$⊢ N \in ℤ_{\geq (j - 1)} \to (0 \dots j - 1) \subseteq (0 \dots N)$
53	51 52	syl	$⊢ φ \to (0 \dots j - 1) \subseteq (0 \dots N)$
54	53	sselda	$⊢ (φ \land i \in (0 \dots j - 1)) \to i \in (0 \dots N)$
55	54 17	syldan	$⊢ (φ \land i \in (0 \dots j - 1)) \to X (i) (t) \in ℝ$
56	39 55	remulcld	$⊢ (φ \land i \in (0 \dots j - 1)) \to E X (i) (t) \in ℝ$
57	38 56	fsumrecl	$⊢ φ \to \sum_{i = 0}^{j - 1} E X (i) (t) \in ℝ$
58	57 29	readdcld	$⊢ φ \to \sum_{i = 0}^{j - 1} E X (i) (t) + (N - j + 1) E (\frac{E}{N}) \in ℝ$
59	21	ltm1d	$⊢ φ \to j - 1 < j$
60		fzdisj	$⊢ j - 1 < j \to (0 \dots j - 1) \cap (j \dots N) = \emptyset$
61	59 60	syl	$⊢ φ \to (0 \dots j - 1) \cap (j \dots N) = \emptyset$
62		fzssp1	$⊢ (0 \dots N - 1) \subseteq (0 \dots N - 1 + 1)$
63	1	nncnd	$⊢ φ \to N \in ℂ$
64		1cnd	$⊢ φ \to 1 \in ℂ$
65	63 64	npcand	$⊢ φ \to N - 1 + 1 = N$
66	65	oveq2d	$⊢ φ \to (0 \dots N - 1 + 1) = (0 \dots N)$
67	62 66	sseqtrid	$⊢ φ \to (0 \dots N - 1) \subseteq (0 \dots N)$
68		1zzd	$⊢ φ \to 1 \in ℤ$
69		fzsubel	$⊢ ((1 \in ℤ \land N \in ℤ) \land (j \in ℤ \land 1 \in ℤ)) \to (j \in (1 \dots N) \leftrightarrow j - 1 \in (1 - 1 \dots N - 1))$
70	68 43 20 68 69	syl22anc	$⊢ φ \to (j \in (1 \dots N) \leftrightarrow j - 1 \in (1 - 1 \dots N - 1))$
71	3 70	mpbid	$⊢ φ \to j - 1 \in (1 - 1 \dots N - 1)$
72		1m1e0	$⊢ 1 - 1 = 0$
73	72	oveq1i	$⊢ (1 - 1 \dots N - 1) = (0 \dots N - 1)$
74	71 73	eleqtrdi	$⊢ φ \to j - 1 \in (0 \dots N - 1)$
75	67 74	sseldd	$⊢ φ \to j - 1 \in (0 \dots N)$
76		fzsplit	$⊢ j - 1 \in (0 \dots N) \to (0 \dots N) = (0 \dots j - 1) \cup (j - 1 + 1 \dots N)$
77	75 76	syl	$⊢ φ \to (0 \dots N) = (0 \dots j - 1) \cup (j - 1 + 1 \dots N)$
78	20	zcnd	$⊢ φ \to j \in ℂ$
79	78 64	npcand	$⊢ φ \to j - 1 + 1 = j$
80	79	oveq1d	$⊢ φ \to (j - 1 + 1 \dots N) = (j \dots N)$
81	80	uneq2d	$⊢ φ \to (0 \dots j - 1) \cup (j - 1 + 1 \dots N) = (0 \dots j - 1) \cup (j \dots N)$
82	77 81	eqtrd	$⊢ φ \to (0 \dots N) = (0 \dots j - 1) \cup (j \dots N)$
83	7	rpcnd	$⊢ φ \to E \in ℂ$
84	83	adantr	$⊢ (φ \land i \in (0 \dots N)) \to E \in ℂ$
85	17	recnd	$⊢ (φ \land i \in (0 \dots N)) \to X (i) (t) \in ℂ$
86	84 85	mulcld	$⊢ (φ \land i \in (0 \dots N)) \to E X (i) (t) \in ℂ$
87	61 82 13 86	fsumsplit	$⊢ φ \to \sum_{i = 0}^{N} E X (i) (t) = \sum_{i = 0}^{j - 1} E X (i) (t) + \sum_{i = j}^{N} E X (i) (t)$
88		fzfid	$⊢ φ \to (j \dots N) \in Fin$
89	14	adantr	$⊢ (φ \land i \in (j \dots N)) \to E \in ℝ$
90		0zd	$⊢ φ \to 0 \in ℤ$
91		0red	$⊢ φ \to 0 \in ℝ$
92		0le1	$⊢ 0 \leq 1$
93	92	a1i	$⊢ φ \to 0 \leq 1$
94		elfzuz	$⊢ j \in (1 \dots N) \to j \in ℤ_{\geq 1}$
95	3 94	syl	$⊢ φ \to j \in ℤ_{\geq 1}$
96		eluz2	$⊢ j \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land j \in ℤ \land 1 \leq j)$
97	95 96	sylib	$⊢ φ \to (1 \in ℤ \land j \in ℤ \land 1 \leq j)$
98	97	simp3d	$⊢ φ \to 1 \leq j$
99	91 25 21 93 98	letrd	$⊢ φ \to 0 \leq j$
100		eluz2	$⊢ j \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land j \in ℤ \land 0 \leq j)$
101	90 20 99 100	syl3anbrc	$⊢ φ \to j \in ℤ_{\geq 0}$
102		fzss1	$⊢ j \in ℤ_{\geq 0} \to (j \dots N) \subseteq (0 \dots N)$
103	101 102	syl	$⊢ φ \to (j \dots N) \subseteq (0 \dots N)$
104	103	sselda	$⊢ (φ \land i \in (j \dots N)) \to i \in (0 \dots N)$
105	104 4	syldan	$⊢ (φ \land i \in (j \dots N)) \to X (i) : T ⟶ ℝ$
106	2	adantr	$⊢ (φ \land i \in (j \dots N)) \to t \in T$
107	105 106	ffvelrnd	$⊢ (φ \land i \in (j \dots N)) \to X (i) (t) \in ℝ$
108	89 107	remulcld	$⊢ (φ \land i \in (j \dots N)) \to E X (i) (t) \in ℝ$
109	88 108	fsumrecl	$⊢ φ \to \sum_{i = j}^{N} E X (i) (t) \in ℝ$
110		eluzfz2	$⊢ N \in ℤ_{\geq j} \to N \in (j \dots N)$
111		ne0i	$⊢ N \in (j \dots N) \to (j \dots N) \neq \emptyset$
112	3 46 110 111	4syl	$⊢ φ \to (j \dots N) \neq \emptyset$
113	1	adantr	$⊢ (φ \land i \in (j \dots N)) \to N \in ℕ$
114	89 113	nndivred	$⊢ (φ \land i \in (j \dots N)) \to \frac{E}{N} \in ℝ$
115	89 114	remulcld	$⊢ (φ \land i \in (j \dots N)) \to E (\frac{E}{N}) \in ℝ$
116	7	rpgt0d	$⊢ φ \to 0 < E$
117	116	adantr	$⊢ (φ \land i \in (j \dots N)) \to 0 < E$
118		ltmul2	$⊢ (X (i) (t) \in ℝ \land \frac{E}{N} \in ℝ \land (E \in ℝ \land 0 < E)) \to (X (i) (t) < \frac{E}{N} \leftrightarrow E X (i) (t) < E (\frac{E}{N}))$
119	107 114 89 117 118	syl112anc	$⊢ (φ \land i \in (j \dots N)) \to (X (i) (t) < \frac{E}{N} \leftrightarrow E X (i) (t) < E (\frac{E}{N}))$
120	6 119	mpbid	$⊢ (φ \land i \in (j \dots N)) \to E X (i) (t) < E (\frac{E}{N})$
121	88 112 108 115 120	fsumlt	$⊢ φ \to \sum_{i = j}^{N} E X (i) (t) < \sum_{i = j}^{N} E (\frac{E}{N})$
122	1	nnne0d	$⊢ φ \to N \neq 0$
123	83 63 122	divcld	$⊢ φ \to \frac{E}{N} \in ℂ$
124	83 123	mulcld	$⊢ φ \to E (\frac{E}{N}) \in ℂ$
125		fsumconst	$⊢ ((j \dots N) \in Fin \land E (\frac{E}{N}) \in ℂ) \to \sum_{i = j}^{N} E (\frac{E}{N}) = \|(j \dots N)\| E (\frac{E}{N})$
126	88 124 125	syl2anc	$⊢ φ \to \sum_{i = j}^{N} E (\frac{E}{N}) = \|(j \dots N)\| E (\frac{E}{N})$
127		hashfz	$⊢ N \in ℤ_{\geq j} \to \|(j \dots N)\| = N - j + 1$
128	3 46 127	3syl	$⊢ φ \to \|(j \dots N)\| = N - j + 1$
129	128	oveq1d	$⊢ φ \to \|(j \dots N)\| E (\frac{E}{N}) = (N - j + 1) E (\frac{E}{N})$
130	126 129	eqtrd	$⊢ φ \to \sum_{i = j}^{N} E (\frac{E}{N}) = (N - j + 1) E (\frac{E}{N})$
131	121 130	breqtrd	$⊢ φ \to \sum_{i = j}^{N} E X (i) (t) < (N - j + 1) E (\frac{E}{N})$
132	109 29 57 131	ltadd2dd	$⊢ φ \to \sum_{i = 0}^{j - 1} E X (i) (t) + \sum_{i = j}^{N} E X (i) (t) < \sum_{i = 0}^{j - 1} E X (i) (t) + (N - j + 1) E (\frac{E}{N})$
133	87 132	eqbrtrd	$⊢ φ \to \sum_{i = 0}^{N} E X (i) (t) < \sum_{i = 0}^{j - 1} E X (i) (t) + (N - j + 1) E (\frac{E}{N})$
134	54 5	syldan	$⊢ (φ \land i \in (0 \dots j - 1)) \to X (i) (t) \leq 1$
135		1red	$⊢ (φ \land i \in (0 \dots j - 1)) \to 1 \in ℝ$
136	116	adantr	$⊢ (φ \land i \in (0 \dots j - 1)) \to 0 < E$
137		lemul2	$⊢ (X (i) (t) \in ℝ \land 1 \in ℝ \land (E \in ℝ \land 0 < E)) \to (X (i) (t) \leq 1 \leftrightarrow E X (i) (t) \leq E \cdot 1)$
138	55 135 39 136 137	syl112anc	$⊢ (φ \land i \in (0 \dots j - 1)) \to (X (i) (t) \leq 1 \leftrightarrow E X (i) (t) \leq E \cdot 1)$
139	134 138	mpbid	$⊢ (φ \land i \in (0 \dots j - 1)) \to E X (i) (t) \leq E \cdot 1$
140	83	mulid1d	$⊢ φ \to E \cdot 1 = E$
141	140	adantr	$⊢ (φ \land i \in (0 \dots j - 1)) \to E \cdot 1 = E$
142	139 141	breqtrd	$⊢ (φ \land i \in (0 \dots j - 1)) \to E X (i) (t) \leq E$
143	38 56 39 142	fsumle	$⊢ φ \to \sum_{i = 0}^{j - 1} E X (i) (t) \leq \sum_{i = 0}^{j - 1} E$
144		fsumconst	$⊢ ((0 \dots j - 1) \in Fin \land E \in ℂ) \to \sum_{i = 0}^{j - 1} E = \|(0 \dots j - 1)\| E$
145	38 83 144	syl2anc	$⊢ φ \to \sum_{i = 0}^{j - 1} E = \|(0 \dots j - 1)\| E$
146		0z	$⊢ 0 \in ℤ$
147		1e0p1	$⊢ 1 = 0 + 1$
148	147	fveq2i	$⊢ ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
149	95 148	eleqtrdi	$⊢ φ \to j \in ℤ_{\geq (0 + 1)}$
150		eluzp1m1	$⊢ (0 \in ℤ \land j \in ℤ_{\geq (0 + 1)}) \to j - 1 \in ℤ_{\geq 0}$
151	146 149 150	sylancr	$⊢ φ \to j - 1 \in ℤ_{\geq 0}$
152		hashfz	$⊢ j - 1 \in ℤ_{\geq 0} \to \|(0 \dots j - 1)\| = (j - 1) - 0 + 1$
153	151 152	syl	$⊢ φ \to \|(0 \dots j - 1)\| = (j - 1) - 0 + 1$
154	78 64	subcld	$⊢ φ \to j - 1 \in ℂ$
155	154	subid1d	$⊢ φ \to j - 1 - 0 = j - 1$
156	155	oveq1d	$⊢ φ \to (j - 1) - 0 + 1 = j - 1 + 1$
157	153 156 79	3eqtrd	$⊢ φ \to \|(0 \dots j - 1)\| = j$
158	157	oveq1d	$⊢ φ \to \|(0 \dots j - 1)\| E = j E$
159	78 83	mulcomd	$⊢ φ \to j E = E j$
160	145 158 159	3eqtrd	$⊢ φ \to \sum_{i = 0}^{j - 1} E = E j$
161	143 160	breqtrd	$⊢ φ \to \sum_{i = 0}^{j - 1} E X (i) (t) \leq E j$
162	57 22 29 161	leadd1dd	$⊢ φ \to \sum_{i = 0}^{j - 1} E X (i) (t) + (N - j + 1) E (\frac{E}{N}) \leq E j + (N - j + 1) E (\frac{E}{N})$
163	19 58 30 133 162	ltletrd	$⊢ φ \to \sum_{i = 0}^{N} E X (i) (t) < E j + (N - j + 1) E (\frac{E}{N})$
164	14 14	remulcld	$⊢ φ \to E E \in ℝ$
165	22 164	readdcld	$⊢ φ \to E j + E E \in ℝ$
166	63 78	subcld	$⊢ φ \to N - j \in ℂ$
167	166 64	addcld	$⊢ φ \to N - j + 1 \in ℂ$
168	83 167 123	mul12d	$⊢ φ \to E (N - j + 1) (\frac{E}{N}) = (N - j + 1) E (\frac{E}{N})$
169	168	oveq2d	$⊢ φ \to E j + E (N - j + 1) (\frac{E}{N}) = E j + (N - j + 1) E (\frac{E}{N})$
170	26 27	remulcld	$⊢ φ \to (N - j + 1) (\frac{E}{N}) \in ℝ$
171	14 170	remulcld	$⊢ φ \to E (N - j + 1) (\frac{E}{N}) \in ℝ$
172	167 83 63 122	div12d	$⊢ φ \to (N - j + 1) (\frac{E}{N}) = E (\frac{N - j + 1}{N})$
173	25 21	resubcld	$⊢ φ \to 1 - j \in ℝ$
174		elfzle1	$⊢ j \in (1 \dots N) \to 1 \leq j$
175	3 174	syl	$⊢ φ \to 1 \leq j$
176	25 21	suble0d	$⊢ φ \to (1 - j \leq 0 \leftrightarrow 1 \leq j)$
177	175 176	mpbird	$⊢ φ \to 1 - j \leq 0$
178	173 91 23 177	leadd2dd	$⊢ φ \to N + 1 - j \leq N + 0$
179	63 64 78	addsub12d	$⊢ φ \to N + 1 - j = 1 + N - j$
180	64 166	addcomd	$⊢ φ \to 1 + N - j = N - j + 1$
181	179 180	eqtrd	$⊢ φ \to N + 1 - j = N - j + 1$
182	63	addid1d	$⊢ φ \to N + 0 = N$
183	178 181 182	3brtr3d	$⊢ φ \to N - j + 1 \leq N$
184	1	nngt0d	$⊢ φ \to 0 < N$
185		lediv1	$⊢ (N - j + 1 \in ℝ \land N \in ℝ \land (N \in ℝ \land 0 < N)) \to (N - j + 1 \leq N \leftrightarrow \frac{N - j + 1}{N} \leq \frac{N}{N})$
186	26 23 23 184 185	syl112anc	$⊢ φ \to (N - j + 1 \leq N \leftrightarrow \frac{N - j + 1}{N} \leq \frac{N}{N})$
187	183 186	mpbid	$⊢ φ \to \frac{N - j + 1}{N} \leq \frac{N}{N}$
188	63 122	dividd	$⊢ φ \to \frac{N}{N} = 1$
189	187 188	breqtrd	$⊢ φ \to \frac{N - j + 1}{N} \leq 1$
190	26 1	nndivred	$⊢ φ \to \frac{N - j + 1}{N} \in ℝ$
191	190 25 7	lemul2d	$⊢ φ \to (\frac{N - j + 1}{N} \leq 1 \leftrightarrow E (\frac{N - j + 1}{N}) \leq E \cdot 1)$
192	189 191	mpbid	$⊢ φ \to E (\frac{N - j + 1}{N}) \leq E \cdot 1$
193	192 140	breqtrd	$⊢ φ \to E (\frac{N - j + 1}{N}) \leq E$
194	172 193	eqbrtrd	$⊢ φ \to (N - j + 1) (\frac{E}{N}) \leq E$
195	170 14 7	lemul2d	$⊢ φ \to ((N - j + 1) (\frac{E}{N}) \leq E \leftrightarrow E (N - j + 1) (\frac{E}{N}) \leq E E)$
196	194 195	mpbid	$⊢ φ \to E (N - j + 1) (\frac{E}{N}) \leq E E$
197	171 164 22 196	leadd2dd	$⊢ φ \to E j + E (N - j + 1) (\frac{E}{N}) \leq E j + E E$
198	169 197	eqbrtrrd	$⊢ φ \to E j + (N - j + 1) E (\frac{E}{N}) \leq E j + E E$
199	83 78	mulcomd	$⊢ φ \to E j = j E$
200	199	oveq1d	$⊢ φ \to E j + E E = j E + E E$
201	78 83 83	adddird	$⊢ φ \to (j + E) E = j E + E E$
202	200 201	eqtr4d	$⊢ φ \to E j + E E = (j + E) E$
203	21 14	readdcld	$⊢ φ \to j + E \in ℝ$
204	14 35 21 8	ltadd2dd	$⊢ φ \to j + E < j + (\frac{1}{3})$
205	203 36 7 204	ltmul1dd	$⊢ φ \to (j + E) E < (j + (\frac{1}{3})) E$
206	202 205	eqbrtrd	$⊢ φ \to E j + E E < (j + (\frac{1}{3})) E$
207	30 165 37 198 206	lelttrd	$⊢ φ \to E j + (N - j + 1) E (\frac{E}{N}) < (j + (\frac{1}{3})) E$
208	19 30 37 163 207	lttrd	$⊢ φ \to \sum_{i = 0}^{N} E X (i) (t) < (j + (\frac{1}{3})) E$
209	12 208	eqbrtrd	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E$

Metamath Proof Explorer

Theorem stoweidlem11

Proof