# Metamath Proof Explorer

## Theorem stoweidlem60

Description: This lemma proves that there exists a function g as in the proof in BrosowskiDeutsh p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all t in T , there is a j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here F is used to represent f in the paper, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

### Proof

Step Hyp Ref Expression
1 stoweidlem60.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{F}$
2 stoweidlem60.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
3 stoweidlem60.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 stoweidlem60.4 ${⊢}{T}=\bigcup {J}$
5 stoweidlem60.5 ${⊢}{C}={J}\mathrm{Cn}{K}$
6 stoweidlem60.6 ${⊢}{D}=\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)$
7 stoweidlem60.7 ${⊢}{B}=\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)$
8 stoweidlem60.8 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
9 stoweidlem60.9 ${⊢}{\phi }\to {T}\ne \varnothing$
10 stoweidlem60.10 ${⊢}{\phi }\to {A}\subseteq {C}$
11 stoweidlem60.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 stoweidlem60.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 stoweidlem60.13 ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left({t}\in {T}⟼{y}\right)\in {A}$
14 stoweidlem60.14 ${⊢}\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)$
15 stoweidlem60.15 ${⊢}{\phi }\to {F}\in {C}$
16 stoweidlem60.16 ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {F}\left({t}\right)$
17 stoweidlem60.17 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
18 stoweidlem60.18 ${⊢}{\phi }\to {E}<\frac{1}{3}$
19 nnre ${⊢}{m}\in ℕ\to {m}\in ℝ$
20 19 adantl ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {m}\in ℝ$
21 17 rpred ${⊢}{\phi }\to {E}\in ℝ$
22 21 adantr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {E}\in ℝ$
23 17 rpne0d ${⊢}{\phi }\to {E}\ne 0$
24 23 adantr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {E}\ne 0$
25 20 22 24 redivcld ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \frac{{m}}{{E}}\in ℝ$
26 1red ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to 1\in ℝ$
27 25 26 readdcld ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \left(\frac{{m}}{{E}}\right)+1\in ℝ$
28 27 adantr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\to \left(\frac{{m}}{{E}}\right)+1\in ℝ$
29 arch ${⊢}\left(\frac{{m}}{{E}}\right)+1\in ℝ\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{m}}{{E}}\right)+1<{n}$
30 28 29 syl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{m}}{{E}}\right)+1<{n}$
31 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{m}\in ℕ$
32 2 31 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {m}\in ℕ\right)$
33 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}$
34 32 33 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)$
35 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{n}\in ℕ$
36 34 35 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)$
37 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\frac{{m}}{{E}}\right)+1<{n}$
38 36 37 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)$
39 simp-5l ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {\phi }$
40 3 4 5 15 fcnre ${⊢}{\phi }\to {F}:{T}⟶ℝ$
41 40 ffvelrnda ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {F}\left({t}\right)\in ℝ$
42 39 41 sylancom ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {F}\left({t}\right)\in ℝ$
43 simp-5r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {m}\in ℕ$
44 43 nnred ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {m}\in ℝ$
45 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {n}\in ℕ$
46 45 nnred ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {n}\in ℝ$
47 1red ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to 1\in ℝ$
48 46 47 resubcld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {n}-1\in ℝ$
49 39 21 syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {E}\in ℝ$
50 48 49 remulcld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to \left({n}-1\right){E}\in ℝ$
51 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}$
52 51 r19.21bi ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {F}\left({t}\right)<{m}$
53 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to \left(\frac{{m}}{{E}}\right)+1<{n}$
54 simpr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \left(\frac{{m}}{{E}}\right)+1<{n}$
55 simpl1 ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {\phi }$
56 simpl2 ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {m}\in ℕ$
57 55 56 25 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \frac{{m}}{{E}}\in ℝ$
58 1red ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to 1\in ℝ$
59 simpl3 ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {n}\in ℕ$
60 59 nnred ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {n}\in ℝ$
61 57 58 60 ltaddsubd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \left(\left(\frac{{m}}{{E}}\right)+1<{n}↔\frac{{m}}{{E}}<{n}-1\right)$
62 54 61 mpbid ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \frac{{m}}{{E}}<{n}-1$
63 19 3ad2ant2 ${⊢}\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\to {m}\in ℝ$
64 63 adantr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {m}\in ℝ$
65 60 58 resubcld ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {n}-1\in ℝ$
66 21 3ad2ant1 ${⊢}\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\to {E}\in ℝ$
67 66 adantr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {E}\in ℝ$
68 17 rpgt0d ${⊢}{\phi }\to 0<{E}$
69 55 68 syl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to 0<{E}$
70 ltdivmul2 ${⊢}\left({m}\in ℝ\wedge {n}-1\in ℝ\wedge \left({E}\in ℝ\wedge 0<{E}\right)\right)\to \left(\frac{{m}}{{E}}<{n}-1↔{m}<\left({n}-1\right){E}\right)$
71 64 65 67 69 70 syl112anc ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \left(\frac{{m}}{{E}}<{n}-1↔{m}<\left({n}-1\right){E}\right)$
72 62 71 mpbid ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to {m}<\left({n}-1\right){E}$
73 39 43 45 53 72 syl31anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {m}<\left({n}-1\right){E}$
74 42 44 50 52 73 lttrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\wedge {t}\in {T}\right)\to {F}\left({t}\right)<\left({n}-1\right){E}$
75 74 ex ${⊢}\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \left({t}\in {T}\to {F}\left({t}\right)<\left({n}-1\right){E}\right)$
76 38 75 ralrimi ${⊢}\left(\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\wedge \left(\frac{{m}}{{E}}\right)+1<{n}\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}$
77 76 ex ${⊢}\left(\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\wedge {n}\in ℕ\right)\to \left(\left(\frac{{m}}{{E}}\right)+1<{n}\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
78 77 reximdva ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{m}}{{E}}\right)+1<{n}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
79 30 78 mpd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}$
80 1 2 3 8 4 9 5 15 rfcnnnub ${⊢}{\phi }\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<{m}$
81 79 80 r19.29a ${⊢}{\phi }\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}$
82 df-rex ${⊢}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}↔\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
83 81 82 sylib ${⊢}{\phi }\to \exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
84 simpr ${⊢}\left({\phi }\wedge \left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\right)\to \left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
85 2 35 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in ℕ\right)$
86 eqid ${⊢}\left\{{y}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\right\}=\left\{{y}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\right\}$
87 eqid ${⊢}\left({j}\in \left(0\dots {n}\right)⟼\left\{{y}\in \left\{{y}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\right\}|\left(\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{y}\left({t}\right)\right)\right\}\right)=\left({j}\in \left(0\dots {n}\right)⟼\left\{{y}\in \left\{{y}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {y}\left({t}\right)\wedge {y}\left({t}\right)\le 1\right)\right\}|\left(\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{y}\left({t}\right)\right)\right\}\right)$
88 8 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {J}\in \mathrm{Comp}$
89 10 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq {C}$
90 11 3adant1r ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\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}$
91 12 3adant1r ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\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}$
92 13 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in ℝ\right)\to \left({t}\in {T}⟼{y}\right)\in {A}$
93 14 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\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)$
94 15 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\in {C}$
95 17 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\in {ℝ}^{+}$
96 18 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}<\frac{1}{3}$
97 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
98 1 85 3 4 5 6 7 86 87 88 89 90 91 92 93 94 95 96 97 stoweidlem59 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)$
99 98 adantrr ${⊢}\left({\phi }\wedge \left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)$
100 19.42v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge \left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)↔\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
101 84 99 100 sylanbrc ${⊢}\left({\phi }\wedge \left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge \left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
102 3anass ${⊢}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)↔\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge \left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
103 102 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge \left({x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
104 101 103 sylibr ${⊢}\left({\phi }\wedge \left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)$
105 104 ex ${⊢}{\phi }\to \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
106 105 eximdv ${⊢}{\phi }\to \left(\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\to \exists {n}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
107 83 106 mpd ${⊢}{\phi }\to \exists {n}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)$
108 simpl ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {\phi }$
109 simpr1l ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {n}\in ℕ$
110 simpr2 ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {x}:\left(0\dots {n}\right)⟶{A}$
111 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{x}:\left(0\dots {n}\right)⟶{A}$
112 2 35 111 nf3an ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)$
113 simp2 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\to {n}\in ℕ$
114 simp3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\to {x}:\left(0\dots {n}\right)⟶{A}$
115 simp1 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\to {\phi }$
116 115 11 syl3an1 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\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}$
117 115 12 syl3an1 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\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}$
118 13 3ad2antl1 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\wedge {y}\in ℝ\right)\to \left({t}\in {T}⟼{y}\right)\in {A}$
119 17 3ad2ant1 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\to {E}\in {ℝ}^{+}$
120 119 rpred ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\to {E}\in ℝ$
121 10 sselda ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}\in {C}$
122 3 4 5 121 fcnre ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
123 122 3ad2antl1 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
124 112 113 114 116 117 118 120 123 stoweidlem17 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {x}:\left(0\dots {n}\right)⟶{A}\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\in {A}$
125 108 109 110 124 syl3anc ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\in {A}$
126 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
127 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
128 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{x}:\left(0\dots {n}\right)⟶{A}$
129 nfra1 ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
130 127 128 129 nf3an ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)$
131 126 130 nfan ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
132 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}$
133 35 132 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)$
134 nfcv ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}\left(0\dots {n}\right)$
135 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)$
136 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}$
137 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)$
138 135 136 137 nf3an ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
139 134 138 nfralw ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
140 133 111 139 nf3an ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)$
141 2 140 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)$
142 eqid ${⊢}\left({t}\in {T}⟼\left\{{j}\in \left(1\dots {n}\right)|{t}\in {D}\left({j}\right)\right\}\right)=\left({t}\in {T}⟼\left\{{j}\in \left(1\dots {n}\right)|{t}\in {D}\left({j}\right)\right\}\right)$
143 8 uniexd ${⊢}{\phi }\to \bigcup {J}\in \mathrm{V}$
144 4 143 eqeltrid ${⊢}{\phi }\to {T}\in \mathrm{V}$
145 144 adantr ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {T}\in \mathrm{V}$
146 40 adantr ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {F}:{T}⟶ℝ$
147 16 r19.21bi ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to 0\le {F}\left({t}\right)$
148 147 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {t}\in {T}\right)\to 0\le {F}\left({t}\right)$
149 simpr1r ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}$
150 149 r19.21bi ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {t}\in {T}\right)\to {F}\left({t}\right)<\left({n}-1\right){E}$
151 17 adantr ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {E}\in {ℝ}^{+}$
152 18 adantr ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to {E}<\frac{1}{3}$
153 simpll ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\right)\to {\phi }$
154 simplr2 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\right)\to {x}:\left(0\dots {n}\right)⟶{A}$
155 simpr ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\right)\to {j}\in \left(0\dots {n}\right)$
156 simp1 ${⊢}\left({\phi }\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge {j}\in \left(0\dots {n}\right)\right)\to {\phi }$
157 ffvelrn ${⊢}\left({x}:\left(0\dots {n}\right)⟶{A}\wedge {j}\in \left(0\dots {n}\right)\right)\to {x}\left({j}\right)\in {A}$
158 157 3adant1 ${⊢}\left({\phi }\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge {j}\in \left(0\dots {n}\right)\right)\to {x}\left({j}\right)\in {A}$
159 10 sselda ${⊢}\left({\phi }\wedge {x}\left({j}\right)\in {A}\right)\to {x}\left({j}\right)\in {C}$
160 3 4 5 159 fcnre ${⊢}\left({\phi }\wedge {x}\left({j}\right)\in {A}\right)\to {x}\left({j}\right):{T}⟶ℝ$
161 156 158 160 syl2anc ${⊢}\left({\phi }\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge {j}\in \left(0\dots {n}\right)\right)\to {x}\left({j}\right):{T}⟶ℝ$
162 153 154 155 161 syl3anc ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\right)\to {x}\left({j}\right):{T}⟶ℝ$
163 simp1r3 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
164 r19.26-3 ${⊢}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)↔\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
165 164 simp1bi ${⊢}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)$
166 simpl ${⊢}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\to 0\le {x}\left({j}\right)\left({t}\right)$
167 166 2ralimi ${⊢}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {x}\left({j}\right)\left({t}\right)$
168 163 165 167 3syl ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {x}\left({j}\right)\left({t}\right)$
169 simp2 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to {j}\in \left(0\dots {n}\right)$
170 simp3 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to {t}\in {T}$
171 rspa ${⊢}\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {x}\left({j}\right)\left({t}\right)\wedge {j}\in \left(0\dots {n}\right)\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {x}\left({j}\right)\left({t}\right)$
172 171 r19.21bi ${⊢}\left(\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}0\le {x}\left({j}\right)\left({t}\right)\wedge {j}\in \left(0\dots {n}\right)\right)\wedge {t}\in {T}\right)\to 0\le {x}\left({j}\right)\left({t}\right)$
173 168 169 170 172 syl21anc ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to 0\le {x}\left({j}\right)\left({t}\right)$
174 simpr ${⊢}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\to {x}\left({j}\right)\left({t}\right)\le 1$
175 174 2ralimi ${⊢}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)\le 1$
176 163 165 175 3syl ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)\le 1$
177 rspa ${⊢}\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)\le 1\wedge {j}\in \left(0\dots {n}\right)\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)\le 1$
178 177 r19.21bi ${⊢}\left(\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)\le 1\wedge {j}\in \left(0\dots {n}\right)\right)\wedge {t}\in {T}\right)\to {x}\left({j}\right)\left({t}\right)\le 1$
179 176 169 170 178 syl21anc ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {T}\right)\to {x}\left({j}\right)\left({t}\right)\le 1$
180 simp1r3 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {D}\left({j}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
181 164 simp2bi ${⊢}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}$
182 180 181 syl ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {D}\left({j}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}$
183 simp2 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {D}\left({j}\right)\right)\to {j}\in \left(0\dots {n}\right)$
184 simp3 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {D}\left({j}\right)\right)\to {t}\in {D}\left({j}\right)$
185 rspa ${⊢}\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge {j}\in \left(0\dots {n}\right)\right)\to \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}$
186 185 r19.21bi ${⊢}\left(\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge {j}\in \left(0\dots {n}\right)\right)\wedge {t}\in {D}\left({j}\right)\right)\to {x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}$
187 182 183 184 186 syl21anc ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {D}\left({j}\right)\right)\to {x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}$
188 simp1r3 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {B}\left({j}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)$
189 164 simp3bi ${⊢}\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)$
190 188 189 syl ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {B}\left({j}\right)\right)\to \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)$
191 simp2 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {B}\left({j}\right)\right)\to {j}\in \left(0\dots {n}\right)$
192 simp3 ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {B}\left({j}\right)\right)\to {t}\in {B}\left({j}\right)$
193 rspa ${⊢}\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\wedge {j}\in \left(0\dots {n}\right)\right)\to \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)$
194 193 r19.21bi ${⊢}\left(\left(\forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\wedge {j}\in \left(0\dots {n}\right)\right)\wedge {t}\in {B}\left({j}\right)\right)\to 1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)$
195 190 191 192 194 syl21anc ${⊢}\left(\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\wedge {j}\in \left(0\dots {n}\right)\wedge {t}\in {B}\left({j}\right)\right)\to 1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)$
196 1 131 141 6 7 142 109 145 146 148 150 151 152 162 173 179 187 195 stoweidlem34 ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\to \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(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)\right)$
197 nfmpt1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)$
198 197 nfeq2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)$
199 fveq1 ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\to {g}\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)$
200 199 breq1d ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\to \left({g}\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}↔\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\right)$
201 199 breq2d ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\to \left(\left({j}-\left(\frac{4}{3}\right)\right){E}<{g}\left({t}\right)↔\left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)$
202 200 201 anbi12d ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\to \left(\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)↔\left(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)\right)$
203 202 anbi2d ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\to \left(\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)↔\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(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)\right)\right)$
204 203 rexbidv ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\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)↔\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(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)\right)\right)$
205 198 204 ralbid ${⊢}{g}=\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\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)↔\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(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)\right)\right)$
206 205 rspcev ${⊢}\left(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\in {A}\wedge \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(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)<\left({j}+\left(\frac{1}{3}\right)\right){E}\wedge \left({j}-\left(\frac{4}{3}\right)\right){E}<\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{x}\left({i}\right)\left({t}\right)\right)\left({t}\right)\right)\right)\right)\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)$
207 125 196 206 syl2anc ${⊢}\left({\phi }\wedge \left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\right)\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)$
208 207 ex ${⊢}{\phi }\to \left(\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\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)\right)$
209 208 2eximdv ${⊢}{\phi }\to \left(\exists {n}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({n}\in ℕ\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)<\left({n}-1\right){E}\right)\wedge {x}:\left(0\dots {n}\right)⟶{A}\wedge \forall {j}\in \left(0\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {x}\left({j}\right)\left({t}\right)\wedge {x}\left({j}\right)\left({t}\right)\le 1\right)\wedge \forall {t}\in {D}\left({j}\right)\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)\left({t}\right)<\frac{{E}}{{n}}\wedge \forall {t}\in {B}\left({j}\right)\phantom{\rule{.4em}{0ex}}1-\left(\frac{{E}}{{n}}\right)<{x}\left({j}\right)\left({t}\right)\right)\right)\to \exists {n}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\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)\right)$
210 107 209 mpd ${⊢}{\phi }\to \exists {n}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\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)$
211 idd ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\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 {x}\phantom{\rule{.4em}{0ex}}\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)\right)$
212 211 exlimdv ${⊢}{\phi }\to \left(\exists {n}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\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 {x}\phantom{\rule{.4em}{0ex}}\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)\right)$
213 210 212 mpd ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\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)$
214 idd ${⊢}{\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}}\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)\right)$
215 214 exlimdv ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\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}}\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)\right)$
216 213 215 mpd ${⊢}{\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)$