stoweidlem60

Description: This lemma proves that there exists a function g as in the proof in BrosowskiDeutsh p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all t in T , there is a j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here F is used to represent f in the paper, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem60.1	$⊢ \underline{Ⅎ} t F$
	stoweidlem60.2	$⊢ Ⅎ t φ$
	stoweidlem60.3	$⊢ K = topGen (ran (.))$
	stoweidlem60.4	$⊢ T = ⋃ J$
	stoweidlem60.5	$⊢ C = J Cn K$
	stoweidlem60.6	$⊢ D = (j \in (0 \dots n) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
	stoweidlem60.7	$⊢ B = (j \in (0 \dots n) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
	stoweidlem60.8	$⊢ φ \to J \in Comp$
	stoweidlem60.9	$⊢ φ \to T \neq \emptyset$
	stoweidlem60.10	$⊢ φ \to A \subseteq C$
	stoweidlem60.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem60.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem60.13	$⊢ (φ \land y \in ℝ) \to (t \in T ⟼ y) \in A$
	stoweidlem60.14	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem60.15	$⊢ φ \to F \in C$
	stoweidlem60.16	$⊢ φ \to \forall t \in T 0 \leq F (t)$
	stoweidlem60.17	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem60.18	$⊢ φ \to E < \frac{1}{3}$
Assertion	stoweidlem60	$⊢ φ \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem60.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem60.2	$⊢ Ⅎ t φ$
3		stoweidlem60.3	$⊢ K = topGen (ran (.))$
4		stoweidlem60.4	$⊢ T = ⋃ J$
5		stoweidlem60.5	$⊢ C = J Cn K$
6		stoweidlem60.6	$⊢ D = (j \in (0 \dots n) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
7		stoweidlem60.7	$⊢ B = (j \in (0 \dots n) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
8		stoweidlem60.8	$⊢ φ \to J \in Comp$
9		stoweidlem60.9	$⊢ φ \to T \neq \emptyset$
10		stoweidlem60.10	$⊢ φ \to A \subseteq C$
11		stoweidlem60.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
12		stoweidlem60.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
13		stoweidlem60.13	$⊢ (φ \land y \in ℝ) \to (t \in T ⟼ y) \in A$
14		stoweidlem60.14	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
15		stoweidlem60.15	$⊢ φ \to F \in C$
16		stoweidlem60.16	$⊢ φ \to \forall t \in T 0 \leq F (t)$
17		stoweidlem60.17	$⊢ φ \to E \in ℝ^{+}$
18		stoweidlem60.18	$⊢ φ \to E < \frac{1}{3}$
19		nnre	$⊢ m \in ℕ \to m \in ℝ$
20	19	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℝ$
21	17	rpred	$⊢ φ \to E \in ℝ$
22	21	adantr	$⊢ (φ \land m \in ℕ) \to E \in ℝ$
23	17	rpne0d	$⊢ φ \to E \neq 0$
24	23	adantr	$⊢ (φ \land m \in ℕ) \to E \neq 0$
25	20 22 24	redivcld	$⊢ (φ \land m \in ℕ) \to \frac{m}{E} \in ℝ$
26		1red	$⊢ (φ \land m \in ℕ) \to 1 \in ℝ$
27	25 26	readdcld	$⊢ (φ \land m \in ℕ) \to (\frac{m}{E}) + 1 \in ℝ$
28	27	adantr	$⊢ ((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \to (\frac{m}{E}) + 1 \in ℝ$
29		arch	$⊢ (\frac{m}{E}) + 1 \in ℝ \to \exists n \in ℕ (\frac{m}{E}) + 1 < n$
30	28 29	syl	$⊢ ((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \to \exists n \in ℕ (\frac{m}{E}) + 1 < n$
31		nfv	$⊢ Ⅎ t m \in ℕ$
32	2 31	nfan	$⊢ Ⅎ t (φ \land m \in ℕ)$
33		nfra1	$⊢ Ⅎ t \forall t \in T F (t) < m$
34	32 33	nfan	$⊢ Ⅎ t ((φ \land m \in ℕ) \land \forall t \in T F (t) < m)$
35		nfv	$⊢ Ⅎ t n \in ℕ$
36	34 35	nfan	$⊢ Ⅎ t (((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ)$
37		nfv	$⊢ Ⅎ t (\frac{m}{E}) + 1 < n$
38	36 37	nfan	$⊢ Ⅎ t ((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n)$
39		simp-5l	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to φ$
40	3 4 5 15	fcnre	$⊢ φ \to F : T ⟶ ℝ$
41	40	ffvelrnda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
42	39 41	sylancom	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to F (t) \in ℝ$
43		simp-5r	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to m \in ℕ$
44	43	nnred	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to m \in ℝ$
45		simpllr	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to n \in ℕ$
46	45	nnred	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to n \in ℝ$
47		1red	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to 1 \in ℝ$
48	46 47	resubcld	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to n - 1 \in ℝ$
49	39 21	syl	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to E \in ℝ$
50	48 49	remulcld	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to (n - 1) E \in ℝ$
51		simpllr	$⊢ ((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to \forall t \in T F (t) < m$
52	51	r19.21bi	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to F (t) < m$
53		simplr	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to (\frac{m}{E}) + 1 < n$
54		simpr	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to (\frac{m}{E}) + 1 < n$
55		simpl1	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to φ$
56		simpl2	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to m \in ℕ$
57	55 56 25	syl2anc	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to \frac{m}{E} \in ℝ$
58		1red	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to 1 \in ℝ$
59		simpl3	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to n \in ℕ$
60	59	nnred	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to n \in ℝ$
61	57 58 60	ltaddsubd	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to ((\frac{m}{E}) + 1 < n \leftrightarrow \frac{m}{E} < n - 1)$
62	54 61	mpbid	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to \frac{m}{E} < n - 1$
63	19	3ad2ant2	$⊢ (φ \land m \in ℕ \land n \in ℕ) \to m \in ℝ$
64	63	adantr	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to m \in ℝ$
65	60 58	resubcld	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to n - 1 \in ℝ$
66	21	3ad2ant1	$⊢ (φ \land m \in ℕ \land n \in ℕ) \to E \in ℝ$
67	66	adantr	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to E \in ℝ$
68	17	rpgt0d	$⊢ φ \to 0 < E$
69	55 68	syl	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to 0 < E$
70		ltdivmul2	$⊢ (m \in ℝ \land n - 1 \in ℝ \land (E \in ℝ \land 0 < E)) \to (\frac{m}{E} < n - 1 \leftrightarrow m < (n - 1) E)$
71	64 65 67 69 70	syl112anc	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to (\frac{m}{E} < n - 1 \leftrightarrow m < (n - 1) E)$
72	62 71	mpbid	$⊢ ((φ \land m \in ℕ \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to m < (n - 1) E$
73	39 43 45 53 72	syl31anc	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to m < (n - 1) E$
74	42 44 50 52 73	lttrd	$⊢ (((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \land t \in T) \to F (t) < (n - 1) E$
75	74	ex	$⊢ ((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to (t \in T \to F (t) < (n - 1) E)$
76	38 75	ralrimi	$⊢ ((((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \land (\frac{m}{E}) + 1 < n) \to \forall t \in T F (t) < (n - 1) E$
77	76	ex	$⊢ (((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \land n \in ℕ) \to ((\frac{m}{E}) + 1 < n \to \forall t \in T F (t) < (n - 1) E)$
78	77	reximdva	$⊢ ((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \to (\exists n \in ℕ (\frac{m}{E}) + 1 < n \to \exists n \in ℕ \forall t \in T F (t) < (n - 1) E)$
79	30 78	mpd	$⊢ ((φ \land m \in ℕ) \land \forall t \in T F (t) < m) \to \exists n \in ℕ \forall t \in T F (t) < (n - 1) E$
80	1 2 3 8 4 9 5 15	rfcnnnub	$⊢ φ \to \exists m \in ℕ \forall t \in T F (t) < m$
81	79 80	r19.29a	$⊢ φ \to \exists n \in ℕ \forall t \in T F (t) < (n - 1) E$
82		df-rex	$⊢ \exists n \in ℕ \forall t \in T F (t) < (n - 1) E \leftrightarrow \exists n (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)$
83	81 82	sylib	$⊢ φ \to \exists n (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)$
84		simpr	$⊢ (φ \land (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)) \to (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)$
85	2 35	nfan	$⊢ Ⅎ t (φ \land n \in ℕ)$
86		eqid	$⊢ \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\} = \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\}$
87		eqid	$⊢ (j \in (0 \dots n) ⟼ \{y \in \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\} \| (\forall t \in D (j) y (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < y (t))\}) = (j \in (0 \dots n) ⟼ \{y \in \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\} \| (\forall t \in D (j) y (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < y (t))\})$
88	8	adantr	$⊢ (φ \land n \in ℕ) \to J \in Comp$
89	10	adantr	$⊢ (φ \land n \in ℕ) \to A \subseteq C$
90	11	3adant1r	$⊢ ((φ \land n \in ℕ) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
91	12	3adant1r	$⊢ ((φ \land n \in ℕ) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
92	13	adantlr	$⊢ ((φ \land n \in ℕ) \land y \in ℝ) \to (t \in T ⟼ y) \in A$
93	14	adantlr	$⊢ ((φ \land n \in ℕ) \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
94	15	adantr	$⊢ (φ \land n \in ℕ) \to F \in C$
95	17	adantr	$⊢ (φ \land n \in ℕ) \to E \in ℝ^{+}$
96	18	adantr	$⊢ (φ \land n \in ℕ) \to E < \frac{1}{3}$
97		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
98	1 85 3 4 5 6 7 86 87 88 89 90 91 92 93 94 95 96 97	stoweidlem59	$⊢ (φ \land n \in ℕ) \to \exists x (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))$
99	98	adantrr	$⊢ (φ \land (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)) \to \exists x (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))$
100		19.42v	$⊢ \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \leftrightarrow ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land \exists x (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
101	84 99 100	sylanbrc	$⊢ (φ \land (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)) \to \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
102		3anass	$⊢ ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))) \leftrightarrow ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
103	102	exbii	$⊢ \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))) \leftrightarrow \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land (x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
104	101 103	sylibr	$⊢ (φ \land (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)) \to \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))$
105	104	ex	$⊢ φ \to ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \to \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
106	105	eximdv	$⊢ φ \to (\exists n (n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \to \exists n \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
107	83 106	mpd	$⊢ φ \to \exists n \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))$
108		simpl	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to φ$
109		simpr1l	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to n \in ℕ$
110		simpr2	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to x : (0 \dots n) ⟶ A$
111		nfv	$⊢ Ⅎ t x : (0 \dots n) ⟶ A$
112	2 35 111	nf3an	$⊢ Ⅎ t (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A)$
113		simp2	$⊢ (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \to n \in ℕ$
114		simp3	$⊢ (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \to x : (0 \dots n) ⟶ A$
115		simp1	$⊢ (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \to φ$
116	115 11	syl3an1	$⊢ ((φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
117	115 12	syl3an1	$⊢ ((φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
118	13	3ad2antl1	$⊢ ((φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \land y \in ℝ) \to (t \in T ⟼ y) \in A$
119	17	3ad2ant1	$⊢ (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \to E \in ℝ^{+}$
120	119	rpred	$⊢ (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \to E \in ℝ$
121	10	sselda	$⊢ (φ \land f \in A) \to f \in C$
122	3 4 5 121	fcnre	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
123	122	3ad2antl1	$⊢ ((φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \land f \in A) \to f : T ⟶ ℝ$
124	112 113 114 116 117 118 120 123	stoweidlem17	$⊢ (φ \land n \in ℕ \land x : (0 \dots n) ⟶ A) \to (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \in A$
125	108 109 110 124	syl3anc	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \in A$
126		nfv	$⊢ Ⅎ j φ$
127		nfv	$⊢ Ⅎ j (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)$
128		nfv	$⊢ Ⅎ j x : (0 \dots n) ⟶ A$
129		nfra1	$⊢ Ⅎ j \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
130	127 128 129	nf3an	$⊢ Ⅎ j ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))$
131	126 130	nfan	$⊢ Ⅎ j (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
132		nfra1	$⊢ Ⅎ t \forall t \in T F (t) < (n - 1) E$
133	35 132	nfan	$⊢ Ⅎ t (n \in ℕ \land \forall t \in T F (t) < (n - 1) E)$
134		nfcv	$⊢ \underline{Ⅎ} t (0 \dots n)$
135		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1)$
136		nfra1	$⊢ Ⅎ t \forall t \in D (j) x (j) (t) < \frac{E}{n}$
137		nfra1	$⊢ Ⅎ t \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)$
138	135 136 137	nf3an	$⊢ Ⅎ t (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
139	134 138	nfralw	$⊢ Ⅎ t \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
140	133 111 139	nf3an	$⊢ Ⅎ t ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))$
141	2 140	nfan	$⊢ Ⅎ t (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))))$
142		eqid	$⊢ (t \in T ⟼ \{j \in (1 \dots n) \| t \in D (j)\}) = (t \in T ⟼ \{j \in (1 \dots n) \| t \in D (j)\})$
143	8	uniexd	$⊢ φ \to ⋃ J \in V$
144	4 143	eqeltrid	$⊢ φ \to T \in V$
145	144	adantr	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to T \in V$
146	40	adantr	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to F : T ⟶ ℝ$
147	16	r19.21bi	$⊢ (φ \land t \in T) \to 0 \leq F (t)$
148	147	adantlr	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land t \in T) \to 0 \leq F (t)$
149		simpr1r	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to \forall t \in T F (t) < (n - 1) E$
150	149	r19.21bi	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land t \in T) \to F (t) < (n - 1) E$
151	17	adantr	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to E \in ℝ^{+}$
152	18	adantr	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to E < \frac{1}{3}$
153		simpll	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n)) \to φ$
154		simplr2	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n)) \to x : (0 \dots n) ⟶ A$
155		simpr	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n)) \to j \in (0 \dots n)$
156		simp1	$⊢ (φ \land x : (0 \dots n) ⟶ A \land j \in (0 \dots n)) \to φ$
157		ffvelrn	$⊢ (x : (0 \dots n) ⟶ A \land j \in (0 \dots n)) \to x (j) \in A$
158	157	3adant1	$⊢ (φ \land x : (0 \dots n) ⟶ A \land j \in (0 \dots n)) \to x (j) \in A$
159	10	sselda	$⊢ (φ \land x (j) \in A) \to x (j) \in C$
160	3 4 5 159	fcnre	$⊢ (φ \land x (j) \in A) \to x (j) : T ⟶ ℝ$
161	156 158 160	syl2anc	$⊢ (φ \land x : (0 \dots n) ⟶ A \land j \in (0 \dots n)) \to x (j) : T ⟶ ℝ$
162	153 154 155 161	syl3anc	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n)) \to x (j) : T ⟶ ℝ$
163		simp1r3	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
164		r19.26-3	$⊢ \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)) \leftrightarrow (\forall j \in (0 \dots n) \forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall j \in (0 \dots n) \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall j \in (0 \dots n) \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
165	164	simp1bi	$⊢ \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)) \to \forall j \in (0 \dots n) \forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1)$
166		simpl	$⊢ (0 \leq x (j) (t) \land x (j) (t) \leq 1) \to 0 \leq x (j) (t)$
167	166	2ralimi	$⊢ \forall j \in (0 \dots n) \forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \to \forall j \in (0 \dots n) \forall t \in T 0 \leq x (j) (t)$
168	163 165 167	3syl	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to \forall j \in (0 \dots n) \forall t \in T 0 \leq x (j) (t)$
169		simp2	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to j \in (0 \dots n)$
170		simp3	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to t \in T$
171		rspa	$⊢ (\forall j \in (0 \dots n) \forall t \in T 0 \leq x (j) (t) \land j \in (0 \dots n)) \to \forall t \in T 0 \leq x (j) (t)$
172	171	r19.21bi	$⊢ ((\forall j \in (0 \dots n) \forall t \in T 0 \leq x (j) (t) \land j \in (0 \dots n)) \land t \in T) \to 0 \leq x (j) (t)$
173	168 169 170 172	syl21anc	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to 0 \leq x (j) (t)$
174		simpr	$⊢ (0 \leq x (j) (t) \land x (j) (t) \leq 1) \to x (j) (t) \leq 1$
175	174	2ralimi	$⊢ \forall j \in (0 \dots n) \forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \to \forall j \in (0 \dots n) \forall t \in T x (j) (t) \leq 1$
176	163 165 175	3syl	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to \forall j \in (0 \dots n) \forall t \in T x (j) (t) \leq 1$
177		rspa	$⊢ (\forall j \in (0 \dots n) \forall t \in T x (j) (t) \leq 1 \land j \in (0 \dots n)) \to \forall t \in T x (j) (t) \leq 1$
178	177	r19.21bi	$⊢ ((\forall j \in (0 \dots n) \forall t \in T x (j) (t) \leq 1 \land j \in (0 \dots n)) \land t \in T) \to x (j) (t) \leq 1$
179	176 169 170 178	syl21anc	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in T) \to x (j) (t) \leq 1$
180		simp1r3	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in D (j)) \to \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
181	164	simp2bi	$⊢ \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)) \to \forall j \in (0 \dots n) \forall t \in D (j) x (j) (t) < \frac{E}{n}$
182	180 181	syl	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in D (j)) \to \forall j \in (0 \dots n) \forall t \in D (j) x (j) (t) < \frac{E}{n}$
183		simp2	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in D (j)) \to j \in (0 \dots n)$
184		simp3	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in D (j)) \to t \in D (j)$
185		rspa	$⊢ (\forall j \in (0 \dots n) \forall t \in D (j) x (j) (t) < \frac{E}{n} \land j \in (0 \dots n)) \to \forall t \in D (j) x (j) (t) < \frac{E}{n}$
186	185	r19.21bi	$⊢ ((\forall j \in (0 \dots n) \forall t \in D (j) x (j) (t) < \frac{E}{n} \land j \in (0 \dots n)) \land t \in D (j)) \to x (j) (t) < \frac{E}{n}$
187	182 183 184 186	syl21anc	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in D (j)) \to x (j) (t) < \frac{E}{n}$
188		simp1r3	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in B (j)) \to \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))$
189	164	simp3bi	$⊢ \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)) \to \forall j \in (0 \dots n) \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)$
190	188 189	syl	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in B (j)) \to \forall j \in (0 \dots n) \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)$
191		simp2	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in B (j)) \to j \in (0 \dots n)$
192		simp3	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in B (j)) \to t \in B (j)$
193		rspa	$⊢ (\forall j \in (0 \dots n) \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t) \land j \in (0 \dots n)) \to \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)$
194	193	r19.21bi	$⊢ ((\forall j \in (0 \dots n) \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t) \land j \in (0 \dots n)) \land t \in B (j)) \to 1 - (\frac{E}{n}) < x (j) (t)$
195	190 191 192 194	syl21anc	$⊢ ((φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \land j \in (0 \dots n) \land t \in B (j)) \to 1 - (\frac{E}{n}) < x (j) (t)$
196	1 131 141 6 7 142 109 145 146 148 150 151 152 162 173 179 187 195	stoweidlem34	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \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)))$
197		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t))$
198	197	nfeq2	$⊢ Ⅎ t g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t))$
199		fveq1	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \to g (t) = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) (t)$
200	199	breq1d	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \to (g (t) < (j + (\frac{1}{3})) E \leftrightarrow (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) (t) < (j + (\frac{1}{3})) E)$
201	199	breq2d	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \to ((j - (\frac{4}{3})) E < g (t) \leftrightarrow (j - (\frac{4}{3})) E < (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) (t))$
202	200 201	anbi12d	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \to ((g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)) \leftrightarrow ((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)))$
203	202	anbi2d	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \to ((((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \leftrightarrow (((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))))$
204	203	rexbidv	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \to (\exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \leftrightarrow \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))))$
205	198 204	ralbid	$⊢ g = (t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \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 (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \leftrightarrow \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))))$
206	205	rspcev	$⊢ ((t \in T ⟼ \sum_{i = 0}^{n} E x (i) (t)) \in A \land \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)))) \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$
207	125 196 206	syl2anc	$⊢ (φ \land ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t)))) \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$
208	207	ex	$⊢ φ \to (((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))) \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))))$
209	208	2eximdv	$⊢ φ \to (\exists n \exists x ((n \in ℕ \land \forall t \in T F (t) < (n - 1) E) \land x : (0 \dots n) ⟶ A \land \forall j \in (0 \dots n) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{n} \land \forall t \in B (j) 1 - (\frac{E}{n}) < x (j) (t))) \to \exists n \exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))))$
210	107 209	mpd	$⊢ φ \to \exists n \exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$
211		idd	$⊢ φ \to (\exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))))$
212	211	exlimdv	$⊢ φ \to (\exists n \exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))))$
213	210 212	mpd	$⊢ φ \to \exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$
214		idd	$⊢ φ \to (\exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))))$
215	214	exlimdv	$⊢ φ \to (\exists x \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))))$
216	213 215	mpd	$⊢ φ \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$

Metamath Proof Explorer

Theorem stoweidlem60

Proof