stoweidlem51

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem51.1	$⊢ Ⅎ i φ$
	stoweidlem51.2	$⊢ Ⅎ t φ$
	stoweidlem51.3	$⊢ Ⅎ w φ$
	stoweidlem51.4	$⊢ \underline{Ⅎ} w V$
	stoweidlem51.5	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
	stoweidlem51.6	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
	stoweidlem51.7	$⊢ X = seq 1 (P, U) (M)$
	stoweidlem51.8	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
	stoweidlem51.9	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
	stoweidlem51.10	$⊢ φ \to M \in ℕ$
	stoweidlem51.11	$⊢ φ \to W : (1 \dots M) ⟶ V$
	stoweidlem51.12	$⊢ φ \to U : (1 \dots M) ⟶ Y$
	stoweidlem51.13	$⊢ (φ \land w \in V) \to w \subseteq T$
	stoweidlem51.14	$⊢ φ \to D \subseteq ⋃ ran W$
	stoweidlem51.15	$⊢ φ \to D \subseteq T$
	stoweidlem51.16	$⊢ φ \to B \subseteq T$
	stoweidlem51.17	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in W (i) U (i) (t) < \frac{E}{M}$
	stoweidlem51.18	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in B 1 - (\frac{E}{M}) < U (i) (t)$
	stoweidlem51.19	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem51.20	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem51.21	$⊢ φ \to T \in V$
	stoweidlem51.22	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem51.23	$⊢ φ \to E < \frac{1}{3}$
