# Metamath Proof Explorer

## Theorem stoweidlem49

Description: There exists a function q_n as in the proof of Lemma 1 in BrosowskiDeutsh p. 91 (at the top of page 91): 0 <= q_n <= 1 , q_n < ε on T \ U , and q_n > 1 - ε on V . Here y is used to represent the final q_n in the paper (the one with n large enough), N represents n in the paper, K represents k , D represents δ, E represents ε, and P represents p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem49.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{P}$
stoweidlem49.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem49.3 ${⊢}{V}=\left\{{t}\in {T}|{P}\left({t}\right)<\frac{{D}}{2}\right\}$
stoweidlem49.4 ${⊢}{\phi }\to {D}\in {ℝ}^{+}$
stoweidlem49.5 ${⊢}{\phi }\to {D}<1$
stoweidlem49.6 ${⊢}{\phi }\to {P}\in {A}$
stoweidlem49.7 ${⊢}{\phi }\to {P}:{T}⟶ℝ$
stoweidlem49.8 ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)$
stoweidlem49.9 ${⊢}{\phi }\to \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{D}\le {P}\left({t}\right)$
stoweidlem49.10 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
stoweidlem49.11 ${⊢}\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}$
stoweidlem49.12 ${⊢}\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}$
stoweidlem49.13 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
stoweidlem49.14 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
Assertion stoweidlem49 ${⊢}{\phi }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\wedge \forall {t}\in {V}\phantom{\rule{.4em}{0ex}}1-{E}<{y}\left({t}\right)\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<{E}\right)$

### Proof

