stoweidlem34

Description: This lemma proves that for all t in T there is a j as in the proof of BrosowskiDeutsh p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		stoweidlem34.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem34.2	$⊢ Ⅎ j φ$
3		stoweidlem34.3	$⊢ Ⅎ t φ$
4		stoweidlem34.4	$⊢ D = (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
5		stoweidlem34.5	$⊢ B = (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
6		stoweidlem34.6	$⊢ J = (t \in T ⟼ \{j \in (1 \dots N) \| t \in D (j)\})$
7		stoweidlem34.7	$⊢ φ \to N \in ℕ$
8		stoweidlem34.8	$⊢ φ \to T \in V$
9		stoweidlem34.9	$⊢ φ \to F : T ⟶ ℝ$
10		stoweidlem34.10	$⊢ (φ \land t \in T) \to 0 \leq F (t)$
11		stoweidlem34.11	$⊢ (φ \land t \in T) \to F (t) < (N - 1) E$
12		stoweidlem34.12	$⊢ φ \to E \in ℝ^{+}$
13		stoweidlem34.13	$⊢ φ \to E < \frac{1}{3}$
14		stoweidlem34.14	$⊢ (φ \land j \in (0 \dots N)) \to X (j) : T ⟶ ℝ$
15		stoweidlem34.15	$⊢ (φ \land j \in (0 \dots N) \land t \in T) \to 0 \leq X (j) (t)$
16		stoweidlem34.16	$⊢ (φ \land j \in (0 \dots N) \land t \in T) \to X (j) (t) \leq 1$
17		stoweidlem34.17	$⊢ (φ \land j \in (0 \dots N) \land t \in D (j)) \to X (j) (t) < \frac{E}{N}$
18		stoweidlem34.18	$⊢ (φ \land j \in (0 \dots N) \land t \in B (j)) \to 1 - (\frac{E}{N}) < X (j) (t)$
19		simpr	$⊢ (φ \land t \in T) \to t \in T$
20		ovex	$⊢ (1 \dots N) \in V$
21	20	rabex	$⊢ \{j \in (1 \dots N) \| t \in D (j)\} \in V$
22	6	fvmpt2	$⊢ (t \in T \land \{j \in (1 \dots N) \| t \in D (j)\} \in V) \to J (t) = \{j \in (1 \dots N) \| t \in D (j)\}$
23	19 21 22	sylancl	$⊢ (φ \land t \in T) \to J (t) = \{j \in (1 \dots N) \| t \in D (j)\}$
24		ssrab2	$⊢ \{j \in (1 \dots N) \| t \in D (j)\} \subseteq (1 \dots N)$
25	23 24	eqsstrdi	$⊢ (φ \land t \in T) \to J (t) \subseteq (1 \dots N)$
26		elfznn	$⊢ x \in (1 \dots N) \to x \in ℕ$
27	26	ssriv	$⊢ (1 \dots N) \subseteq ℕ$
28	25 27	sstrdi	$⊢ (φ \land t \in T) \to J (t) \subseteq ℕ$
29		nnssre	$⊢ ℕ \subseteq ℝ$
30	28 29	sstrdi	$⊢ (φ \land t \in T) \to J (t) \subseteq ℝ$
31	7	adantr	$⊢ (φ \land t \in T) \to N \in ℕ$
32		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
33	31 32	eleqtrdi	$⊢ (φ \land t \in T) \to N \in ℤ_{\geq 1}$
34		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
35	33 34	syl	$⊢ (φ \land t \in T) \to N \in (1 \dots N)$
36		3re	$⊢ 3 \in ℝ$
37		3ne0	$⊢ 3 \neq 0$
38	36 37	rereccli	$⊢ \frac{1}{3} \in ℝ$
39	38	a1i	$⊢ (φ \land t \in T) \to \frac{1}{3} \in ℝ$
40		1red	$⊢ (φ \land t \in T) \to 1 \in ℝ$
41	31	nnred	$⊢ (φ \land t \in T) \to N \in ℝ$
42		1lt3	$⊢ 1 < 3$
43	36 42	pm3.2i	$⊢ (3 \in ℝ \land 1 < 3)$
44		recgt1i	$⊢ (3 \in ℝ \land 1 < 3) \to (0 < \frac{1}{3} \land \frac{1}{3} < 1)$
45	44	simprd	$⊢ (3 \in ℝ \land 1 < 3) \to \frac{1}{3} < 1$
46	43 45	mp1i	$⊢ (φ \land t \in T) \to \frac{1}{3} < 1$
47	39 40 41 46	ltsub2dd	$⊢ (φ \land t \in T) \to N - 1 < N - (\frac{1}{3})$
48	41 40	resubcld	$⊢ (φ \land t \in T) \to N - 1 \in ℝ$
49	41 39	resubcld	$⊢ (φ \land t \in T) \to N - (\frac{1}{3}) \in ℝ$
50	12	rpred	$⊢ φ \to E \in ℝ$
51	50	adantr	$⊢ (φ \land t \in T) \to E \in ℝ$
52	12	rpgt0d	$⊢ φ \to 0 < E$
53	52	adantr	$⊢ (φ \land t \in T) \to 0 < E$
54		ltmul1	$⊢ (N - 1 \in ℝ \land N - (\frac{1}{3}) \in ℝ \land (E \in ℝ \land 0 < E)) \to (N - 1 < N - (\frac{1}{3}) \leftrightarrow (N - 1) E < (N - (\frac{1}{3})) E)$
55	48 49 51 53 54	syl112anc	$⊢ (φ \land t \in T) \to (N - 1 < N - (\frac{1}{3}) \leftrightarrow (N - 1) E < (N - (\frac{1}{3})) E)$
56	47 55	mpbid	$⊢ (φ \land t \in T) \to (N - 1) E < (N - (\frac{1}{3})) E$
57	11 56	jca	$⊢ (φ \land t \in T) \to (F (t) < (N - 1) E \land (N - 1) E < (N - (\frac{1}{3})) E)$
58	9	ffvelrnda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
59	48 51	remulcld	$⊢ (φ \land t \in T) \to (N - 1) E \in ℝ$
60	49 51	remulcld	$⊢ (φ \land t \in T) \to (N - (\frac{1}{3})) E \in ℝ$
61		lttr	$⊢ (F (t) \in ℝ \land (N - 1) E \in ℝ \land (N - (\frac{1}{3})) E \in ℝ) \to ((F (t) < (N - 1) E \land (N - 1) E < (N - (\frac{1}{3})) E) \to F (t) < (N - (\frac{1}{3})) E)$
62		ltle	$⊢ (F (t) \in ℝ \land (N - (\frac{1}{3})) E \in ℝ) \to (F (t) < (N - (\frac{1}{3})) E \to F (t) \leq (N - (\frac{1}{3})) E)$
63	62	3adant2	$⊢ (F (t) \in ℝ \land (N - 1) E \in ℝ \land (N - (\frac{1}{3})) E \in ℝ) \to (F (t) < (N - (\frac{1}{3})) E \to F (t) \leq (N - (\frac{1}{3})) E)$
64	61 63	syld	$⊢ (F (t) \in ℝ \land (N - 1) E \in ℝ \land (N - (\frac{1}{3})) E \in ℝ) \to ((F (t) < (N - 1) E \land (N - 1) E < (N - (\frac{1}{3})) E) \to F (t) \leq (N - (\frac{1}{3})) E)$
65	58 59 60 64	syl3anc	$⊢ (φ \land t \in T) \to ((F (t) < (N - 1) E \land (N - 1) E < (N - (\frac{1}{3})) E) \to F (t) \leq (N - (\frac{1}{3})) E)$
66	57 65	mpd	$⊢ (φ \land t \in T) \to F (t) \leq (N - (\frac{1}{3})) E$
67		rabid	$⊢ t \in \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\} \leftrightarrow (t \in T \land F (t) \leq (N - (\frac{1}{3})) E)$
68	19 66 67	sylanbrc	$⊢ (φ \land t \in T) \to t \in \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\}$
69		oveq1	$⊢ j = N \to j - (\frac{1}{3}) = N - (\frac{1}{3})$
70	69	oveq1d	$⊢ j = N \to (j - (\frac{1}{3})) E = (N - (\frac{1}{3})) E$
71	70	breq2d	$⊢ j = N \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (N - (\frac{1}{3})) E)$
72	71	rabbidv	$⊢ j = N \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\}$
73		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
74		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
75	73 74	eleqtrdi	$⊢ N \in ℕ \to N \in ℤ_{\geq 0}$
76		eluzfz2	$⊢ N \in ℤ_{\geq 0} \to N \in (0 \dots N)$
77	7 75 76	3syl	$⊢ φ \to N \in (0 \dots N)$
78		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\} \in V$
79	8 78	syl	$⊢ φ \to \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\} \in V$
80	4 72 77 79	fvmptd3	$⊢ φ \to D (N) = \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\}$
81	80	adantr	$⊢ (φ \land t \in T) \to D (N) = \{t \in T \| F (t) \leq (N - (\frac{1}{3})) E\}$
82	68 81	eleqtrrd	$⊢ (φ \land t \in T) \to t \in D (N)$
83		nfcv	$⊢ \underline{Ⅎ} j N$
84		nfcv	$⊢ \underline{Ⅎ} j (1 \dots N)$
85		nfmpt1	$⊢ \underline{Ⅎ} j (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
86	4 85	nfcxfr	$⊢ \underline{Ⅎ} j D$
87	86 83	nffv	$⊢ \underline{Ⅎ} j D (N)$
88	87	nfcri	$⊢ Ⅎ j t \in D (N)$
89		fveq2	$⊢ j = N \to D (j) = D (N)$
90	89	eleq2d	$⊢ j = N \to (t \in D (j) \leftrightarrow t \in D (N))$
91	83 84 88 90	elrabf	$⊢ N \in \{j \in (1 \dots N) \| t \in D (j)\} \leftrightarrow (N \in (1 \dots N) \land t \in D (N))$
92	35 82 91	sylanbrc	$⊢ (φ \land t \in T) \to N \in \{j \in (1 \dots N) \| t \in D (j)\}$
93	92 23	eleqtrrd	$⊢ (φ \land t \in T) \to N \in J (t)$
94		ne0i	$⊢ N \in J (t) \to J (t) \neq \emptyset$
95	93 94	syl	$⊢ (φ \land t \in T) \to J (t) \neq \emptyset$
96		nnwo	$⊢ (J (t) \subseteq ℕ \land J (t) \neq \emptyset) \to \exists i \in J (t) \forall k \in J (t) i \leq k$
97		nfcv	$⊢ \underline{Ⅎ} i J (t)$
98		nfcv	$⊢ \underline{Ⅎ} j T$
99		nfrab1	$⊢ \underline{Ⅎ} j \{j \in (1 \dots N) \| t \in D (j)\}$
100	98 99	nfmpt	$⊢ \underline{Ⅎ} j (t \in T ⟼ \{j \in (1 \dots N) \| t \in D (j)\})$
101	6 100	nfcxfr	$⊢ \underline{Ⅎ} j J$
102		nfcv	$⊢ \underline{Ⅎ} j t$
103	101 102	nffv	$⊢ \underline{Ⅎ} j J (t)$
104		nfv	$⊢ Ⅎ j i \leq k$
105	103 104	nfralw	$⊢ Ⅎ j \forall k \in J (t) i \leq k$
106		nfv	$⊢ Ⅎ i \forall k \in J (t) j \leq k$
107		breq1	$⊢ i = j \to (i \leq k \leftrightarrow j \leq k)$
108	107	ralbidv	$⊢ i = j \to (\forall k \in J (t) i \leq k \leftrightarrow \forall k \in J (t) j \leq k)$
109	97 103 105 106 108	cbvrexfw	$⊢ \exists i \in J (t) \forall k \in J (t) i \leq k \leftrightarrow \exists j \in J (t) \forall k \in J (t) j \leq k$
110	96 109	sylib	$⊢ (J (t) \subseteq ℕ \land J (t) \neq \emptyset) \to \exists j \in J (t) \forall k \in J (t) j \leq k$
111	28 95 110	syl2anc	$⊢ (φ \land t \in T) \to \exists j \in J (t) \forall k \in J (t) j \leq k$
112		nfv	$⊢ Ⅎ j t \in T$
113	2 112	nfan	$⊢ Ⅎ j (φ \land t \in T)$
114	23	eleq2d	$⊢ (φ \land t \in T) \to (j \in J (t) \leftrightarrow j \in \{j \in (1 \dots N) \| t \in D (j)\})$
115	114	biimpa	$⊢ ((φ \land t \in T) \land j \in J (t)) \to j \in \{j \in (1 \dots N) \| t \in D (j)\}$
116		rabid	$⊢ j \in \{j \in (1 \dots N) \| t \in D (j)\} \leftrightarrow (j \in (1 \dots N) \land t \in D (j))$
117	115 116	sylib	$⊢ ((φ \land t \in T) \land j \in J (t)) \to (j \in (1 \dots N) \land t \in D (j))$
118	117	simprd	$⊢ ((φ \land t \in T) \land j \in J (t)) \to t \in D (j)$
119	118	adantr	$⊢ (((φ \land t \in T) \land j \in J (t)) \land \forall k \in J (t) j \leq k) \to t \in D (j)$
120		simp3	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to t \in D (j - 1)$
121		simp1l	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to φ$
122		noel	$⊢ \neg t \in \emptyset$
123		oveq1	$⊢ j = 1 \to j - 1 = 1 - 1$
124		1m1e0	$⊢ 1 - 1 = 0$
125	123 124	eqtrdi	$⊢ j = 1 \to j - 1 = 0$
126	125	fveq2d	$⊢ j = 1 \to D (j - 1) = D (0)$
127	36	a1i	$⊢ (φ \land t \in T) \to 3 \in ℝ$
128	37	a1i	$⊢ (φ \land t \in T) \to 3 \neq 0$
129	40 127 128	redivcld	$⊢ (φ \land t \in T) \to \frac{1}{3} \in ℝ$
130	129	renegcld	$⊢ (φ \land t \in T) \to - \frac{1}{3} \in ℝ$
131	130 51	remulcld	$⊢ (φ \land t \in T) \to (- \frac{1}{3}) E \in ℝ$
132		0red	$⊢ (φ \land t \in T) \to 0 \in ℝ$
133		3pos	$⊢ 0 < 3$
134	36 133	recgt0ii	$⊢ 0 < \frac{1}{3}$
135		lt0neg2	$⊢ \frac{1}{3} \in ℝ \to (0 < \frac{1}{3} \leftrightarrow - \frac{1}{3} < 0)$
136	38 135	ax-mp	$⊢ 0 < \frac{1}{3} \leftrightarrow - \frac{1}{3} < 0$
137	134 136	mpbi	$⊢ - \frac{1}{3} < 0$
138		ltmul1	$⊢ (- \frac{1}{3} \in ℝ \land 0 \in ℝ \land (E \in ℝ \land 0 < E)) \to (- \frac{1}{3} < 0 \leftrightarrow (- \frac{1}{3}) E < 0 \cdot E)$
139	130 132 51 53 138	syl112anc	$⊢ (φ \land t \in T) \to (- \frac{1}{3} < 0 \leftrightarrow (- \frac{1}{3}) E < 0 \cdot E)$
140	137 139	mpbii	$⊢ (φ \land t \in T) \to (- \frac{1}{3}) E < 0 \cdot E$
141		mul02lem2	$⊢ E \in ℝ \to 0 \cdot E = 0$
142	51 141	syl	$⊢ (φ \land t \in T) \to 0 \cdot E = 0$
143	140 142	breqtrd	$⊢ (φ \land t \in T) \to (- \frac{1}{3}) E < 0$
144	131 132 58 143 10	ltletrd	$⊢ (φ \land t \in T) \to (- \frac{1}{3}) E < F (t)$
145	131 58	ltnled	$⊢ (φ \land t \in T) \to ((- \frac{1}{3}) E < F (t) \leftrightarrow \neg F (t) \leq (- \frac{1}{3}) E)$
146	144 145	mpbid	$⊢ (φ \land t \in T) \to \neg F (t) \leq (- \frac{1}{3}) E$
147		nan	$⊢ (φ \to \neg (t \in T \land F (t) \leq (- \frac{1}{3}) E)) \leftrightarrow ((φ \land t \in T) \to \neg F (t) \leq (- \frac{1}{3}) E)$
148	146 147	mpbir	$⊢ φ \to \neg (t \in T \land F (t) \leq (- \frac{1}{3}) E)$
149		rabid	$⊢ t \in \{t \in T \| F (t) \leq (- \frac{1}{3}) E\} \leftrightarrow (t \in T \land F (t) \leq (- \frac{1}{3}) E)$
150	148 149	sylnibr	$⊢ φ \to \neg t \in \{t \in T \| F (t) \leq (- \frac{1}{3}) E\}$
151		oveq1	$⊢ j = 0 \to j - (\frac{1}{3}) = 0 - (\frac{1}{3})$
152		df-neg	$⊢ - \frac{1}{3} = 0 - (\frac{1}{3})$
153	151 152	eqtr4di	$⊢ j = 0 \to j - (\frac{1}{3}) = - \frac{1}{3}$
154	153	oveq1d	$⊢ j = 0 \to (j - (\frac{1}{3})) E = (- \frac{1}{3}) E$
155	154	breq2d	$⊢ j = 0 \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (- \frac{1}{3}) E)$
156	155	rabbidv	$⊢ j = 0 \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (- \frac{1}{3}) E\}$
157	7	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
158		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
159	157 158	sylib	$⊢ φ \to N \in ℤ_{\geq 0}$
160		eluzfz1	$⊢ N \in ℤ_{\geq 0} \to 0 \in (0 \dots N)$
161	159 160	syl	$⊢ φ \to 0 \in (0 \dots N)$
162		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (- \frac{1}{3}) E\} \in V$
163	8 162	syl	$⊢ φ \to \{t \in T \| F (t) \leq (- \frac{1}{3}) E\} \in V$
164	4 156 161 163	fvmptd3	$⊢ φ \to D (0) = \{t \in T \| F (t) \leq (- \frac{1}{3}) E\}$
165	150 164	neleqtrrd	$⊢ φ \to \neg t \in D (0)$
166	3 165	alrimi	$⊢ φ \to \forall t \neg t \in D (0)$
167		nfcv	$⊢ \underline{Ⅎ} t (0 \dots N)$
168		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
169	167 168	nfmpt	$⊢ \underline{Ⅎ} t (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
170	4 169	nfcxfr	$⊢ \underline{Ⅎ} t D$
171		nfcv	$⊢ \underline{Ⅎ} t 0$
172	170 171	nffv	$⊢ \underline{Ⅎ} t D (0)$
173	172	eq0f	$⊢ D (0) = \emptyset \leftrightarrow \forall t \neg t \in D (0)$
174	166 173	sylibr	$⊢ φ \to D (0) = \emptyset$
175	126 174	sylan9eqr	$⊢ (φ \land j = 1) \to D (j - 1) = \emptyset$
176	175	eleq2d	$⊢ (φ \land j = 1) \to (t \in D (j - 1) \leftrightarrow t \in \emptyset)$
177	122 176	mtbiri	$⊢ (φ \land j = 1) \to \neg t \in D (j - 1)$
178	177	ex	$⊢ φ \to (j = 1 \to \neg t \in D (j - 1))$
179	178	con2d	$⊢ φ \to (t \in D (j - 1) \to \neg j = 1)$
180	121 120 179	sylc	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to \neg j = 1$
181		simplll	$⊢ (((φ \land t \in T) \land j \in J (t)) \land \neg j = 1) \to φ$
182	114 116	syl6bb	$⊢ (φ \land t \in T) \to (j \in J (t) \leftrightarrow (j \in (1 \dots N) \land t \in D (j)))$
183	182	simprbda	$⊢ ((φ \land t \in T) \land j \in J (t)) \to j \in (1 \dots N)$
184	7 32	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
185	184	adantr	$⊢ (φ \land j \in J (t)) \to N \in ℤ_{\geq 1}$
186		elfzp12	$⊢ N \in ℤ_{\geq 1} \to (j \in (1 \dots N) \leftrightarrow (j = 1 \lor j \in (1 + 1 \dots N)))$
187	185 186	syl	$⊢ (φ \land j \in J (t)) \to (j \in (1 \dots N) \leftrightarrow (j = 1 \lor j \in (1 + 1 \dots N)))$
188	187	adantlr	$⊢ ((φ \land t \in T) \land j \in J (t)) \to (j \in (1 \dots N) \leftrightarrow (j = 1 \lor j \in (1 + 1 \dots N)))$
189	183 188	mpbid	$⊢ ((φ \land t \in T) \land j \in J (t)) \to (j = 1 \lor j \in (1 + 1 \dots N))$
190	189	orcanai	$⊢ (((φ \land t \in T) \land j \in J (t)) \land \neg j = 1) \to j \in (1 + 1 \dots N)$
191		fzssp1	$⊢ (1 \dots N - 1) \subseteq (1 \dots N - 1 + 1)$
192	7	nncnd	$⊢ φ \to N \in ℂ$
193		1cnd	$⊢ φ \to 1 \in ℂ$
194	192 193	npcand	$⊢ φ \to N - 1 + 1 = N$
195	194	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
196	191 195	sseqtrid	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
197	196	adantr	$⊢ (φ \land j \in (1 + 1 \dots N)) \to (1 \dots N - 1) \subseteq (1 \dots N)$
198		simpr	$⊢ (φ \land j \in (1 + 1 \dots N)) \to j \in (1 + 1 \dots N)$
199		1z	$⊢ 1 \in ℤ$
200		zaddcl	$⊢ (1 \in ℤ \land 1 \in ℤ) \to 1 + 1 \in ℤ$
201	199 199 200	mp2an	$⊢ 1 + 1 \in ℤ$
202	201	a1i	$⊢ (φ \land j \in (1 + 1 \dots N)) \to 1 + 1 \in ℤ$
203	7	nnzd	$⊢ φ \to N \in ℤ$
204	203	adantr	$⊢ (φ \land j \in (1 + 1 \dots N)) \to N \in ℤ$
205		elfzelz	$⊢ j \in (1 + 1 \dots N) \to j \in ℤ$
206	205	adantl	$⊢ (φ \land j \in (1 + 1 \dots N)) \to j \in ℤ$
207		1zzd	$⊢ (φ \land j \in (1 + 1 \dots N)) \to 1 \in ℤ$
208		fzsubel	$⊢ ((1 + 1 \in ℤ \land N \in ℤ) \land (j \in ℤ \land 1 \in ℤ)) \to (j \in (1 + 1 \dots N) \leftrightarrow j - 1 \in (1 + 1 - 1 \dots N - 1))$
209	202 204 206 207 208	syl22anc	$⊢ (φ \land j \in (1 + 1 \dots N)) \to (j \in (1 + 1 \dots N) \leftrightarrow j - 1 \in (1 + 1 - 1 \dots N - 1))$
210	198 209	mpbid	$⊢ (φ \land j \in (1 + 1 \dots N)) \to j - 1 \in (1 + 1 - 1 \dots N - 1)$
211		ax-1cn	$⊢ 1 \in ℂ$
212	211 211	pncan3oi	$⊢ 1 + 1 - 1 = 1$
213	212	oveq1i	$⊢ (1 + 1 - 1 \dots N - 1) = (1 \dots N - 1)$
214	210 213	eleqtrdi	$⊢ (φ \land j \in (1 + 1 \dots N)) \to j - 1 \in (1 \dots N - 1)$
215	197 214	sseldd	$⊢ (φ \land j \in (1 + 1 \dots N)) \to j - 1 \in (1 \dots N)$
216	181 190 215	syl2anc	$⊢ (((φ \land t \in T) \land j \in J (t)) \land \neg j = 1) \to j - 1 \in (1 \dots N)$
217	216	ex	$⊢ ((φ \land t \in T) \land j \in J (t)) \to (\neg j = 1 \to j - 1 \in (1 \dots N))$
218	217	3adant3	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to (\neg j = 1 \to j - 1 \in (1 \dots N))$
219	180 218	mpd	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to j - 1 \in (1 \dots N)$
220		fveq2	$⊢ i = j - 1 \to D (i) = D (j - 1)$
221	220	eleq2d	$⊢ i = j - 1 \to (t \in D (i) \leftrightarrow t \in D (j - 1))$
222	221	elrab3	$⊢ j - 1 \in (1 \dots N) \to (j - 1 \in \{i \in (1 \dots N) \| t \in D (i)\} \leftrightarrow t \in D (j - 1))$
223	219 222	syl	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to (j - 1 \in \{i \in (1 \dots N) \| t \in D (i)\} \leftrightarrow t \in D (j - 1))$
224	120 223	mpbird	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to j - 1 \in \{i \in (1 \dots N) \| t \in D (i)\}$
225		nfcv	$⊢ \underline{Ⅎ} i (1 \dots N)$
226		nfv	$⊢ Ⅎ i t \in D (j)$
227		nfcv	$⊢ \underline{Ⅎ} j i$
228	86 227	nffv	$⊢ \underline{Ⅎ} j D (i)$
229	228	nfcri	$⊢ Ⅎ j t \in D (i)$
230		fveq2	$⊢ j = i \to D (j) = D (i)$
231	230	eleq2d	$⊢ j = i \to (t \in D (j) \leftrightarrow t \in D (i))$
232	84 225 226 229 231	cbvrabw	$⊢ \{j \in (1 \dots N) \| t \in D (j)\} = \{i \in (1 \dots N) \| t \in D (i)\}$
233	224 232	eleqtrrdi	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to j - 1 \in \{j \in (1 \dots N) \| t \in D (j)\}$
234	23	3ad2ant1	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to J (t) = \{j \in (1 \dots N) \| t \in D (j)\}$
235	233 234	eleqtrrd	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to j - 1 \in J (t)$
236		elfzelz	$⊢ j \in (1 \dots N) \to j \in ℤ$
237		zre	$⊢ j \in ℤ \to j \in ℝ$
238	183 236 237	3syl	$⊢ ((φ \land t \in T) \land j \in J (t)) \to j \in ℝ$
239	238	3adant3	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to j \in ℝ$
240		peano2rem	$⊢ j \in ℝ \to j - 1 \in ℝ$
241		ltm1	$⊢ j \in ℝ \to j - 1 < j$
242	241	adantr	$⊢ (j \in ℝ \land j - 1 \in ℝ) \to j - 1 < j$
243		ltnle	$⊢ (j - 1 \in ℝ \land j \in ℝ) \to (j - 1 < j \leftrightarrow \neg j \leq j - 1)$
244	243	ancoms	$⊢ (j \in ℝ \land j - 1 \in ℝ) \to (j - 1 < j \leftrightarrow \neg j \leq j - 1)$
245	242 244	mpbid	$⊢ (j \in ℝ \land j - 1 \in ℝ) \to \neg j \leq j - 1$
246	239 240 245	syl2anc2	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to \neg j \leq j - 1$
247		breq2	$⊢ k = j - 1 \to (j \leq k \leftrightarrow j \leq j - 1)$
248	247	notbid	$⊢ k = j - 1 \to (\neg j \leq k \leftrightarrow \neg j \leq j - 1)$
249	248	rspcev	$⊢ (j - 1 \in J (t) \land \neg j \leq j - 1) \to \exists k \in J (t) \neg j \leq k$
250	235 246 249	syl2anc	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to \exists k \in J (t) \neg j \leq k$
251		rexnal	$⊢ \exists k \in J (t) \neg j \leq k \leftrightarrow \neg \forall k \in J (t) j \leq k$
252	250 251	sylib	$⊢ ((φ \land t \in T) \land j \in J (t) \land t \in D (j - 1)) \to \neg \forall k \in J (t) j \leq k$
253	252	3expia	$⊢ ((φ \land t \in T) \land j \in J (t)) \to (t \in D (j - 1) \to \neg \forall k \in J (t) j \leq k)$
254	253	con2d	$⊢ ((φ \land t \in T) \land j \in J (t)) \to (\forall k \in J (t) j \leq k \to \neg t \in D (j - 1))$
255	254	imp	$⊢ (((φ \land t \in T) \land j \in J (t)) \land \forall k \in J (t) j \leq k) \to \neg t \in D (j - 1)$
256	119 255	eldifd	$⊢ (((φ \land t \in T) \land j \in J (t)) \land \forall k \in J (t) j \leq k) \to t \in (D (j) ∖ D (j - 1))$
257	256	exp31	$⊢ (φ \land t \in T) \to (j \in J (t) \to (\forall k \in J (t) j \leq k \to t \in (D (j) ∖ D (j - 1))))$
258	113 257	reximdai	$⊢ (φ \land t \in T) \to (\exists j \in J (t) \forall k \in J (t) j \leq k \to \exists j \in J (t) t \in (D (j) ∖ D (j - 1)))$
259	111 258	mpd	$⊢ (φ \land t \in T) \to \exists j \in J (t) t \in (D (j) ∖ D (j - 1))$
260		df-rex	$⊢ \exists j \in J (t) t \in (D (j) ∖ D (j - 1)) \leftrightarrow \exists j (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))$
261	259 260	sylib	$⊢ (φ \land t \in T) \to \exists j (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))$
262		simprl	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to j \in J (t)$
263		eldifn	$⊢ t \in (D (j) ∖ D (j - 1)) \to \neg t \in D (j - 1)$
264		simplr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to t \in T$
265		simpll	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to φ$
266	183	adantrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to j \in (1 \dots N)$
267		simprr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to \neg t \in D (j - 1)$
268		oveq1	$⊢ j = k \to j - (\frac{1}{3}) = k - (\frac{1}{3})$
269	268	oveq1d	$⊢ j = k \to (j - (\frac{1}{3})) E = (k - (\frac{1}{3})) E$
270	269	breq2d	$⊢ j = k \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (k - (\frac{1}{3})) E)$
271	270	rabbidv	$⊢ j = k \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (k - (\frac{1}{3})) E\}$
272	271	cbvmptv	$⊢ (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}) = (k \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (k - (\frac{1}{3})) E\})$
273	4 272	eqtri	$⊢ D = (k \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (k - (\frac{1}{3})) E\})$
274		oveq1	$⊢ k = j - 1 \to k - (\frac{1}{3}) = j - 1 - (\frac{1}{3})$
275	274	oveq1d	$⊢ k = j - 1 \to (k - (\frac{1}{3})) E = (j - 1 - (\frac{1}{3})) E$
276	275	breq2d	$⊢ k = j - 1 \to (F (t) \leq (k - (\frac{1}{3})) E \leftrightarrow F (t) \leq (j - 1 - (\frac{1}{3})) E)$
277	276	rabbidv	$⊢ k = j - 1 \to \{t \in T \| F (t) \leq (k - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\}$
278		fzssp1	$⊢ (0 \dots N - 1) \subseteq (0 \dots N - 1 + 1)$
279	194	oveq2d	$⊢ φ \to (0 \dots N - 1 + 1) = (0 \dots N)$
280	278 279	sseqtrid	$⊢ φ \to (0 \dots N - 1) \subseteq (0 \dots N)$
281	280	adantr	$⊢ (φ \land j \in (1 \dots N)) \to (0 \dots N - 1) \subseteq (0 \dots N)$
282		simpr	$⊢ (φ \land j \in (1 \dots N)) \to j \in (1 \dots N)$
283		1zzd	$⊢ (φ \land j \in (1 \dots N)) \to 1 \in ℤ$
284	203	adantr	$⊢ (φ \land j \in (1 \dots N)) \to N \in ℤ$
285	236	adantl	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℤ$
286		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))$
287	283 284 285 283 286	syl22anc	$⊢ (φ \land j \in (1 \dots N)) \to (j \in (1 \dots N) \leftrightarrow j - 1 \in (1 - 1 \dots N - 1))$
288	282 287	mpbid	$⊢ (φ \land j \in (1 \dots N)) \to j - 1 \in (1 - 1 \dots N - 1)$
289	124	a1i	$⊢ (φ \land j \in (1 \dots N)) \to 1 - 1 = 0$
290	289	oveq1d	$⊢ (φ \land j \in (1 \dots N)) \to (1 - 1 \dots N - 1) = (0 \dots N - 1)$
291	288 290	eleqtrd	$⊢ (φ \land j \in (1 \dots N)) \to j - 1 \in (0 \dots N - 1)$
292	281 291	sseldd	$⊢ (φ \land j \in (1 \dots N)) \to j - 1 \in (0 \dots N)$
293	8	adantr	$⊢ (φ \land j \in (1 \dots N)) \to T \in V$
294		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\} \in V$
295	293 294	syl	$⊢ (φ \land j \in (1 \dots N)) \to \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\} \in V$
296	273 277 292 295	fvmptd3	$⊢ (φ \land j \in (1 \dots N)) \to D (j - 1) = \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\}$
297	296	eleq2d	$⊢ (φ \land j \in (1 \dots N)) \to (t \in D (j - 1) \leftrightarrow t \in \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\})$
298	297	notbid	$⊢ (φ \land j \in (1 \dots N)) \to (\neg t \in D (j - 1) \leftrightarrow \neg t \in \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\})$
299	298	biimpa	$⊢ ((φ \land j \in (1 \dots N)) \land \neg t \in D (j - 1)) \to \neg t \in \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\}$
300	265 266 267 299	syl21anc	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to \neg t \in \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\}$
301		rabid	$⊢ t \in \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\} \leftrightarrow (t \in T \land F (t) \leq (j - 1 - (\frac{1}{3})) E)$
302	238	adantrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to j \in ℝ$
303		recn	$⊢ j \in ℝ \to j \in ℂ$
304		1cnd	$⊢ j \in ℝ \to 1 \in ℂ$
305		1re	$⊢ 1 \in ℝ$
306	305 36 37	3pm3.2i	$⊢ (1 \in ℝ \land 3 \in ℝ \land 3 \neq 0)$
307		redivcl	$⊢ (1 \in ℝ \land 3 \in ℝ \land 3 \neq 0) \to \frac{1}{3} \in ℝ$
308		recn	$⊢ \frac{1}{3} \in ℝ \to \frac{1}{3} \in ℂ$
309	306 307 308	mp2b	$⊢ \frac{1}{3} \in ℂ$
310	309	a1i	$⊢ j \in ℝ \to \frac{1}{3} \in ℂ$
311	303 304 310	subsub4d	$⊢ j \in ℝ \to j - 1 - (\frac{1}{3}) = j - (1 + (\frac{1}{3}))$
312		3cn	$⊢ 3 \in ℂ$
313	312 211 312 37	divdiri	$⊢ \frac{3 + 1}{3} = (\frac{3}{3}) + (\frac{1}{3})$
314		3p1e4	$⊢ 3 + 1 = 4$
315	314	oveq1i	$⊢ \frac{3 + 1}{3} = \frac{4}{3}$
316	312 37	dividi	$⊢ \frac{3}{3} = 1$
317	316	oveq1i	$⊢ (\frac{3}{3}) + (\frac{1}{3}) = 1 + (\frac{1}{3})$
318	313 315 317	3eqtr3i	$⊢ \frac{4}{3} = 1 + (\frac{1}{3})$
319	318	a1i	$⊢ j \in ℝ \to \frac{4}{3} = 1 + (\frac{1}{3})$
320	319	oveq2d	$⊢ j \in ℝ \to j - (\frac{4}{3}) = j - (1 + (\frac{1}{3}))$
321	311 320	eqtr4d	$⊢ j \in ℝ \to j - 1 - (\frac{1}{3}) = j - (\frac{4}{3})$
322	321	oveq1d	$⊢ j \in ℝ \to (j - 1 - (\frac{1}{3})) E = (j - (\frac{4}{3})) E$
323	302 322	syl	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to (j - 1 - (\frac{1}{3})) E = (j - (\frac{4}{3})) E$
324	323	breq2d	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to (F (t) \leq (j - 1 - (\frac{1}{3})) E \leftrightarrow F (t) \leq (j - (\frac{4}{3})) E)$
325	324	anbi2d	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to ((t \in T \land F (t) \leq (j - 1 - (\frac{1}{3})) E) \leftrightarrow (t \in T \land F (t) \leq (j - (\frac{4}{3})) E))$
326	301 325	syl5bb	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to (t \in \{t \in T \| F (t) \leq (j - 1 - (\frac{1}{3})) E\} \leftrightarrow (t \in T \land F (t) \leq (j - (\frac{4}{3})) E))$
327	300 326	mtbid	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to \neg (t \in T \land F (t) \leq (j - (\frac{4}{3})) E)$
328		imnan	$⊢ (t \in T \to \neg F (t) \leq (j - (\frac{4}{3})) E) \leftrightarrow \neg (t \in T \land F (t) \leq (j - (\frac{4}{3})) E)$
329	327 328	sylibr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to (t \in T \to \neg F (t) \leq (j - (\frac{4}{3})) E)$
330	264 329	mpd	$⊢ ((φ \land t \in T) \land (j \in J (t) \land \neg t \in D (j - 1))) \to \neg F (t) \leq (j - (\frac{4}{3})) E$
331	263 330	sylanr2	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to \neg F (t) \leq (j - (\frac{4}{3})) E$
332	238	adantrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to j \in ℝ$
333		4re	$⊢ 4 \in ℝ$
334	333	a1i	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to 4 \in ℝ$
335	36	a1i	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to 3 \in ℝ$
336	37	a1i	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to 3 \neq 0$
337	334 335 336	redivcld	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to \frac{4}{3} \in ℝ$
338	332 337	resubcld	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to j - (\frac{4}{3}) \in ℝ$
339	50	ad2antrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to E \in ℝ$
340		remulcl	$⊢ (j - (\frac{4}{3}) \in ℝ \land E \in ℝ) \to (j - (\frac{4}{3})) E \in ℝ$
341	340	rexrd	$⊢ (j - (\frac{4}{3}) \in ℝ \land E \in ℝ) \to (j - (\frac{4}{3})) E \in ℝ^{*}$
342	338 339 341	syl2anc	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j - (\frac{4}{3})) E \in ℝ^{*}$
343	58	rexrd	$⊢ (φ \land t \in T) \to F (t) \in ℝ^{*}$
344	343	adantr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to F (t) \in ℝ^{*}$
345		xrltnle	$⊢ ((j - (\frac{4}{3})) E \in ℝ^{} \land F (t) \in ℝ^{}) \to ((j - (\frac{4}{3})) E < F (t) \leftrightarrow \neg F (t) \leq (j - (\frac{4}{3})) E)$
346	342 344 345	syl2anc	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to ((j - (\frac{4}{3})) E < F (t) \leftrightarrow \neg F (t) \leq (j - (\frac{4}{3})) E)$
347	331 346	mpbird	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j - (\frac{4}{3})) E < F (t)$
348		simpl	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (φ \land t \in T)$
349		simprr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to t \in (D (j) ∖ D (j - 1))$
350	349	eldifad	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to t \in D (j)$
351		simplll	$⊢ (((φ \land t \in T) \land j \in J (t)) \land t \in D (j)) \to φ$
352	183	adantr	$⊢ (((φ \land t \in T) \land j \in J (t)) \land t \in D (j)) \to j \in (1 \dots N)$
353		simpr	$⊢ (((φ \land t \in T) \land j \in J (t)) \land t \in D (j)) \to t \in D (j)$
354		oveq1	$⊢ k = j \to k - (\frac{1}{3}) = j - (\frac{1}{3})$
355	354	oveq1d	$⊢ k = j \to (k - (\frac{1}{3})) E = (j - (\frac{1}{3})) E$
356	355	breq2d	$⊢ k = j \to (F (t) \leq (k - (\frac{1}{3})) E \leftrightarrow F (t) \leq (j - (\frac{1}{3})) E)$
357	356	rabbidv	$⊢ k = j \to \{t \in T \| F (t) \leq (k - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
358		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
359	358	sseli	$⊢ j \in (1 \dots N) \to j \in (0 \dots N)$
360	359	adantl	$⊢ (φ \land j \in (1 \dots N)) \to j \in (0 \dots N)$
361		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \in V$
362	293 361	syl	$⊢ (φ \land j \in (1 \dots N)) \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \in V$
363	273 357 360 362	fvmptd3	$⊢ (φ \land j \in (1 \dots N)) \to D (j) = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
364	363	eleq2d	$⊢ (φ \land j \in (1 \dots N)) \to (t \in D (j) \leftrightarrow t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
365	364	biimpa	$⊢ ((φ \land j \in (1 \dots N)) \land t \in D (j)) \to t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
366	351 352 353 365	syl21anc	$⊢ (((φ \land t \in T) \land j \in J (t)) \land t \in D (j)) \to t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
367		rabid	$⊢ t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \leftrightarrow (t \in T \land F (t) \leq (j - (\frac{1}{3})) E)$
368	366 367	sylib	$⊢ (((φ \land t \in T) \land j \in J (t)) \land t \in D (j)) \to (t \in T \land F (t) \leq (j - (\frac{1}{3})) E)$
369	368	simprd	$⊢ (((φ \land t \in T) \land j \in J (t)) \land t \in D (j)) \to F (t) \leq (j - (\frac{1}{3})) E$
370	348 262 350 369	syl21anc	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to F (t) \leq (j - (\frac{1}{3})) E$
371	347 370	jca	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E)$
372	7	ad2antrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to N \in ℕ$
373		simplr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to t \in T$
374	183	adantrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to j \in (1 \dots N)$
375		nfv	$⊢ Ⅎ j i \in (0 \dots N)$
376	2 375	nfan	$⊢ Ⅎ j (φ \land i \in (0 \dots N))$
377		nfv	$⊢ Ⅎ j X (i) : T ⟶ ℝ$
378	376 377	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ)$
379		eleq1w	$⊢ j = i \to (j \in (0 \dots N) \leftrightarrow i \in (0 \dots N))$
380	379	anbi2d	$⊢ j = i \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land i \in (0 \dots N)))$
381		fveq2	$⊢ j = i \to X (j) = X (i)$
382	381	feq1d	$⊢ j = i \to (X (j) : T ⟶ ℝ \leftrightarrow X (i) : T ⟶ ℝ)$
383	380 382	imbi12d	$⊢ j = i \to (((φ \land j \in (0 \dots N)) \to X (j) : T ⟶ ℝ) \leftrightarrow ((φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ))$
384	378 383 14	chvarfv	$⊢ (φ \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
385	384	ad4ant14	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
386		simplll	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (0 \dots N)) \to φ$
387		simpr	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (0 \dots N)) \to i \in (0 \dots N)$
388		simpllr	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (0 \dots N)) \to t \in T$
389	2 375 112	nf3an	$⊢ Ⅎ j (φ \land i \in (0 \dots N) \land t \in T)$
390		nfv	$⊢ Ⅎ j X (i) (t) \leq 1$
391	389 390	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in T) \to X (i) (t) \leq 1)$
392	379	3anbi2d	$⊢ j = i \to ((φ \land j \in (0 \dots N) \land t \in T) \leftrightarrow (φ \land i \in (0 \dots N) \land t \in T))$
393	381	fveq1d	$⊢ j = i \to X (j) (t) = X (i) (t)$
394	393	breq1d	$⊢ j = i \to (X (j) (t) \leq 1 \leftrightarrow X (i) (t) \leq 1)$
395	392 394	imbi12d	$⊢ j = i \to (((φ \land j \in (0 \dots N) \land t \in T) \to X (j) (t) \leq 1) \leftrightarrow ((φ \land i \in (0 \dots N) \land t \in T) \to X (i) (t) \leq 1))$
396	391 395 16	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in T) \to X (i) (t) \leq 1$
397	386 387 388 396	syl3anc	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (0 \dots N)) \to X (i) (t) \leq 1$
398		simplll	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to φ$
399		0zd	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \in ℤ$
400		elfzel2	$⊢ i \in (j \dots N) \to N \in ℤ$
401	400	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to N \in ℤ$
402		elfzelz	$⊢ i \in (j \dots N) \to i \in ℤ$
403	402	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \in ℤ$
404	399 401 403	3jca	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to (0 \in ℤ \land N \in ℤ \land i \in ℤ)$
405		0red	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \in ℝ$
406		elfzel1	$⊢ i \in (j \dots N) \to j \in ℤ$
407	406	zred	$⊢ i \in (j \dots N) \to j \in ℝ$
408	407	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to j \in ℝ$
409	402	zred	$⊢ i \in (j \dots N) \to i \in ℝ$
410	409	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \in ℝ$
411		0red	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 0 \in ℝ$
412		1red	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 1 \in ℝ$
413		0le1	$⊢ 0 \leq 1$
414	413	a1i	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 0 \leq 1$
415		elfzle1	$⊢ j \in (1 \dots N) \to 1 \leq j$
416	183 415	syl	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 1 \leq j$
417	411 412 238 414 416	letrd	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 0 \leq j$
418	417	adantr	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \leq j$
419		elfzle1	$⊢ i \in (j \dots N) \to j \leq i$
420	419	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to j \leq i$
421	405 408 410 418 420	letrd	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \leq i$
422		elfzle2	$⊢ i \in (j \dots N) \to i \leq N$
423	422	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \leq N$
424	421 423	jca	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to (0 \leq i \land i \leq N)$
425		elfz2	$⊢ i \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land i \in ℤ) \land (0 \leq i \land i \leq N))$
426	404 424 425	sylanbrc	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \in (0 \dots N)$
427	426	adantlrr	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to i \in (0 \dots N)$
428		simpll	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to (φ \land t \in T)$
429		simplrl	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to j \in J (t)$
430		simplrr	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to t \in (D (j) ∖ D (j - 1))$
431	430	eldifad	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to t \in D (j)$
432		simpr	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to i \in (j \dots N)$
433		simpl1	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (φ \land t \in T)$
434	433	simprd	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to t \in T$
435	433 58	syl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to F (t) \in ℝ$
436	407	adantl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j \in ℝ$
437	38	a1i	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to \frac{1}{3} \in ℝ$
438	436 437	resubcld	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j - (\frac{1}{3}) \in ℝ$
439		simpl1l	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to φ$
440	439 50	syl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to E \in ℝ$
441	438 440	remulcld	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (j - (\frac{1}{3})) E \in ℝ$
442	409	adantl	$⊢ (φ \land i \in (j \dots N)) \to i \in ℝ$
443	38	a1i	$⊢ (φ \land i \in (j \dots N)) \to \frac{1}{3} \in ℝ$
444	442 443	resubcld	$⊢ (φ \land i \in (j \dots N)) \to i - (\frac{1}{3}) \in ℝ$
445	50	adantr	$⊢ (φ \land i \in (j \dots N)) \to E \in ℝ$
446	444 445	remulcld	$⊢ (φ \land i \in (j \dots N)) \to (i - (\frac{1}{3})) E \in ℝ$
447	439 446	sylancom	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (i - (\frac{1}{3})) E \in ℝ$
448		simpl3	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to t \in D (j)$
449		simpl2	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j \in J (t)$
450	433 449 183	syl2anc	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j \in (1 \dots N)$
451	439 450 363	syl2anc	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to D (j) = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
452	448 451	eleqtrd	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
453	452 367	sylib	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (t \in T \land F (t) \leq (j - (\frac{1}{3})) E)$
454	453	simprd	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to F (t) \leq (j - (\frac{1}{3})) E$
455	409	adantl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to i \in ℝ$
456	419	adantl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j \leq i$
457	436 455 437 456	lesub1dd	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j - (\frac{1}{3}) \leq i - (\frac{1}{3})$
458	439 444	sylancom	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to i - (\frac{1}{3}) \in ℝ$
459	12	rpregt0d	$⊢ φ \to (E \in ℝ \land 0 < E)$
460	439 459	syl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (E \in ℝ \land 0 < E)$
461		lemul1	$⊢ (j - (\frac{1}{3}) \in ℝ \land i - (\frac{1}{3}) \in ℝ \land (E \in ℝ \land 0 < E)) \to (j - (\frac{1}{3}) \leq i - (\frac{1}{3}) \leftrightarrow (j - (\frac{1}{3})) E \leq (i - (\frac{1}{3})) E)$
462	438 458 460 461	syl3anc	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (j - (\frac{1}{3}) \leq i - (\frac{1}{3}) \leftrightarrow (j - (\frac{1}{3})) E \leq (i - (\frac{1}{3})) E)$
463	457 462	mpbid	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to (j - (\frac{1}{3})) E \leq (i - (\frac{1}{3})) E$
464	435 441 447 454 463	letrd	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to F (t) \leq (i - (\frac{1}{3})) E$
465		rabid	$⊢ t \in \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \leftrightarrow (t \in T \land F (t) \leq (i - (\frac{1}{3})) E)$
466	434 464 465	sylanbrc	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to t \in \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\}$
467		simpr	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to i \in (j \dots N)$
468		0zd	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to 0 \in ℤ$
469	400	3ad2ant3	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to N \in ℤ$
470	402	3ad2ant3	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to i \in ℤ$
471	468 469 470	3jca	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to (0 \in ℤ \land N \in ℤ \land i \in ℤ)$
472	424	3impa	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to (0 \leq i \land i \leq N)$
473	471 472 425	sylanbrc	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to i \in (0 \dots N)$
474	433 449 467 473	syl3anc	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to i \in (0 \dots N)$
475		oveq1	$⊢ j = i \to j - (\frac{1}{3}) = i - (\frac{1}{3})$
476	475	oveq1d	$⊢ j = i \to (j - (\frac{1}{3})) E = (i - (\frac{1}{3})) E$
477	476	breq2d	$⊢ j = i \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (i - (\frac{1}{3})) E)$
478	477	rabbidv	$⊢ j = i \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\}$
479		simpr	$⊢ (φ \land i \in (0 \dots N)) \to i \in (0 \dots N)$
480		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \in V$
481	8 480	syl	$⊢ φ \to \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \in V$
482	481	adantr	$⊢ (φ \land i \in (0 \dots N)) \to \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \in V$
483	4 478 479 482	fvmptd3	$⊢ (φ \land i \in (0 \dots N)) \to D (i) = \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\}$
484	439 474 483	syl2anc	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to D (i) = \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\}$
485	466 484	eleqtrrd	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to t \in D (i)$
486	428 429 431 432 485	syl31anc	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to t \in D (i)$
487	2 375 229	nf3an	$⊢ Ⅎ j (φ \land i \in (0 \dots N) \land t \in D (i))$
488		nfv	$⊢ Ⅎ j X (i) (t) < \frac{E}{N}$
489	487 488	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in D (i)) \to X (i) (t) < \frac{E}{N})$
490	379 231	3anbi23d	$⊢ j = i \to ((φ \land j \in (0 \dots N) \land t \in D (j)) \leftrightarrow (φ \land i \in (0 \dots N) \land t \in D (i)))$
491	393	breq1d	$⊢ j = i \to (X (j) (t) < \frac{E}{N} \leftrightarrow X (i) (t) < \frac{E}{N})$
492	490 491	imbi12d	$⊢ j = i \to (((φ \land j \in (0 \dots N) \land t \in D (j)) \to X (j) (t) < \frac{E}{N}) \leftrightarrow ((φ \land i \in (0 \dots N) \land t \in D (i)) \to X (i) (t) < \frac{E}{N}))$
493	489 492 17	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in D (i)) \to X (i) (t) < \frac{E}{N}$
494	398 427 486 493	syl3anc	$⊢ (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \land i \in (j \dots N)) \to X (i) (t) < \frac{E}{N}$
495	12	ad2antrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to E \in ℝ^{+}$
496	13	ad2antrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to E < \frac{1}{3}$
497	372 373 374 385 397 494 495 496	stoweidlem11	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E$
498		eleq1w	$⊢ l = j \to (l \in J (t) \leftrightarrow j \in J (t))$
499		fveq2	$⊢ l = j \to D (l) = D (j)$
500		oveq1	$⊢ l = j \to l - 1 = j - 1$
501	500	fveq2d	$⊢ l = j \to D (l - 1) = D (j - 1)$
502	499 501	difeq12d	$⊢ l = j \to D (l) ∖ D (l - 1) = D (j) ∖ D (j - 1)$
503	502	eleq2d	$⊢ l = j \to (t \in (D (l) ∖ D (l - 1)) \leftrightarrow t \in (D (j) ∖ D (j - 1)))$
504	498 503	anbi12d	$⊢ l = j \to ((l \in J (t) \land t \in (D (l) ∖ D (l - 1))) \leftrightarrow (j \in J (t) \land t \in (D (j) ∖ D (j - 1))))$
505	504	anbi2d	$⊢ l = j \to (((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \leftrightarrow ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))))$
506		oveq1	$⊢ l = j \to l - (\frac{4}{3}) = j - (\frac{4}{3})$
507	506	oveq1d	$⊢ l = j \to (l - (\frac{4}{3})) E = (j - (\frac{4}{3})) E$
508	507	breq1d	$⊢ l = j \to ((l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) \leftrightarrow (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
509	505 508	imbi12d	$⊢ l = j \to ((((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)) \leftrightarrow (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$
510		eleq1w	$⊢ s = t \to (s \in T \leftrightarrow t \in T)$
511	510	anbi2d	$⊢ s = t \to ((φ \land s \in T) \leftrightarrow (φ \land t \in T))$
512		fveq2	$⊢ s = t \to J (s) = J (t)$
513	512	eleq2d	$⊢ s = t \to (l \in J (s) \leftrightarrow l \in J (t))$
514		eleq1w	$⊢ s = t \to (s \in (D (l) ∖ D (l - 1)) \leftrightarrow t \in (D (l) ∖ D (l - 1)))$
515	513 514	anbi12d	$⊢ s = t \to ((l \in J (s) \land s \in (D (l) ∖ D (l - 1))) \leftrightarrow (l \in J (t) \land t \in (D (l) ∖ D (l - 1))))$
516	511 515	anbi12d	$⊢ s = t \to (((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \leftrightarrow ((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))))$
517		fveq2	$⊢ s = t \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (s) = (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)$
518	517	breq2d	$⊢ s = t \to ((l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (s) \leftrightarrow (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
519	516 518	imbi12d	$⊢ s = t \to ((((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (s)) \leftrightarrow (((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$
520		nfv	$⊢ Ⅎ j s \in T$
521	2 520	nfan	$⊢ Ⅎ j (φ \land s \in T)$
522		nfcv	$⊢ \underline{Ⅎ} j s$
523	101 522	nffv	$⊢ \underline{Ⅎ} j J (s)$
524	523	nfcri	$⊢ Ⅎ j l \in J (s)$
525		nfcv	$⊢ \underline{Ⅎ} j l$
526	86 525	nffv	$⊢ \underline{Ⅎ} j D (l)$
527		nfcv	$⊢ \underline{Ⅎ} j (l - 1)$
528	86 527	nffv	$⊢ \underline{Ⅎ} j D (l - 1)$
529	526 528	nfdif	$⊢ \underline{Ⅎ} j (D (l) ∖ D (l - 1))$
530	529	nfcri	$⊢ Ⅎ j s \in (D (l) ∖ D (l - 1))$
531	524 530	nfan	$⊢ Ⅎ j (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))$
532	521 531	nfan	$⊢ Ⅎ j ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1))))$
533		nfv	$⊢ Ⅎ t s \in T$
534	3 533	nfan	$⊢ Ⅎ t (φ \land s \in T)$
535		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \{j \in (1 \dots N) \| t \in D (j)\})$
536	6 535	nfcxfr	$⊢ \underline{Ⅎ} t J$
537		nfcv	$⊢ \underline{Ⅎ} t s$
538	536 537	nffv	$⊢ \underline{Ⅎ} t J (s)$
539	538	nfcri	$⊢ Ⅎ t l \in J (s)$
540		nfcv	$⊢ \underline{Ⅎ} t l$
541	170 540	nffv	$⊢ \underline{Ⅎ} t D (l)$
542		nfcv	$⊢ \underline{Ⅎ} t (l - 1)$
543	170 542	nffv	$⊢ \underline{Ⅎ} t D (l - 1)$
544	541 543	nfdif	$⊢ \underline{Ⅎ} t (D (l) ∖ D (l - 1))$
545	544	nfcri	$⊢ Ⅎ t s \in (D (l) ∖ D (l - 1))$
546	539 545	nfan	$⊢ Ⅎ t (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))$
547	534 546	nfan	$⊢ Ⅎ t ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1))))$
548	7	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to N \in ℕ$
549	8	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to T \in V$
550	20	rabex	$⊢ \{j \in (1 \dots N) \| s \in D (j)\} \in V$
551		nfcv	$⊢ \underline{Ⅎ} t j$
552	170 551	nffv	$⊢ \underline{Ⅎ} t D (j)$
553	552	nfcri	$⊢ Ⅎ t s \in D (j)$
554		nfcv	$⊢ \underline{Ⅎ} t (1 \dots N)$
555	553 554	nfrabw	$⊢ \underline{Ⅎ} t \{j \in (1 \dots N) \| s \in D (j)\}$
556		eleq1w	$⊢ t = s \to (t \in D (j) \leftrightarrow s \in D (j))$
557	556	rabbidv	$⊢ t = s \to \{j \in (1 \dots N) \| t \in D (j)\} = \{j \in (1 \dots N) \| s \in D (j)\}$
558	537 555 557 6	fvmptf	$⊢ (s \in T \land \{j \in (1 \dots N) \| s \in D (j)\} \in V) \to J (s) = \{j \in (1 \dots N) \| s \in D (j)\}$
559	550 558	mpan2	$⊢ s \in T \to J (s) = \{j \in (1 \dots N) \| s \in D (j)\}$
560	559	eleq2d	$⊢ s \in T \to (l \in J (s) \leftrightarrow l \in \{j \in (1 \dots N) \| s \in D (j)\})$
561	560	biimpa	$⊢ (s \in T \land l \in J (s)) \to l \in \{j \in (1 \dots N) \| s \in D (j)\}$
562	526	nfcri	$⊢ Ⅎ j s \in D (l)$
563		fveq2	$⊢ j = l \to D (j) = D (l)$
564	563	eleq2d	$⊢ j = l \to (s \in D (j) \leftrightarrow s \in D (l))$
565	525 84 562 564	elrabf	$⊢ l \in \{j \in (1 \dots N) \| s \in D (j)\} \leftrightarrow (l \in (1 \dots N) \land s \in D (l))$
566	561 565	sylib	$⊢ (s \in T \land l \in J (s)) \to (l \in (1 \dots N) \land s \in D (l))$
567	566	simpld	$⊢ (s \in T \land l \in J (s)) \to l \in (1 \dots N)$
568	567	ad2ant2lr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to l \in (1 \dots N)$
569		simprr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to s \in (D (l) ∖ D (l - 1))$
570	9	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to F : T ⟶ ℝ$
571	12	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to E \in ℝ^{+}$
572	13	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to E < \frac{1}{3}$
573	384	ad4ant14	$⊢ (((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \land i \in (0 \dots N)) \to X (i) : T ⟶ ℝ$
574		simp1ll	$⊢ (((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \land i \in (0 \dots N) \land t \in T) \to φ$
575		nfv	$⊢ Ⅎ j 0 \leq X (i) (t)$
576	389 575	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t))$
577	393	breq2d	$⊢ j = i \to (0 \leq X (j) (t) \leftrightarrow 0 \leq X (i) (t))$
578	392 577	imbi12d	$⊢ j = i \to (((φ \land j \in (0 \dots N) \land t \in T) \to 0 \leq X (j) (t)) \leftrightarrow ((φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t)))$
579	576 578 15	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t)$
580	574 579	syld3an1	$⊢ (((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t)$
581		simp1ll	$⊢ (((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \land i \in (0 \dots N) \land t \in B (i)) \to φ$
582		nfmpt1	$⊢ \underline{Ⅎ} j (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
583	5 582	nfcxfr	$⊢ \underline{Ⅎ} j B$
584	583 227	nffv	$⊢ \underline{Ⅎ} j B (i)$
585	584	nfcri	$⊢ Ⅎ j t \in B (i)$
586	2 375 585	nf3an	$⊢ Ⅎ j (φ \land i \in (0 \dots N) \land t \in B (i))$
587		nfv	$⊢ Ⅎ j 1 - (\frac{E}{N}) < X (i) (t)$
588	586 587	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t))$
589		fveq2	$⊢ j = i \to B (j) = B (i)$
590	589	eleq2d	$⊢ j = i \to (t \in B (j) \leftrightarrow t \in B (i))$
591	379 590	3anbi23d	$⊢ j = i \to ((φ \land j \in (0 \dots N) \land t \in B (j)) \leftrightarrow (φ \land i \in (0 \dots N) \land t \in B (i)))$
592	393	breq2d	$⊢ j = i \to (1 - (\frac{E}{N}) < X (j) (t) \leftrightarrow 1 - (\frac{E}{N}) < X (i) (t))$
593	591 592	imbi12d	$⊢ j = i \to (((φ \land j \in (0 \dots N) \land t \in B (j)) \to 1 - (\frac{E}{N}) < X (j) (t)) \leftrightarrow ((φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)))$
594	588 593 18	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)$
595	581 594	syld3an1	$⊢ (((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)$
596	1 532 547 4 5 548 549 568 569 570 571 572 573 580 595	stoweidlem26	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (s)$
597	519 596	vtoclg	$⊢ t \in T \to (((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
598	597	ad2antlr	$⊢ ((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \to (((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
599	598	pm2.43i	$⊢ ((φ \land t \in T) \land (l \in J (t) \land t \in (D (l) ∖ D (l - 1)))) \to (l - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)$
600	509 599	vtoclg	$⊢ j \in J (t) \to (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
601	600	ad2antrl	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
602	601	pm2.43i	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)$
603	497 602	jca	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))$
604	262 371 603	3jca	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to (j \in J (t) \land ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$
605	604	ex	$⊢ (φ \land t \in T) \to ((j \in J (t) \land t \in (D (j) ∖ D (j - 1))) \to (j \in J (t) \land ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
606	113 605	eximd	$⊢ (φ \land t \in T) \to (\exists j (j \in J (t) \land t \in (D (j) ∖ D (j - 1))) \to \exists j (j \in J (t) \land ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
607	261 606	mpd	$⊢ (φ \land t \in T) \to \exists j (j \in J (t) \land ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$
608		3anass	$⊢ (j \in J (t) \land ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))) \leftrightarrow (j \in J (t) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
609	608	exbii	$⊢ \exists j (j \in J (t) \land ((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))) \leftrightarrow \exists j (j \in J (t) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
610	607 609	sylib	$⊢ (φ \land t \in T) \to \exists j (j \in J (t) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
611		df-rex	$⊢ \exists j \in J (t) (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))) \leftrightarrow \exists j (j \in J (t) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
612	610 611	sylibr	$⊢ (φ \land t \in T) \to \exists j \in J (t) (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$
613		nfcv	$⊢ \underline{Ⅎ} j ℝ$
614	103 613	ssrexf	$⊢ J (t) \subseteq ℝ \to (\exists j \in J (t) (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))) \to \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
615	30 612 614	sylc	$⊢ (φ \land t \in T) \to \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$
616	615	ex	$⊢ φ \to (t \in T \to \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t))))$
617	3 616	ralrimi	$⊢ φ \to \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land ((t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) (t)))$

Metamath Proof Explorer

Theorem stoweidlem34

Proof