Metamath Proof Explorer

Theorem 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 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{U}$
stoweidlem56.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem56.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
stoweidlem56.4 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
stoweidlem56.5 ${⊢}{T}=\bigcup {J}$
stoweidlem56.6 ${⊢}{C}={J}\mathrm{Cn}{K}$
stoweidlem56.7 ${⊢}{\phi }\to {A}\subseteq {C}$
stoweidlem56.8 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
stoweidlem56.9 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
stoweidlem56.10 ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left({t}\in {T}⟼{y}\right)\in {A}$
stoweidlem56.11 ${⊢}\left({\phi }\wedge \left({r}\in {T}\wedge {t}\in {T}\wedge {r}\ne {t}\right)\right)\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\left({r}\right)\ne {q}\left({t}\right)$
stoweidlem56.12 ${⊢}{\phi }\to {U}\in {J}$
stoweidlem56.13 ${⊢}{\phi }\to {Z}\in {U}$
Assertion stoweidlem56 ${⊢}{\phi }\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({Z}\in {v}\wedge {v}\subseteq {U}\right)\wedge \forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({t}\right)\wedge {x}\left({t}\right)\le 1\right)\wedge \forall {t}\in {v}\phantom{\rule{.4em}{0ex}}{x}\left({t}\right)<{e}\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}1-{e}<{x}\left({t}\right)\right)\right)$

Proof

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