Step Hyp Ref Expression
1 stoweidlem49.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{P}$
2 stoweidlem49.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
3 stoweidlem49.3 ${⊢}{V}=\left\{{t}\in {T}|{P}\left({t}\right)<\frac{{D}}{2}\right\}$
4 stoweidlem49.4 ${⊢}{\phi }\to {D}\in {ℝ}^{+}$
5 stoweidlem49.5 ${⊢}{\phi }\to {D}<1$
6 stoweidlem49.6 ${⊢}{\phi }\to {P}\in {A}$
7 stoweidlem49.7 ${⊢}{\phi }\to {P}:{T}⟶ℝ$
8 stoweidlem49.8 ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {P}\left({t}\right)\wedge {P}\left({t}\right)\le 1\right)$
9 stoweidlem49.9 ${⊢}{\phi }\to \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{D}\le {P}\left({t}\right)$
10 stoweidlem49.10 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
11 stoweidlem49.11 ${⊢}\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}$
12 stoweidlem49.12 ${⊢}\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}$
13 stoweidlem49.13 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
14 stoweidlem49.14 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
15 breq2 ${⊢}{j}={i}\to \left(\frac{1}{{D}}<{j}↔\frac{1}{{D}}<{i}\right)$
16 15 cbvrabv ${⊢}\left\{{j}\in ℕ|\frac{1}{{D}}<{j}\right\}=\left\{{i}\in ℕ|\frac{1}{{D}}<{i}\right\}$
17 16 4 5 stoweidlem14 ${⊢}{\phi }\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)$
18 eqid ${⊢}\left({i}\in {ℕ}_{0}⟼{\left(\frac{1}{{k}{D}}\right)}^{{i}}\right)=\left({i}\in {ℕ}_{0}⟼{\left(\frac{1}{{k}{D}}\right)}^{{i}}\right)$
19 eqid ${⊢}\left({i}\in {ℕ}_{0}⟼{\left(\frac{{k}{D}}{2}\right)}^{{i}}\right)=\left({i}\in {ℕ}_{0}⟼{\left(\frac{{k}{D}}{2}\right)}^{{i}}\right)$
20 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
21 20 adantl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}\in ℝ$
22 4 rpred ${⊢}{\phi }\to {D}\in ℝ$
23 22 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {D}\in ℝ$
24 21 23 remulcld ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}{D}\in ℝ$
25 24 adantr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\right)\to {k}{D}\in ℝ$
26 simprl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\right)\to 1<{k}{D}$
27 24 rehalfcld ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \frac{{k}{D}}{2}\in ℝ$
28 nngt0 ${⊢}{k}\in ℕ\to 0<{k}$
29 28 adantl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to 0<{k}$
30 4 rpgt0d ${⊢}{\phi }\to 0<{D}$
31 30 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to 0<{D}$
32 21 23 29 31 mulgt0d ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to 0<{k}{D}$
33 2re ${⊢}2\in ℝ$
34 2pos ${⊢}0<2$
35 33 34 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
36 35 a1i ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(2\in ℝ\wedge 0<2\right)$
37 divgt0 ${⊢}\left(\left({k}{D}\in ℝ\wedge 0<{k}{D}\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0<\frac{{k}{D}}{2}$
38 24 32 36 37 syl21anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to 0<\frac{{k}{D}}{2}$
39 27 38 elrpd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \frac{{k}{D}}{2}\in {ℝ}^{+}$
40 39 adantr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\right)\to \frac{{k}{D}}{2}\in {ℝ}^{+}$
41 simprr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\right)\to \frac{{k}{D}}{2}<1$
42 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\right)\to {E}\in {ℝ}^{+}$
43 18 19 25 26 40 41 42 stoweidlem7 ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)$
44 43 ex ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(\left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)$
45 44 reximdva ${⊢}{\phi }\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1<{k}{D}\wedge \frac{{k}{D}}{2}<1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)$
46 17 45 mpd ${⊢}{\phi }\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)$
47 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({k}\in ℕ\wedge {n}\in ℕ\right)$
48 2 47 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)$
49 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)$
50 48 49 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)$
51 eqid ${⊢}\left({t}\in {T}⟼{\left(1-{{P}\left({t}\right)}^{{n}}\right)}^{{{k}}^{{n}}}\right)=\left({t}\in {T}⟼{\left(1-{{P}\left({t}\right)}^{{n}}\right)}^{{{k}}^{{n}}}\right)$
52 simplrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {n}\in ℕ$
53 simplrl ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {k}\in ℕ$
54 4 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {D}\in {ℝ}^{+}$
55 5 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {D}<1$
56 6 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {P}\in {A}$
57 7 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {P}:{T}⟶ℝ$
58 8 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\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)$
59 9 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{D}\le {P}\left({t}\right)$
60 10 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
61 simp1ll ${⊢}\left(\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\wedge {f}\in {A}\wedge {g}\in {A}\right)\to {\phi }$
62 61 11 syld3an1 ${⊢}\left(\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\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 61 12 syld3an1 ${⊢}\left(\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\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 13 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
65 14 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to {E}\in {ℝ}^{+}$
66 simprl ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to 1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}$
67 simprr ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to \frac{1}{{{k}{D}}^{{n}}}<{E}$
68 1 50 3 51 52 53 54 55 56 57 58 59 60 62 63 64 65 66 67 stoweidlem45 ${⊢}\left(\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\wedge \left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\wedge \forall {t}\in {V}\phantom{\rule{.4em}{0ex}}1-{E}<{y}\left({t}\right)\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<{E}\right)$
69 68 ex ${⊢}\left({\phi }\wedge \left({k}\in ℕ\wedge {n}\in ℕ\right)\right)\to \left(\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\wedge \forall {t}\in {V}\phantom{\rule{.4em}{0ex}}1-{E}<{y}\left({t}\right)\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<{E}\right)\right)$
70 69 rexlimdvva ${⊢}{\phi }\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(1-{E}<1-{\left(\frac{{k}{D}}{2}\right)}^{{n}}\wedge \frac{1}{{{k}{D}}^{{n}}}<{E}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\wedge \forall {t}\in {V}\phantom{\rule{.4em}{0ex}}1-{E}<{y}\left({t}\right)\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<{E}\right)\right)$
71 46 70 mpd ${⊢}{\phi }\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\wedge \forall {t}\in {V}\phantom{\rule{.4em}{0ex}}1-{E}<{y}\left({t}\right)\wedge \forall {t}\in \left({T}\setminus {U}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<{E}\right)$