stoweidlem52

Description: There exists a neighborhood V as in Lemma 1 of BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem52.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem52.2	$⊢ Ⅎ t φ$
	stoweidlem52.3	$⊢ \underline{Ⅎ} t P$
	stoweidlem52.4	$⊢ K = topGen (ran (.))$
	stoweidlem52.5	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
	stoweidlem52.7	$⊢ T = ⋃ J$
	stoweidlem52.8	$⊢ C = J Cn K$
	stoweidlem52.9	$⊢ φ \to A \subseteq C$
	stoweidlem52.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem52.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem52.12	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
	stoweidlem52.13	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem52.14	$⊢ φ \to D < 1$
	stoweidlem52.15	$⊢ φ \to U \in J$
	stoweidlem52.16	$⊢ φ \to Z \in U$
	stoweidlem52.17	$⊢ φ \to P \in A$
	stoweidlem52.18	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
	stoweidlem52.19	$⊢ φ \to P (Z) = 0$
	stoweidlem52.20	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
Assertion	stoweidlem52	$⊢ φ \to \exists v \in J ((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem52.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem52.2	$⊢ Ⅎ t φ$
3		stoweidlem52.3	$⊢ \underline{Ⅎ} t P$
4		stoweidlem52.4	$⊢ K = topGen (ran (.))$
5		stoweidlem52.5	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
6		stoweidlem52.7	$⊢ T = ⋃ J$
7		stoweidlem52.8	$⊢ C = J Cn K$
8		stoweidlem52.9	$⊢ φ \to A \subseteq C$
9		stoweidlem52.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
10		stoweidlem52.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
11		stoweidlem52.12	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
12		stoweidlem52.13	$⊢ φ \to D \in ℝ^{+}$
13		stoweidlem52.14	$⊢ φ \to D < 1$
14		stoweidlem52.15	$⊢ φ \to U \in J$
15		stoweidlem52.16	$⊢ φ \to Z \in U$
16		stoweidlem52.17	$⊢ φ \to P \in A$
17		stoweidlem52.18	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
18		stoweidlem52.19	$⊢ φ \to P (Z) = 0$
19		stoweidlem52.20	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
20		nfcv	$⊢ \underline{Ⅎ} t (\frac{D}{2})$
21	12	rpred	$⊢ φ \to D \in ℝ$
22	21	rehalfcld	$⊢ φ \to \frac{D}{2} \in ℝ$
23	22	rexrd	$⊢ φ \to \frac{D}{2} \in ℝ^{*}$
24	8 7	sseqtrdi	$⊢ φ \to A \subseteq J Cn K$
25	24 16	sseldd	$⊢ φ \to P \in (J Cn K)$
26	20 3 2 4 6 5 23 25	rfcnpre2	$⊢ φ \to V \in J$
27		elssuni	$⊢ U \in J \to U \subseteq ⋃ J$
28	14 27	syl	$⊢ φ \to U \subseteq ⋃ J$
29	28 6	sseqtrrdi	$⊢ φ \to U \subseteq T$
30	29 15	sseldd	$⊢ φ \to Z \in T$
31		2re	$⊢ 2 \in ℝ$
32	31	a1i	$⊢ φ \to 2 \in ℝ$
33	12	rpgt0d	$⊢ φ \to 0 < D$
34		2pos	$⊢ 0 < 2$
35	34	a1i	$⊢ φ \to 0 < 2$
36	21 32 33 35	divgt0d	$⊢ φ \to 0 < \frac{D}{2}$
37	18 36	eqbrtrd	$⊢ φ \to P (Z) < \frac{D}{2}$
38		nfcv	$⊢ \underline{Ⅎ} t Z$
39		nfcv	$⊢ \underline{Ⅎ} t T$
40	3 38	nffv	$⊢ \underline{Ⅎ} t P (Z)$
41		nfcv	$⊢ \underline{Ⅎ} t <$
42	40 41 20	nfbr	$⊢ Ⅎ t P (Z) < \frac{D}{2}$
43		fveq2	$⊢ t = Z \to P (t) = P (Z)$
44	43	breq1d	$⊢ t = Z \to (P (t) < \frac{D}{2} \leftrightarrow P (Z) < \frac{D}{2})$
45	38 39 42 44	elrabf	$⊢ Z \in \{t \in T \| P (t) < \frac{D}{2}\} \leftrightarrow (Z \in T \land P (Z) < \frac{D}{2})$
46	30 37 45	sylanbrc	$⊢ φ \to Z \in \{t \in T \| P (t) < \frac{D}{2}\}$
47	46 5	eleqtrrdi	$⊢ φ \to Z \in V$
48		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| P (t) < \frac{D}{2}\}$
49	5 48	nfcxfr	$⊢ \underline{Ⅎ} t V$
50	8 16	sseldd	$⊢ φ \to P \in C$
51	4 6 7 50	fcnre	$⊢ φ \to P : T ⟶ ℝ$
52	51	adantr	$⊢ (φ \land t \in V) \to P : T ⟶ ℝ$
53	5	reqabi	$⊢ t \in V \leftrightarrow (t \in T \land P (t) < \frac{D}{2})$
54	53	bilani	$⊢ (φ \land t \in V) \to (t \in T \land P (t) < \frac{D}{2})$
55	54	simpld	$⊢ (φ \land t \in V) \to t \in T$
56	52 55	ffvelcdmd	$⊢ (φ \land t \in V) \to P (t) \in ℝ$
57	22	adantr	$⊢ (φ \land t \in V) \to \frac{D}{2} \in ℝ$
58	21	adantr	$⊢ (φ \land t \in V) \to D \in ℝ$
59	54	simprd	$⊢ (φ \land t \in V) \to P (t) < \frac{D}{2}$
60		halfpos	$⊢ D \in ℝ \to (0 < D \leftrightarrow \frac{D}{2} < D)$
61	21 60	syl	$⊢ φ \to (0 < D \leftrightarrow \frac{D}{2} < D)$
62	33 61	mpbid	$⊢ φ \to \frac{D}{2} < D$
63	62	adantr	$⊢ (φ \land t \in V) \to \frac{D}{2} < D$
64	56 57 58 59 63	lttrd	$⊢ (φ \land t \in V) \to P (t) < D$
65	64	adantr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to P (t) < D$
66	21	ad2antrr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to D \in ℝ$
67	56	adantr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to P (t) \in ℝ$
68	19	ad2antrr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to \forall t \in (T ∖ U) D \leq P (t)$
69	55	anim1i	$⊢ ((φ \land t \in V) \land \neg t \in U) \to (t \in T \land \neg t \in U)$
70		eldif	$⊢ t \in (T ∖ U) \leftrightarrow (t \in T \land \neg t \in U)$
71	69 70	sylibr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to t \in (T ∖ U)$
72		rsp	$⊢ \forall t \in (T ∖ U) D \leq P (t) \to (t \in (T ∖ U) \to D \leq P (t))$
73	68 71 72	sylc	$⊢ ((φ \land t \in V) \land \neg t \in U) \to D \leq P (t)$
74	66 67 73	lensymd	$⊢ ((φ \land t \in V) \land \neg t \in U) \to \neg P (t) < D$
75	65 74	condan	$⊢ (φ \land t \in V) \to t \in U$
76	75	ex	$⊢ φ \to (t \in V \to t \in U)$
77	2 49 1 76	ssrd	$⊢ φ \to V \subseteq U$
78		nfv	$⊢ Ⅎ t e \in ℝ^{+}$
79	2 78	nfan	$⊢ Ⅎ t (φ \land e \in ℝ^{+})$
80		nfv	$⊢ Ⅎ t y \in A$
81	79 80	nfan	$⊢ Ⅎ t ((φ \land e \in ℝ^{+}) \land y \in A)$
82		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
83		nfra1	$⊢ Ⅎ t \forall t \in V 1 - e < y (t)$
84		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) y (t) < e$
85	82 83 84	nf3an	$⊢ Ⅎ t (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)$
86	81 85	nfan	$⊢ Ⅎ t (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e))$
87		eqid	$⊢ (t \in T ⟼ 1 - y (t)) = (t \in T ⟼ 1 - y (t))$
88		eqid	$⊢ (t \in T ⟼ 1) = (t \in T ⟼ 1)$
89		ssrab2	$⊢ \{t \in T \| P (t) < \frac{D}{2}\} \subseteq T$
90	5 89	eqsstri	$⊢ V \subseteq T$
91		simplr	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to y \in A$
92		simplll	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to φ$
93	8	sselda	$⊢ (φ \land y \in A) \to y \in C$
94	4 6 7 93	fcnre	$⊢ (φ \land y \in A) \to y : T ⟶ ℝ$
95	92 91 94	syl2anc	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to y : T ⟶ ℝ$
96	8	sselda	$⊢ (φ \land f \in A) \to f \in C$
97	4 6 7 96	fcnre	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
98	92 97	sylan	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land f \in A) \to f : T ⟶ ℝ$
99	92 9	syl3an1	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
100	92 10	syl3an1	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
101	92 11	sylan	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
102		simpllr	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to e \in ℝ^{+}$
103		simpr1	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
104		simpr2	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \forall t \in V 1 - e < y (t)$
105		simpr3	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \forall t \in (T ∖ U) y (t) < e$
106	86 87 88 90 91 95 98 99 100 101 102 103 104 105	stoweidlem41	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))$
107	12	adantr	$⊢ (φ \land e \in ℝ^{+}) \to D \in ℝ^{+}$
108	13	adantr	$⊢ (φ \land e \in ℝ^{+}) \to D < 1$
109	16	adantr	$⊢ (φ \land e \in ℝ^{+}) \to P \in A$
110	51	adantr	$⊢ (φ \land e \in ℝ^{+}) \to P : T ⟶ ℝ$
111	17	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
112	19	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \forall t \in (T ∖ U) D \leq P (t)$
113	97	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land f \in A) \to f : T ⟶ ℝ$
114	9	3adant1r	$⊢ ((φ \land e \in ℝ^{+}) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
115	10	3adant1r	$⊢ ((φ \land e \in ℝ^{+}) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
116	11	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
117		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
118	3 79 5 107 108 109 110 111 112 113 114 115 116 117	stoweidlem49	$⊢ (φ \land e \in ℝ^{+}) \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)$
119	106 118	r19.29a	$⊢ (φ \land e \in ℝ^{+}) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))$
120	119	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))$
121	47 77 120	jca31	$⊢ φ \to ((Z \in V \land V \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
122		eleq2	$⊢ v = V \to (Z \in v \leftrightarrow Z \in V)$
123		sseq1	$⊢ v = V \to (v \subseteq U \leftrightarrow V \subseteq U)$
124	122 123	anbi12d	$⊢ v = V \to ((Z \in v \land v \subseteq U) \leftrightarrow (Z \in V \land V \subseteq U))$
125		nfcv	$⊢ \underline{Ⅎ} t v$
126	125 49	raleqf	$⊢ v = V \to (\forall t \in v x (t) < e \leftrightarrow \forall t \in V x (t) < e)$
127	126	3anbi2d	$⊢ v = V \to ((\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)) \leftrightarrow (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
128	127	rexbidv	$⊢ v = V \to (\exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)) \leftrightarrow \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
129	128	ralbidv	$⊢ v = V \to (\forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)) \leftrightarrow \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
130	124 129	anbi12d	$⊢ v = V \to (((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))) \leftrightarrow ((Z \in V \land V \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))))$
131	130	rspcev	$⊢ (V \in J \land ((Z \in V \land V \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))) \to \exists v \in J ((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
132	26 121 131	syl2anc	$⊢ φ \to \exists v \in J ((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$

Metamath Proof Explorer

Theorem stoweidlem52

Proof