# Metamath Proof Explorer

## Theorem stoweidlem61

Description: This lemma proves that there exists a function g as in the proof in BrosowskiDeutsh p. 92: g is in the subalgebra, and for all t in T , abs( f(t) - g(t) ) < 2*ε. Here F is used to represent f in the paper, and E is used to represent ε. For this lemma there's the further assumption that the function F to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem61.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{F}$
stoweidlem61.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem61.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
stoweidlem61.4 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
stoweidlem61.5 ${⊢}{T}=\bigcup {J}$
stoweidlem61.6 ${⊢}{\phi }\to {T}\ne \varnothing$
stoweidlem61.7 ${⊢}{C}={J}\mathrm{Cn}{K}$
stoweidlem61.8 ${⊢}{\phi }\to {A}\subseteq {C}$
stoweidlem61.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}$
stoweidlem61.10 ${⊢}\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}$
stoweidlem61.11 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
stoweidlem61.12 ${⊢}\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)$
stoweidlem61.13 ${⊢}{\phi }\to {F}\in {C}$
stoweidlem61.14 ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {F}\left({t}\right)$
stoweidlem61.15 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
stoweidlem61.16 ${⊢}{\phi }\to {E}<\frac{1}{3}$
Assertion stoweidlem61 ${⊢}{\phi }\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}$

### Proof

Step Hyp Ref Expression
1 stoweidlem61.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{F}$
2 stoweidlem61.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
3 stoweidlem61.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 stoweidlem61.4 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
5 stoweidlem61.5 ${⊢}{T}=\bigcup {J}$
6 stoweidlem61.6 ${⊢}{\phi }\to {T}\ne \varnothing$
7 stoweidlem61.7 ${⊢}{C}={J}\mathrm{Cn}{K}$
8 stoweidlem61.8 ${⊢}{\phi }\to {A}\subseteq {C}$
9 stoweidlem61.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 stoweidlem61.10 ${⊢}\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}$
11 stoweidlem61.11 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
12 stoweidlem61.12 ${⊢}\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)$
13 stoweidlem61.13 ${⊢}{\phi }\to {F}\in {C}$
14 stoweidlem61.14 ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {F}\left({t}\right)$
15 stoweidlem61.15 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
16 stoweidlem61.16 ${⊢}{\phi }\to {E}<\frac{1}{3}$
17 eqid ${⊢}\left({j}\in \left(0\dots {n}\right)⟼\left\{{t}\in {T}|{F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right\}\right)=\left({j}\in \left(0\dots {n}\right)⟼\left\{{t}\in {T}|{F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right\}\right)$
18 eqid ${⊢}\left({j}\in \left(0\dots {n}\right)⟼\left\{{t}\in {T}|\left({j}+\left(\frac{1}{3}\right)\right){E}\le {F}\left({t}\right)\right\}\right)=\left({j}\in \left(0\dots {n}\right)⟼\left\{{t}\in {T}|\left({j}+\left(\frac{1}{3}\right)\right){E}\le {F}\left({t}\right)\right\}\right)$
19 1 2 3 5 7 17 18 4 6 8 9 10 11 12 13 14 15 16 stoweidlem60 ${⊢}{\phi }\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)$
20 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{g}\in {A}$
21 2 20 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {g}\in {A}\right)$
22 15 ad2antrr ${⊢}\left(\left({\phi }\wedge {g}\in {A}\right)\wedge {t}\in {T}\right)\to {E}\in {ℝ}^{+}$
23 3 5 7 13 fcnre ${⊢}{\phi }\to {F}:{T}⟶ℝ$
24 23 ffvelrnda ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {F}\left({t}\right)\in ℝ$
25 24 adantlr ${⊢}\left(\left({\phi }\wedge {g}\in {A}\right)\wedge {t}\in {T}\right)\to {F}\left({t}\right)\in ℝ$
26 8 sselda ${⊢}\left({\phi }\wedge {g}\in {A}\right)\to {g}\in {C}$
27 3 5 7 26 fcnre ${⊢}\left({\phi }\wedge {g}\in {A}\right)\to {g}:{T}⟶ℝ$
28 27 ffvelrnda ${⊢}\left(\left({\phi }\wedge {g}\in {A}\right)\wedge {t}\in {T}\right)\to {g}\left({t}\right)\in ℝ$
29 simpll1 ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to {E}\in {ℝ}^{+}$
30 simpll2 ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to {F}\left({t}\right)\in ℝ$
31 simpll3 ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to {g}\left({t}\right)\in ℝ$
32 simplr ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to {j}\in ℝ$
33 simprll ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to \left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)$
34 simprlr ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}$
35 simprrr ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)$
36 simprrl ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to {g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}$
37 29 30 31 32 33 34 35 36 stoweidlem13 ${⊢}\left(\left(\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\wedge {j}\in ℝ\right)\wedge \left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\right)\to \left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}$
38 37 rexlimdva2 ${⊢}\left({E}\in {ℝ}^{+}\wedge {F}\left({t}\right)\in ℝ\wedge {g}\left({t}\right)\in ℝ\right)\to \left(\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\to \left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}\right)$
39 22 25 28 38 syl3anc ${⊢}\left(\left({\phi }\wedge {g}\in {A}\right)\wedge {t}\in {T}\right)\to \left(\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\to \left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}\right)$
40 21 39 ralimdaa ${⊢}\left({\phi }\wedge {g}\in {A}\right)\to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}\right)$
41 40 reximdva ${⊢}{\phi }\to \left(\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{F}\left({t}\right)\wedge {F}\left({t}\right)\le \left({j}-\left(\frac{1}{3}\right)\right){E}\right)\wedge \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)\right)\right)\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}\right)$
42 19 41 mpd ${⊢}{\phi }\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left|{g}\left({t}\right)-{F}\left({t}\right)\right|<2{E}$