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	bitrdi	$⊢ (φ \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		0red	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \in ℝ$
405		elfzel1	$⊢ i \in (j \dots N) \to j \in ℤ$
406	405	zred	$⊢ i \in (j \dots N) \to j \in ℝ$
407	406	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to j \in ℝ$
408	402	zred	$⊢ i \in (j \dots N) \to i \in ℝ$
409	408	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \in ℝ$
410		0red	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 0 \in ℝ$
411		1red	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 1 \in ℝ$
412		0le1	$⊢ 0 \leq 1$
413	412	a1i	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 0 \leq 1$
414		elfzle1	$⊢ j \in (1 \dots N) \to 1 \leq j$
415	183 414	syl	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 1 \leq j$
416	410 411 238 413 415	letrd	$⊢ ((φ \land t \in T) \land j \in J (t)) \to 0 \leq j$
417	416	adantr	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \leq j$
418		elfzle1	$⊢ i \in (j \dots N) \to j \leq i$
419	418	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to j \leq i$
420	404 407 409 417 419	letrd	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to 0 \leq i$
421		elfzle2	$⊢ i \in (j \dots N) \to i \leq N$
422	421	adantl	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \leq N$
423	399 401 403 420 422	elfzd	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to i \in (0 \dots N)$
424	423	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)$
425		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)$
426		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)$
427		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))$
428	427	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)$
429		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)$
430		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)$
431	430	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$
432	430 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 ℝ$
433	406	adantl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to j \in ℝ$
434	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 ℝ$
435	433 434	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 ℝ$
436		simpl1l	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to φ$
437	436 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 ℝ$
438	435 437	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 ℝ$
439	408	adantl	$⊢ (φ \land i \in (j \dots N)) \to i \in ℝ$
440	38	a1i	$⊢ (φ \land i \in (j \dots N)) \to \frac{1}{3} \in ℝ$
441	439 440	resubcld	$⊢ (φ \land i \in (j \dots N)) \to i - (\frac{1}{3}) \in ℝ$
442	50	adantr	$⊢ (φ \land i \in (j \dots N)) \to E \in ℝ$
443	441 442	remulcld	$⊢ (φ \land i \in (j \dots N)) \to (i - (\frac{1}{3})) E \in ℝ$
444	436 443	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 ℝ$
445		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)$
446		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)$
447	430 446 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)$
448	436 447 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\}$
449	445 448	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\}$
450	449 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)$
451	450	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$
452	408	adantl	$⊢ (((φ \land t \in T) \land j \in J (t) \land t \in D (j)) \land i \in (j \dots N)) \to i \in ℝ$
453	418	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$
454	433 452 434 453	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})$
455	436 441	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 ℝ$
456	12	rpregt0d	$⊢ φ \to (E \in ℝ \land 0 < E)$
457	436 456	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)$
458		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)$
459	435 455 457 458	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)$
460	454 459	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$
461	432 438 444 451 460	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$
462		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)$
463	431 461 462	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\}$
464		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)$
465		0zd	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to 0 \in ℤ$
466	400	3ad2ant3	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to N \in ℤ$
467	402	3ad2ant3	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to i \in ℤ$
468	465 466 467	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 ℤ)$
469	420 422	jca	$⊢ (((φ \land t \in T) \land j \in J (t)) \land i \in (j \dots N)) \to (0 \leq i \land i \leq N)$
470	469	3impa	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to (0 \leq i \land i \leq N)$
471		elfz2	$⊢ i \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land i \in ℤ) \land (0 \leq i \land i \leq N))$
472	468 470 471	sylanbrc	$⊢ ((φ \land t \in T) \land j \in J (t) \land i \in (j \dots N)) \to i \in (0 \dots N)$
473	430 446 464 472	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)$
474		oveq1	$⊢ j = i \to j - (\frac{1}{3}) = i - (\frac{1}{3})$
475	474	oveq1d	$⊢ j = i \to (j - (\frac{1}{3})) E = (i - (\frac{1}{3})) E$
476	475	breq2d	$⊢ j = i \to (F (t) \leq (j - (\frac{1}{3})) E \leftrightarrow F (t) \leq (i - (\frac{1}{3})) E)$
477	476	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\}$
478		simpr	$⊢ (φ \land i \in (0 \dots N)) \to i \in (0 \dots N)$
479		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \in V$
480	8 479	syl	$⊢ φ \to \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \in V$
481	480	adantr	$⊢ (φ \land i \in (0 \dots N)) \to \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\} \in V$
482	4 477 478 481	fvmptd3	$⊢ (φ \land i \in (0 \dots N)) \to D (i) = \{t \in T \| F (t) \leq (i - (\frac{1}{3})) E\}$
483	436 473 482	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\}$
484	463 483	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)$
485	425 426 428 429 484	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)$
486	2 375 229	nf3an	$⊢ Ⅎ j (φ \land i \in (0 \dots N) \land t \in D (i))$
487		nfv	$⊢ Ⅎ j X (i) (t) < \frac{E}{N}$
488	486 487	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in D (i)) \to X (i) (t) < \frac{E}{N})$
489	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)))$
490	393	breq1d	$⊢ j = i \to (X (j) (t) < \frac{E}{N} \leftrightarrow X (i) (t) < \frac{E}{N})$
491	489 490	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}))$
492	488 491 17	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in D (i)) \to X (i) (t) < \frac{E}{N}$
493	398 424 485 492	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}$
494	12	ad2antrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to E \in ℝ^{+}$
495	13	ad2antrr	$⊢ ((φ \land t \in T) \land (j \in J (t) \land t \in (D (j) ∖ D (j - 1)))) \to E < \frac{1}{3}$
496	372 373 374 385 397 493 494 495	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$
497		eleq1w	$⊢ l = j \to (l \in J (t) \leftrightarrow j \in J (t))$
498		fveq2	$⊢ l = j \to D (l) = D (j)$
499		oveq1	$⊢ l = j \to l - 1 = j - 1$
500	499	fveq2d	$⊢ l = j \to D (l - 1) = D (j - 1)$
501	498 500	difeq12d	$⊢ l = j \to D (l) ∖ D (l - 1) = D (j) ∖ D (j - 1)$
502	501	eleq2d	$⊢ l = j \to (t \in (D (l) ∖ D (l - 1)) \leftrightarrow t \in (D (j) ∖ D (j - 1)))$
503	497 502	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))))$
504	503	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)))))$
505		oveq1	$⊢ l = j \to l - (\frac{4}{3}) = j - (\frac{4}{3})$
506	505	oveq1d	$⊢ l = j \to (l - (\frac{4}{3})) E = (j - (\frac{4}{3})) E$
507	506	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))$
508	504 507	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)))$
509		eleq1w	$⊢ s = t \to (s \in T \leftrightarrow t \in T)$
510	509	anbi2d	$⊢ s = t \to ((φ \land s \in T) \leftrightarrow (φ \land t \in T))$
511		fveq2	$⊢ s = t \to J (s) = J (t)$
512	511	eleq2d	$⊢ s = t \to (l \in J (s) \leftrightarrow l \in J (t))$
513		eleq1w	$⊢ s = t \to (s \in (D (l) ∖ D (l - 1)) \leftrightarrow t \in (D (l) ∖ D (l - 1)))$
514	512 513	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))))$
515	510 514	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)))))$
516		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)$
517	516	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))$
518	515 517	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)))$
519		nfv	$⊢ Ⅎ j s \in T$
520	2 519	nfan	$⊢ Ⅎ j (φ \land s \in T)$
521		nfcv	$⊢ \underline{Ⅎ} j s$
522	101 521	nffv	$⊢ \underline{Ⅎ} j J (s)$
523	522	nfcri	$⊢ Ⅎ j l \in J (s)$
524		nfcv	$⊢ \underline{Ⅎ} j l$
525	86 524	nffv	$⊢ \underline{Ⅎ} j D (l)$
526		nfcv	$⊢ \underline{Ⅎ} j (l - 1)$
527	86 526	nffv	$⊢ \underline{Ⅎ} j D (l - 1)$
528	525 527	nfdif	$⊢ \underline{Ⅎ} j (D (l) ∖ D (l - 1))$
529	528	nfcri	$⊢ Ⅎ j s \in (D (l) ∖ D (l - 1))$
530	523 529	nfan	$⊢ Ⅎ j (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))$
531	520 530	nfan	$⊢ Ⅎ j ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1))))$
532		nfv	$⊢ Ⅎ t s \in T$
533	3 532	nfan	$⊢ Ⅎ t (φ \land s \in T)$
534		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \{j \in (1 \dots N) \| t \in D (j)\})$
535	6 534	nfcxfr	$⊢ \underline{Ⅎ} t J$
536		nfcv	$⊢ \underline{Ⅎ} t s$
537	535 536	nffv	$⊢ \underline{Ⅎ} t J (s)$
538	537	nfcri	$⊢ Ⅎ t l \in J (s)$
539		nfcv	$⊢ \underline{Ⅎ} t l$
540	170 539	nffv	$⊢ \underline{Ⅎ} t D (l)$
541		nfcv	$⊢ \underline{Ⅎ} t (l - 1)$
542	170 541	nffv	$⊢ \underline{Ⅎ} t D (l - 1)$
543	540 542	nfdif	$⊢ \underline{Ⅎ} t (D (l) ∖ D (l - 1))$
544	543	nfcri	$⊢ Ⅎ t s \in (D (l) ∖ D (l - 1))$
545	538 544	nfan	$⊢ Ⅎ t (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))$
546	533 545	nfan	$⊢ Ⅎ t ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1))))$
547	7	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to N \in ℕ$
548	8	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to T \in V$
549	20	rabex	$⊢ \{j \in (1 \dots N) \| s \in D (j)\} \in V$
550		nfcv	$⊢ \underline{Ⅎ} t j$
551	170 550	nffv	$⊢ \underline{Ⅎ} t D (j)$
552	551	nfcri	$⊢ Ⅎ t s \in D (j)$
553		nfcv	$⊢ \underline{Ⅎ} t (1 \dots N)$
554	552 553	nfrabw	$⊢ \underline{Ⅎ} t \{j \in (1 \dots N) \| s \in D (j)\}$
555		eleq1w	$⊢ t = s \to (t \in D (j) \leftrightarrow s \in D (j))$
556	555	rabbidv	$⊢ t = s \to \{j \in (1 \dots N) \| t \in D (j)\} = \{j \in (1 \dots N) \| s \in D (j)\}$
557	536 554 556 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)\}$
558	549 557	mpan2	$⊢ s \in T \to J (s) = \{j \in (1 \dots N) \| s \in D (j)\}$
559	558	eleq2d	$⊢ s \in T \to (l \in J (s) \leftrightarrow l \in \{j \in (1 \dots N) \| s \in D (j)\})$
560	559	biimpa	$⊢ (s \in T \land l \in J (s)) \to l \in \{j \in (1 \dots N) \| s \in D (j)\}$
561	525	nfcri	$⊢ Ⅎ j s \in D (l)$
562		fveq2	$⊢ j = l \to D (j) = D (l)$
563	562	eleq2d	$⊢ j = l \to (s \in D (j) \leftrightarrow s \in D (l))$
564	524 84 561 563	elrabf	$⊢ l \in \{j \in (1 \dots N) \| s \in D (j)\} \leftrightarrow (l \in (1 \dots N) \land s \in D (l))$
565	560 564	sylib	$⊢ (s \in T \land l \in J (s)) \to (l \in (1 \dots N) \land s \in D (l))$
566	565	simpld	$⊢ (s \in T \land l \in J (s)) \to l \in (1 \dots N)$
567	566	ad2ant2lr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to l \in (1 \dots N)$
568		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))$
569	9	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to F : T ⟶ ℝ$
570	12	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to E \in ℝ^{+}$
571	13	ad2antrr	$⊢ ((φ \land s \in T) \land (l \in J (s) \land s \in (D (l) ∖ D (l - 1)))) \to E < \frac{1}{3}$
572	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 ⟶ ℝ$
573		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 φ$
574		nfv	$⊢ Ⅎ j 0 \leq X (i) (t)$
575	389 574	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t))$
576	393	breq2d	$⊢ j = i \to (0 \leq X (j) (t) \leftrightarrow 0 \leq X (i) (t))$
577	392 576	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)))$
578	575 577 15	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in T) \to 0 \leq X (i) (t)$
579	573 578	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)$
580		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 φ$
581		nfmpt1	$⊢ \underline{Ⅎ} j (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
582	5 581	nfcxfr	$⊢ \underline{Ⅎ} j B$
583	582 227	nffv	$⊢ \underline{Ⅎ} j B (i)$
584	583	nfcri	$⊢ Ⅎ j t \in B (i)$
585	2 375 584	nf3an	$⊢ Ⅎ j (φ \land i \in (0 \dots N) \land t \in B (i))$
586		nfv	$⊢ Ⅎ j 1 - (\frac{E}{N}) < X (i) (t)$
587	585 586	nfim	$⊢ Ⅎ j ((φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t))$
588		fveq2	$⊢ j = i \to B (j) = B (i)$
589	588	eleq2d	$⊢ j = i \to (t \in B (j) \leftrightarrow t \in B (i))$
590	379 589	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)))$
591	393	breq2d	$⊢ j = i \to (1 - (\frac{E}{N}) < X (j) (t) \leftrightarrow 1 - (\frac{E}{N}) < X (i) (t))$
592	590 591	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)))$
593	587 592 18	chvarfv	$⊢ (φ \land i \in (0 \dots N) \land t \in B (i)) \to 1 - (\frac{E}{N}) < X (i) (t)$
594	580 593	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)$
595	1 531 546 4 5 547 548 567 568 569 570 571 572 579 594	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)$
596	518 595	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))$
597	596	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))$
598	597	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)$
599	508 598	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))$
600	599	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))$
601	600	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)$
602	496 601	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))$
603	262 371 602	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)))$
604	603	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))))$
605	113 604	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))))$
606	261 605	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)))$
607		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))))$
608	607	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))))$
609	606 608	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))))$
610		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))))$
611	609 610	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)))$
612		nfcv	$⊢ \underline{Ⅎ} j ℝ$
613	103 612	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))))$
614	30 611 613	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)))$
615	614	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))))$
616	3 615	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