stoweidlem56

Description: This theorem proves Lemma 1 in BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, v is used to represent V in the paper, and e is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem56.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem56.2	$⊢ Ⅎ t φ$
	stoweidlem56.3	$⊢ K = topGen (ran (.))$
	stoweidlem56.4	$⊢ φ \to J \in Comp$
	stoweidlem56.5	$⊢ T = ⋃ J$
	stoweidlem56.6	$⊢ C = J Cn K$
	stoweidlem56.7	$⊢ φ \to A \subseteq C$
	stoweidlem56.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem56.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem56.10	$⊢ (φ \land y \in ℝ) \to (t \in T ⟼ y) \in A$
	stoweidlem56.11	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem56.12	$⊢ φ \to U \in J$
	stoweidlem56.13	$⊢ φ \to Z \in U$
Assertion	stoweidlem56	$⊢ φ \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		stoweidlem56.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem56.2	$⊢ Ⅎ t φ$
3		stoweidlem56.3	$⊢ K = topGen (ran (.))$
4		stoweidlem56.4	$⊢ φ \to J \in Comp$
5		stoweidlem56.5	$⊢ T = ⋃ J$
6		stoweidlem56.6	$⊢ C = J Cn K$
7		stoweidlem56.7	$⊢ φ \to A \subseteq C$
8		stoweidlem56.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweidlem56.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
10		stoweidlem56.10	$⊢ (φ \land y \in ℝ) \to (t \in T ⟼ y) \in A$
11		stoweidlem56.11	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
12		stoweidlem56.12	$⊢ φ \to U \in J$
13		stoweidlem56.13	$⊢ φ \to Z \in U$
14		eqid	$⊢ \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\} = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
15		eqid	$⊢ \{w \in J \| \exists h \in \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\} w = \{t \in T \| 0 < h (t)\}\} = \{w \in J \| \exists h \in \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\} w = \{t \in T \| 0 < h (t)\}\}$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	stoweidlem55	$⊢ φ \to \exists p \in A (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))$
17		df-rex	$⊢ \exists p \in A (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)) \leftrightarrow \exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))$
18	16 17	sylib	$⊢ φ \to \exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))$
19		simpl	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to φ$
20		simprl	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to p \in A$
21		simprr3	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to \forall t \in (T ∖ U) 0 < p (t)$
22		nfv	$⊢ Ⅎ t p \in A$
23		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) 0 < p (t)$
24	2 22 23	nf3an	$⊢ Ⅎ t (φ \land p \in A \land \forall t \in (T ∖ U) 0 < p (t))$
25	4	3ad2ant1	$⊢ (φ \land p \in A \land \forall t \in (T ∖ U) 0 < p (t)) \to J \in Comp$
26	7	sselda	$⊢ (φ \land p \in A) \to p \in C$
27	26 6	eleqtrdi	$⊢ (φ \land p \in A) \to p \in (J Cn K)$
28	27	3adant3	$⊢ (φ \land p \in A \land \forall t \in (T ∖ U) 0 < p (t)) \to p \in (J Cn K)$
29		simp3	$⊢ (φ \land p \in A \land \forall t \in (T ∖ U) 0 < p (t)) \to \forall t \in (T ∖ U) 0 < p (t)$
30	12	3ad2ant1	$⊢ (φ \land p \in A \land \forall t \in (T ∖ U) 0 < p (t)) \to U \in J$
31	1 24 3 5 25 28 29 30	stoweidlem28	$⊢ (φ \land p \in A \land \forall t \in (T ∖ U) 0 < p (t)) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))$
32	19 20 21 31	syl3anc	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))$
33		simpr1	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to d \in ℝ^{+}$
34		simpr2	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to d < 1$
35		simplrl	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to p \in A$
36		simprr1	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to \forall t \in T (0 \leq p (t) \land p (t) \leq 1)$
37	36	adantr	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to \forall t \in T (0 \leq p (t) \land p (t) \leq 1)$
38		simprr2	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to p (Z) = 0$
39	38	adantr	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to p (Z) = 0$
40		simpr3	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to \forall t \in (T ∖ U) d \leq p (t)$
41	37 39 40	3jca	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))$
42	35 41	jca	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))$
43	33 34 42	3jca	$⊢ ((φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \land (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t))) \to (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))$
44	43	ex	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to ((d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t)) \to (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))))$
45	44	eximdv	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to (\exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq p (t)) \to \exists d (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))))$
46	32 45	mpd	$⊢ (φ \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))) \to \exists d (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))$
47	46	ex	$⊢ φ \to ((p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))) \to \exists d (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))))$
48	47	eximdv	$⊢ φ \to (\exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))) \to \exists p \exists d (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))))$
49	18 48	mpd	$⊢ φ \to \exists p \exists d (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))$
50		nfv	$⊢ Ⅎ t d \in ℝ^{+}$
51		nfv	$⊢ Ⅎ t d < 1$
52		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq p (t) \land p (t) \leq 1)$
53		nfv	$⊢ Ⅎ t p (Z) = 0$
54		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) d \leq p (t)$
55	52 53 54	nf3an	$⊢ Ⅎ t (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))$
56	22 55	nfan	$⊢ Ⅎ t (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))$
57	50 51 56	nf3an	$⊢ Ⅎ t (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))$
58	2 57	nfan	$⊢ Ⅎ t (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))))$
59		nfcv	$⊢ \underline{Ⅎ} t p$
60		eqid	$⊢ \{t \in T \| p (t) < \frac{d}{2}\} = \{t \in T \| p (t) < \frac{d}{2}\}$
61	7	adantr	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to A \subseteq C$
62	8	3adant1r	$⊢ ((φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
63	9	3adant1r	$⊢ ((φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
64	10	adantlr	$⊢ ((φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \land y \in ℝ) \to (t \in T ⟼ y) \in A$
65		simpr1	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to d \in ℝ^{+}$
66		simpr2	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to d < 1$
67	12	adantr	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to U \in J$
68	13	adantr	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to Z \in U$
69		simpr3l	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to p \in A$
70		simp3r1	$⊢ (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))) \to \forall t \in T (0 \leq p (t) \land p (t) \leq 1)$
71	70	adantl	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to \forall t \in T (0 \leq p (t) \land p (t) \leq 1)$
72		simp3r2	$⊢ (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))) \to p (Z) = 0$
73	72	adantl	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to p (Z) = 0$
74		simp3r3	$⊢ (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t)))) \to \forall t \in (T ∖ U) d \leq p (t)$
75	74	adantl	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (t))))) \to \forall t \in (T ∖ U) d \leq p (t)$
76	1 58 59 3 60 5 6 61 62 63 64 65 66 67 68 69 71 73 75	stoweidlem52	$⊢ (φ \land (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (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)))$
77	76	ex	$⊢ φ \to ((d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (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))))$
78	77	exlimdvv	$⊢ φ \to (\exists p \exists d (d \in ℝ^{+} \land d < 1 \land (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) d \leq p (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))))$
79	49 78	mpd	$⊢ φ \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 stoweidlem56

Proof