Assertion	stoweidlem51	$⊢ φ \to \exists x (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem51.1	$⊢ Ⅎ i φ$
2		stoweidlem51.2	$⊢ Ⅎ t φ$
3		stoweidlem51.3	$⊢ Ⅎ w φ$
4		stoweidlem51.4	$⊢ \underline{Ⅎ} w V$
5		stoweidlem51.5	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
6		stoweidlem51.6	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
7		stoweidlem51.7	$⊢ X = seq 1 (P, U) (M)$
8		stoweidlem51.8	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
9		stoweidlem51.9	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
10		stoweidlem51.10	$⊢ φ \to M \in ℕ$
11		stoweidlem51.11	$⊢ φ \to W : (1 \dots M) ⟶ V$
12		stoweidlem51.12	$⊢ φ \to U : (1 \dots M) ⟶ Y$
13		stoweidlem51.13	$⊢ (φ \land w \in V) \to w \subseteq T$
14		stoweidlem51.14	$⊢ φ \to D \subseteq ⋃ ran W$
15		stoweidlem51.15	$⊢ φ \to D \subseteq T$
16		stoweidlem51.16	$⊢ φ \to B \subseteq T$
17		stoweidlem51.17	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in W (i) U (i) (t) < \frac{E}{M}$
18		stoweidlem51.18	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in B 1 - (\frac{E}{M}) < U (i) (t)$
19		stoweidlem51.19	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
20		stoweidlem51.20	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
21		stoweidlem51.21	$⊢ φ \to T \in V$
22		stoweidlem51.22	$⊢ φ \to E \in ℝ^{+}$
23		stoweidlem51.23	$⊢ φ \to E < \frac{1}{3}$
24		ssrab2	$⊢ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \subseteq A$
25	5 24	eqsstri	$⊢ Y \subseteq A$
26		1zzd	$⊢ φ \to 1 \in ℤ$
27	10	nnzd	$⊢ φ \to M \in ℤ$
28	10	nnge1d	$⊢ φ \to 1 \leq M$
29	10	nnred	$⊢ φ \to M \in ℝ$
30	29	leidd	$⊢ φ \to M \leq M$
31	26 27 27 28 30	elfzd	$⊢ φ \to M \in (1 \dots M)$
32		eqid	$⊢ (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ f (t) g (t))$
33	2 5 32 20 19	stoweidlem16	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
34	6 7 31 12 33 21	fmulcl	$⊢ φ \to X \in Y$
35	25 34	sselid	$⊢ φ \to X \in A$
36	5	eleq2i	$⊢ X \in Y \leftrightarrow X \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
37		nfcv	$⊢ \underline{Ⅎ} h 1$
38		nfrab1	$⊢ \underline{Ⅎ} h \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
39	5 38	nfcxfr	$⊢ \underline{Ⅎ} h Y$
40		nfcv	$⊢ \underline{Ⅎ} h (t \in T ⟼ f (t) g (t))$
41	39 39 40	nfmpo	$⊢ \underline{Ⅎ} h (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
42	6 41	nfcxfr	$⊢ \underline{Ⅎ} h P$
43		nfcv	$⊢ \underline{Ⅎ} h U$
44	37 42 43	nfseq	$⊢ \underline{Ⅎ} h seq 1 (P, U)$
45		nfcv	$⊢ \underline{Ⅎ} h M$
46	44 45	nffv	$⊢ \underline{Ⅎ} h seq 1 (P, U) (M)$
47	7 46	nfcxfr	$⊢ \underline{Ⅎ} h X$
48		nfcv	$⊢ \underline{Ⅎ} h A$
49		nfcv	$⊢ \underline{Ⅎ} h T$
50		nfcv	$⊢ \underline{Ⅎ} h 0$
51		nfcv	$⊢ \underline{Ⅎ} h \leq$
52		nfcv	$⊢ \underline{Ⅎ} h t$
53	47 52	nffv	$⊢ \underline{Ⅎ} h X (t)$
54	50 51 53	nfbr	$⊢ Ⅎ h 0 \leq X (t)$
55	53 51 37	nfbr	$⊢ Ⅎ h X (t) \leq 1$
56	54 55	nfan	$⊢ Ⅎ h (0 \leq X (t) \land X (t) \leq 1)$
57	49 56	nfralw	$⊢ Ⅎ h \forall t \in T (0 \leq X (t) \land X (t) \leq 1)$
58		nfcv	$⊢ \underline{Ⅎ} t 1$
59		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq h (t) \land h (t) \leq 1)$
60		nfcv	$⊢ \underline{Ⅎ} t A$
61	59 60	nfrabw	$⊢ \underline{Ⅎ} t \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
62	5 61	nfcxfr	$⊢ \underline{Ⅎ} t Y$
63		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ f (t) g (t))$
64	62 62 63	nfmpo	$⊢ \underline{Ⅎ} t (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
65	6 64	nfcxfr	$⊢ \underline{Ⅎ} t P$
66		nfcv	$⊢ \underline{Ⅎ} t U$
67	58 65 66	nfseq	$⊢ \underline{Ⅎ} t seq 1 (P, U)$
68		nfcv	$⊢ \underline{Ⅎ} t M$
69	67 68	nffv	$⊢ \underline{Ⅎ} t seq 1 (P, U) (M)$
70	7 69	nfcxfr	$⊢ \underline{Ⅎ} t X$
71	70	nfeq2	$⊢ Ⅎ t h = X$
72		fveq1	$⊢ h = X \to h (t) = X (t)$
73	72	breq2d	$⊢ h = X \to (0 \leq h (t) \leftrightarrow 0 \leq X (t))$
74	72	breq1d	$⊢ h = X \to (h (t) \leq 1 \leftrightarrow X (t) \leq 1)$
75	73 74	anbi12d	$⊢ h = X \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq X (t) \land X (t) \leq 1))$
76	71 75	ralbid	$⊢ h = X \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq X (t) \land X (t) \leq 1))$
77	47 48 57 76	elrabf	$⊢ X \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \leftrightarrow (X \in A \land \forall t \in T (0 \leq X (t) \land X (t) \leq 1))$
78	36 77	bitri	$⊢ X \in Y \leftrightarrow (X \in A \land \forall t \in T (0 \leq X (t) \land X (t) \leq 1))$
79	34 78	sylib	$⊢ φ \to (X \in A \land \forall t \in T (0 \leq X (t) \land X (t) \leq 1))$
80	79	simprd	$⊢ φ \to \forall t \in T (0 \leq X (t) \land X (t) \leq 1)$
81		nfv	$⊢ Ⅎ t i \in (1 \dots M)$
82	2 81	nfan	$⊢ Ⅎ t (φ \land i \in (1 \dots M))$
83	12	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to U (i) \in Y$
84		fveq1	$⊢ h = U (i) \to h (t) = U (i) (t)$
85	84	breq2d	$⊢ h = U (i) \to (0 \leq h (t) \leftrightarrow 0 \leq U (i) (t))$
86	84	breq1d	$⊢ h = U (i) \to (h (t) \leq 1 \leftrightarrow U (i) (t) \leq 1)$
87	85 86	anbi12d	$⊢ h = U (i) \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
88	87	ralbidv	$⊢ h = U (i) \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
89	88 5	elrab2	$⊢ U (i) \in Y \leftrightarrow (U (i) \in A \land \forall t \in T (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
90	89	simplbi	$⊢ U (i) \in Y \to U (i) \in A$
91	83 90	syl	$⊢ (φ \land i \in (1 \dots M)) \to U (i) \in A$
92		eleq1	$⊢ f = U (i) \to (f \in A \leftrightarrow U (i) \in A)$
93	92	anbi2d	$⊢ f = U (i) \to ((φ \land f \in A) \leftrightarrow (φ \land U (i) \in A))$
94		feq1	$⊢ f = U (i) \to (f : T ⟶ ℝ \leftrightarrow U (i) : T ⟶ ℝ)$
95	93 94	imbi12d	$⊢ f = U (i) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land U (i) \in A) \to U (i) : T ⟶ ℝ))$
96	20	a1i	$⊢ f \in A \to ((φ \land f \in A) \to f : T ⟶ ℝ)$
97	95 96	vtoclga	$⊢ U (i) \in A \to ((φ \land U (i) \in A) \to U (i) : T ⟶ ℝ)$
98	97	anabsi7	$⊢ (φ \land U (i) \in A) \to U (i) : T ⟶ ℝ$
99	91 98	syldan	$⊢ (φ \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
100	99	adantr	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to U (i) : T ⟶ ℝ$
101	11	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to W (i) \in V$
102		simpl	$⊢ (φ \land i \in (1 \dots M)) \to φ$
103	102 101	jca	$⊢ (φ \land i \in (1 \dots M)) \to (φ \land W (i) \in V)$
104	4	nfel2	$⊢ Ⅎ w W (i) \in V$
105	3 104	nfan	$⊢ Ⅎ w (φ \land W (i) \in V)$
106		nfv	$⊢ Ⅎ w W (i) \subseteq T$
107	105 106	nfim	$⊢ Ⅎ w ((φ \land W (i) \in V) \to W (i) \subseteq T)$
108		eleq1	$⊢ w = W (i) \to (w \in V \leftrightarrow W (i) \in V)$
109	108	anbi2d	$⊢ w = W (i) \to ((φ \land w \in V) \leftrightarrow (φ \land W (i) \in V))$
110		sseq1	$⊢ w = W (i) \to (w \subseteq T \leftrightarrow W (i) \subseteq T)$
111	109 110	imbi12d	$⊢ w = W (i) \to (((φ \land w \in V) \to w \subseteq T) \leftrightarrow ((φ \land W (i) \in V) \to W (i) \subseteq T))$
112	107 111 13	vtoclg1f	$⊢ W (i) \in V \to ((φ \land W (i) \in V) \to W (i) \subseteq T)$
113	101 103 112	sylc	$⊢ (φ \land i \in (1 \dots M)) \to W (i) \subseteq T$
114	113	sselda	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to t \in T$
115	100 114	ffvelcdmd	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to U (i) (t) \in ℝ$
116	22	rpred	$⊢ φ \to E \in ℝ$
117	116	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to E \in ℝ$
118	29	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to M \in ℝ$
119	10	nnne0d	$⊢ φ \to M \neq 0$
120	119	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to M \neq 0$
121	117 118 120	redivcld	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to \frac{E}{M} \in ℝ$
122	17	r19.21bi	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to U (i) (t) < \frac{E}{M}$
123		1red	$⊢ φ \to 1 \in ℝ$
124		0lt1	$⊢ 0 < 1$
125	124	a1i	$⊢ φ \to 0 < 1$
126	10	nngt0d	$⊢ φ \to 0 < M$
127	22	rpregt0d	$⊢ φ \to (E \in ℝ \land 0 < E)$
128		lediv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (M \in ℝ \land 0 < M) \land (E \in ℝ \land 0 < E)) \to (1 \leq M \leftrightarrow \frac{E}{M} \leq \frac{E}{1})$
129	123 125 29 126 127 128	syl221anc	$⊢ φ \to (1 \leq M \leftrightarrow \frac{E}{M} \leq \frac{E}{1})$
130	28 129	mpbid	$⊢ φ \to \frac{E}{M} \leq \frac{E}{1}$
131	22	rpcnd	$⊢ φ \to E \in ℂ$
132	131	div1d	$⊢ φ \to \frac{E}{1} = E$
133	130 132	breqtrd	$⊢ φ \to \frac{E}{M} \leq E$
134	133	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to \frac{E}{M} \leq E$
135	115 121 117 122 134	ltletrd	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to U (i) (t) < E$
136	135	ex	$⊢ (φ \land i \in (1 \dots M)) \to (t \in W (i) \to U (i) (t) < E)$
137	82 136	ralrimi	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in W (i) U (i) (t) < E$
138	1 2 5 6 7 8 9 10 11 12 14 15 137 21 20 19 22	stoweidlem48	$⊢ φ \to \forall t \in D X (t) < E$
139	25	sseli	$⊢ f \in Y \to f \in A$
140	139 20	sylan2	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
141	1 2 62 6 7 8 9 10 12 18 22 23 140 33 21 16	stoweidlem42	$⊢ φ \to \forall t \in B 1 - E < X (t)$
142	80 138 141	3jca	$⊢ φ \to (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in D X (t) < E \land \forall t \in B 1 - E < X (t))$
143	35 142	jca	$⊢ φ \to (X \in A \land (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in D X (t) < E \land \forall t \in B 1 - E < X (t)))$
144		eleq1	$⊢ x = X \to (x \in A \leftrightarrow X \in A)$
145	70	nfeq2	$⊢ Ⅎ t x = X$
146		fveq1	$⊢ x = X \to x (t) = X (t)$
147	146	breq2d	$⊢ x = X \to (0 \leq x (t) \leftrightarrow 0 \leq X (t))$
148	146	breq1d	$⊢ x = X \to (x (t) \leq 1 \leftrightarrow X (t) \leq 1)$
149	147 148	anbi12d	$⊢ x = X \to ((0 \leq x (t) \land x (t) \leq 1) \leftrightarrow (0 \leq X (t) \land X (t) \leq 1))$
150	145 149	ralbid	$⊢ x = X \to (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq X (t) \land X (t) \leq 1))$
151	146	breq1d	$⊢ x = X \to (x (t) < E \leftrightarrow X (t) < E)$
152	145 151	ralbid	$⊢ x = X \to (\forall t \in D x (t) < E \leftrightarrow \forall t \in D X (t) < E)$
153	146	breq2d	$⊢ x = X \to (1 - E < x (t) \leftrightarrow 1 - E < X (t))$
154	145 153	ralbid	$⊢ x = X \to (\forall t \in B 1 - E < x (t) \leftrightarrow \forall t \in B 1 - E < X (t))$
155	150 152 154	3anbi123d	$⊢ x = X \to ((\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t)) \leftrightarrow (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in D X (t) < E \land \forall t \in B 1 - E < X (t)))$
156	144 155	anbi12d	$⊢ x = X \to ((x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))) \leftrightarrow (X \in A \land (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in D X (t) < E \land \forall t \in B 1 - E < X (t))))$
157	156	spcegv	$⊢ X \in A \to ((X \in A \land (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in D X (t) < E \land \forall t \in B 1 - E < X (t))) \to \exists x (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))))$
158	35 143 157	sylc	$⊢ φ \to \exists x (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t)))$

Metamath Proof Explorer

Theorem stoweidlem51

Proof