# Metamath Proof Explorer

## Theorem poimir

Description: Poincare-Miranda theorem. Theorem on Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
poimir.i ${⊢}{I}={\left[0,1\right]}^{\left(1\dots {N}\right)}$
poimir.r ${⊢}{R}={\prod }_{𝑡}\left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right)$
poimir.1 ${⊢}{\phi }\to {F}\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}{R}\right)$
poimir.2 ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge {z}\in {I}\wedge {z}\left({n}\right)=0\right)\right)\to {F}\left({z}\right)\left({n}\right)\le 0$
poimir.3 ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge {z}\in {I}\wedge {z}\left({n}\right)=1\right)\right)\to 0\le {F}\left({z}\right)\left({n}\right)$
Assertion poimir ${⊢}{\phi }\to \exists {c}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)=\left(1\dots {N}\right)×\left\{0\right\}$

### Proof

Step Hyp Ref Expression
1 poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
2 poimir.i ${⊢}{I}={\left[0,1\right]}^{\left(1\dots {N}\right)}$
3 poimir.r ${⊢}{R}={\prod }_{𝑡}\left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right)$
4 poimir.1 ${⊢}{\phi }\to {F}\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}{R}\right)$
5 poimir.2 ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge {z}\in {I}\wedge {z}\left({n}\right)=0\right)\right)\to {F}\left({z}\right)\left({n}\right)\le 0$
6 poimir.3 ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge {z}\in {I}\wedge {z}\left({n}\right)=1\right)\right)\to 0\le {F}\left({z}\right)\left({n}\right)$
7 1 2 3 4 5 6 poimirlem32 ${⊢}{\phi }\to \exists {c}\in {I}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
8 ovex ${⊢}\left(1\dots {N}\right)\in \mathrm{V}$
9 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
10 3 pttoponconst ${⊢}\left(\left(1\dots {N}\right)\in \mathrm{V}\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)\right)\to {R}\in \mathrm{TopOn}\left({ℝ}^{\left(1\dots {N}\right)}\right)$
11 8 9 10 mp2an ${⊢}{R}\in \mathrm{TopOn}\left({ℝ}^{\left(1\dots {N}\right)}\right)$
12 11 topontopi ${⊢}{R}\in \mathrm{Top}$
13 reex ${⊢}ℝ\in \mathrm{V}$
14 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
15 mapss ${⊢}\left(ℝ\in \mathrm{V}\wedge \left[0,1\right]\subseteq ℝ\right)\to {\left[0,1\right]}^{\left(1\dots {N}\right)}\subseteq {ℝ}^{\left(1\dots {N}\right)}$
16 13 14 15 mp2an ${⊢}{\left[0,1\right]}^{\left(1\dots {N}\right)}\subseteq {ℝ}^{\left(1\dots {N}\right)}$
17 2 16 eqsstri ${⊢}{I}\subseteq {ℝ}^{\left(1\dots {N}\right)}$
18 11 toponunii ${⊢}{ℝ}^{\left(1\dots {N}\right)}=\bigcup {R}$
19 18 restuni ${⊢}\left({R}\in \mathrm{Top}\wedge {I}\subseteq {ℝ}^{\left(1\dots {N}\right)}\right)\to {I}=\bigcup \left({R}{↾}_{𝑡}{I}\right)$
20 12 17 19 mp2an ${⊢}{I}=\bigcup \left({R}{↾}_{𝑡}{I}\right)$
21 20 18 cnf ${⊢}{F}\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}{R}\right)\to {F}:{I}⟶{ℝ}^{\left(1\dots {N}\right)}$
22 4 21 syl ${⊢}{\phi }\to {F}:{I}⟶{ℝ}^{\left(1\dots {N}\right)}$
23 22 ffvelrnda ${⊢}\left({\phi }\wedge {c}\in {I}\right)\to {F}\left({c}\right)\in \left({ℝ}^{\left(1\dots {N}\right)}\right)$
24 elmapi ${⊢}{F}\left({c}\right)\in \left({ℝ}^{\left(1\dots {N}\right)}\right)\to {F}\left({c}\right):\left(1\dots {N}\right)⟶ℝ$
25 23 24 syl ${⊢}\left({\phi }\wedge {c}\in {I}\right)\to {F}\left({c}\right):\left(1\dots {N}\right)⟶ℝ$
26 25 ffvelrnda ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {F}\left({c}\right)\left({n}\right)\in ℝ$
27 recn ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)\in ℂ$
28 absrpcl ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℂ\wedge {F}\left({c}\right)\left({n}\right)\ne 0\right)\to \left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}$
29 28 ex ${⊢}{F}\left({c}\right)\left({n}\right)\in ℂ\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}\right)$
30 27 29 syl ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}\right)$
31 ltsubrp ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge \left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}\right)\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({c}\right)\left({n}\right)$
32 ltaddrp ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge \left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}\right)\to {F}\left({c}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|$
33 31 32 jca ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge \left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({c}\right)\left({n}\right)\wedge {F}\left({c}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)$
34 33 ex ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to \left(\left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{+}\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({c}\right)\left({n}\right)\wedge {F}\left({c}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
35 30 34 syld ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({c}\right)\left({n}\right)\wedge {F}\left({c}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
36 27 abscld ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to \left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ$
37 resubcl ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge \left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ\right)\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ$
38 36 37 mpdan ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ$
39 38 rexrd ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{*}$
40 readdcl ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge \left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ\right)\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ$
41 36 40 mpdan ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\in ℝ$
42 41 rexrd ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{*}$
43 rexr ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)\in {ℝ}^{*}$
44 elioo5 ${⊢}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{*}\wedge {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\in {ℝ}^{*}\wedge {F}\left({c}\right)\left({n}\right)\in {ℝ}^{*}\right)\to \left({F}\left({c}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({c}\right)\left({n}\right)\wedge {F}\left({c}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
45 39 42 43 44 syl3anc ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to \left({F}\left({c}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({c}\right)\left({n}\right)\wedge {F}\left({c}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
46 35 45 sylibrd ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to {F}\left({c}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
47 26 46 syl ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to {F}\left({c}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
48 fveq2 ${⊢}{x}={c}\to {F}\left({x}\right)={F}\left({c}\right)$
49 48 fveq1d ${⊢}{x}={c}\to {F}\left({x}\right)\left({n}\right)={F}\left({c}\right)\left({n}\right)$
50 eqid ${⊢}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)=\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)$
51 fvex ${⊢}{F}\left({c}\right)\left({n}\right)\in \mathrm{V}$
52 49 50 51 fvmpt ${⊢}{c}\in {I}\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)={F}\left({c}\right)\left({n}\right)$
53 52 eleq1d ${⊢}{c}\in {I}\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔{F}\left({c}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
54 53 ad2antlr ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔{F}\left({c}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
55 47 54 sylibrd ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
56 iooretop ${⊢}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
57 resttopon ${⊢}\left({R}\in \mathrm{TopOn}\left({ℝ}^{\left(1\dots {N}\right)}\right)\wedge {I}\subseteq {ℝ}^{\left(1\dots {N}\right)}\right)\to {R}{↾}_{𝑡}{I}\in \mathrm{TopOn}\left({I}\right)$
58 11 17 57 mp2an ${⊢}{R}{↾}_{𝑡}{I}\in \mathrm{TopOn}\left({I}\right)$
59 58 a1i ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {R}{↾}_{𝑡}{I}\in \mathrm{TopOn}\left({I}\right)$
60 22 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {I}⟼{F}\left({x}\right)\right)$
61 60 4 eqeltrrd ${⊢}{\phi }\to \left({x}\in {I}⟼{F}\left({x}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}{R}\right)$
62 61 adantr ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({x}\in {I}⟼{F}\left({x}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}{R}\right)$
63 11 a1i ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {R}\in \mathrm{TopOn}\left({ℝ}^{\left(1\dots {N}\right)}\right)$
64 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
65 64 fconst6 ${⊢}\left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right):\left(1\dots {N}\right)⟶\mathrm{Top}$
66 18 3 ptpjcn ${⊢}\left(\left(1\dots {N}\right)\in \mathrm{V}\wedge \left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right):\left(1\dots {N}\right)⟶\mathrm{Top}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({z}\in \left({ℝ}^{\left(1\dots {N}\right)}\right)⟼{z}\left({n}\right)\right)\in \left({R}\mathrm{Cn}\left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right)\left({n}\right)\right)$
67 8 65 66 mp3an12 ${⊢}{n}\in \left(1\dots {N}\right)\to \left({z}\in \left({ℝ}^{\left(1\dots {N}\right)}\right)⟼{z}\left({n}\right)\right)\in \left({R}\mathrm{Cn}\left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right)\left({n}\right)\right)$
68 fvex ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{V}$
69 68 fvconst2 ${⊢}{n}\in \left(1\dots {N}\right)\to \left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right)\left({n}\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
70 69 oveq2d ${⊢}{n}\in \left(1\dots {N}\right)\to {R}\mathrm{Cn}\left(\left(1\dots {N}\right)×\left\{\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right\}\right)\left({n}\right)={R}\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
71 67 70 eleqtrd ${⊢}{n}\in \left(1\dots {N}\right)\to \left({z}\in \left({ℝ}^{\left(1\dots {N}\right)}\right)⟼{z}\left({n}\right)\right)\in \left({R}\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
72 71 adantl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({z}\in \left({ℝ}^{\left(1\dots {N}\right)}\right)⟼{z}\left({n}\right)\right)\in \left({R}\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
73 fveq1 ${⊢}{z}={F}\left({x}\right)\to {z}\left({n}\right)={F}\left({x}\right)\left({n}\right)$
74 59 62 63 72 73 cnmpt11 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
75 20 cncnpi ${⊢}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in {I}\right)\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({c}\right)$
76 74 75 sylan ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {c}\in {I}\right)\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({c}\right)$
77 76 an32s ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({c}\right)$
78 iscnp ${⊢}\left({R}{↾}_{𝑡}{I}\in \mathrm{TopOn}\left({I}\right)\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)\wedge {c}\in {I}\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({c}\right)↔\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right):{I}⟶ℝ\wedge \forall {z}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)\right)\right)$
79 58 9 78 mp3an12 ${⊢}{c}\in {I}\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({c}\right)↔\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right):{I}⟶ℝ\wedge \forall {z}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)\right)\right)$
80 79 ad2antlr ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\in \left(\left({R}{↾}_{𝑡}{I}\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({c}\right)↔\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right):{I}⟶ℝ\wedge \forall {z}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)\right)\right)$
81 77 80 mpbid ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right):{I}⟶ℝ\wedge \forall {z}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)\right)$
82 81 simprd ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \forall {z}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)$
83 eleq2 ${⊢}{z}=\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}↔\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
84 sseq2 ${⊢}{z}=\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}↔\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
85 84 anbi2d ${⊢}{z}=\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left(\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)↔\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\right)$
86 85 rexbidv ${⊢}{z}=\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left(\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)↔\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\right)$
87 83 86 imbi12d ${⊢}{z}=\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left(\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)↔\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\right)\right)$
88 87 rspcv ${⊢}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to \left(\forall {z}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in {z}\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq {z}\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\right)\right)$
89 56 82 88 mpsyl ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({c}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\right)$
90 55 89 syld ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\right)$
91 0re ${⊢}0\in ℝ$
92 letric ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge 0\in ℝ\right)\to \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)$
93 26 91 92 sylancl ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)$
94 90 93 jctird ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \left(\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)$
95 r19.41v ${⊢}\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left(\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)↔\left(\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)$
96 anass ${⊢}\left(\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)↔\left({c}\in {v}\wedge \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)$
97 96 rexbii ${⊢}\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left(\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)↔\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)$
98 95 97 bitr3i ${⊢}\left(\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)↔\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)$
99 94 98 syl6ib ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)\right)$
100 58 topontopi ${⊢}{R}{↾}_{𝑡}{I}\in \mathrm{Top}$
101 20 eltopss ${⊢}\left({R}{↾}_{𝑡}{I}\in \mathrm{Top}\wedge {v}\in \left({R}{↾}_{𝑡}{I}\right)\right)\to {v}\subseteq {I}$
102 100 101 mpan ${⊢}{v}\in \left({R}{↾}_{𝑡}{I}\right)\to {v}\subseteq {I}$
103 fvex ${⊢}{F}\left({x}\right)\left({n}\right)\in \mathrm{V}$
104 103 50 dmmpti ${⊢}\mathrm{dom}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)={I}$
105 104 sseq2i ${⊢}{v}\subseteq \mathrm{dom}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)↔{v}\subseteq {I}$
106 funmpt ${⊢}\mathrm{Fun}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)$
107 funimass4 ${⊢}\left(\mathrm{Fun}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\wedge {v}\subseteq \mathrm{dom}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
108 106 107 mpan ${⊢}{v}\subseteq \mathrm{dom}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
109 105 108 sylbir ${⊢}{v}\subseteq {I}\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
110 ssel2 ${⊢}\left({v}\subseteq {I}\wedge {z}\in {v}\right)\to {z}\in {I}$
111 fveq2 ${⊢}{x}={z}\to {F}\left({x}\right)={F}\left({z}\right)$
112 111 fveq1d ${⊢}{x}={z}\to {F}\left({x}\right)\left({n}\right)={F}\left({z}\right)\left({n}\right)$
113 fvex ${⊢}{F}\left({z}\right)\left({n}\right)\in \mathrm{V}$
114 112 50 113 fvmpt ${⊢}{z}\in {I}\to \left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)={F}\left({z}\right)\left({n}\right)$
115 114 eleq1d ${⊢}{z}\in {I}\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)↔{F}\left({z}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
116 eliooord ${⊢}{F}\left({z}\right)\left({n}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)$
117 115 116 syl6bi ${⊢}{z}\in {I}\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
118 110 117 syl ${⊢}\left({v}\subseteq {I}\wedge {z}\in {v}\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
119 118 ralimdva ${⊢}{v}\subseteq {I}\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left({z}\right)\in \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
120 109 119 sylbid ${⊢}{v}\subseteq {I}\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
121 120 adantl ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\to \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)$
122 absnid ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\to \left|{F}\left({c}\right)\left({n}\right)\right|=-{F}\left({c}\right)\left({n}\right)$
123 122 oveq2d ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|={F}\left({c}\right)\left({n}\right)+\left(-{F}\left({c}\right)\left({n}\right)\right)$
124 27 negidd ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)+\left(-{F}\left({c}\right)\left({n}\right)\right)=0$
125 124 adantr ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\to {F}\left({c}\right)\left({n}\right)+\left(-{F}\left({c}\right)\left({n}\right)\right)=0$
126 123 125 eqtrd ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|=0$
127 26 126 sylan ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|=0$
128 127 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {z}\in {I}\right)\to {F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|=0$
129 128 breq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {z}\in {I}\right)\to \left({F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|↔{F}\left({z}\right)\left({n}\right)<0\right)$
130 22 ffvelrnda ${⊢}\left({\phi }\wedge {z}\in {I}\right)\to {F}\left({z}\right)\in \left({ℝ}^{\left(1\dots {N}\right)}\right)$
131 elmapi ${⊢}{F}\left({z}\right)\in \left({ℝ}^{\left(1\dots {N}\right)}\right)\to {F}\left({z}\right):\left(1\dots {N}\right)⟶ℝ$
132 130 131 syl ${⊢}\left({\phi }\wedge {z}\in {I}\right)\to {F}\left({z}\right):\left(1\dots {N}\right)⟶ℝ$
133 132 ffvelrnda ${⊢}\left(\left({\phi }\wedge {z}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {F}\left({z}\right)\left({n}\right)\in ℝ$
134 133 an32s ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {z}\in {I}\right)\to {F}\left({z}\right)\left({n}\right)\in ℝ$
135 0red ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {z}\in {I}\right)\to 0\in ℝ$
136 134 135 ltnled ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {z}\in {I}\right)\to \left({F}\left({z}\right)\left({n}\right)<0↔¬0\le {F}\left({z}\right)\left({n}\right)\right)$
137 136 adantllr ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {z}\in {I}\right)\to \left({F}\left({z}\right)\left({n}\right)<0↔¬0\le {F}\left({z}\right)\left({n}\right)\right)$
138 137 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {z}\in {I}\right)\to \left({F}\left({z}\right)\left({n}\right)<0↔¬0\le {F}\left({z}\right)\left({n}\right)\right)$
139 129 138 bitrd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {z}\in {I}\right)\to \left({F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|↔¬0\le {F}\left({z}\right)\left({n}\right)\right)$
140 139 biimpd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {z}\in {I}\right)\to \left({F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\to ¬0\le {F}\left({z}\right)\left({n}\right)\right)$
141 110 140 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge \left({v}\subseteq {I}\wedge {z}\in {v}\right)\right)\to \left({F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\to ¬0\le {F}\left({z}\right)\left({n}\right)\right)$
142 141 anassrs ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {v}\subseteq {I}\right)\wedge {z}\in {v}\right)\to \left({F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\to ¬0\le {F}\left({z}\right)\left({n}\right)\right)$
143 142 adantld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {v}\subseteq {I}\right)\wedge {z}\in {v}\right)\to \left(\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to ¬0\le {F}\left({z}\right)\left({n}\right)\right)$
144 143 ralimdva ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\wedge {v}\subseteq {I}\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\right)$
145 144 an32s ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\wedge {F}\left({c}\right)\left({n}\right)\le 0\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\right)$
146 145 impancom ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\wedge \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\le 0\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\right)$
147 absid ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\to \left|{F}\left({c}\right)\left({n}\right)\right|={F}\left({c}\right)\left({n}\right)$
148 147 oveq2d ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|={F}\left({c}\right)\left({n}\right)-{F}\left({c}\right)\left({n}\right)$
149 27 subidd ${⊢}{F}\left({c}\right)\left({n}\right)\in ℝ\to {F}\left({c}\right)\left({n}\right)-{F}\left({c}\right)\left({n}\right)=0$
150 149 adantr ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\to {F}\left({c}\right)\left({n}\right)-{F}\left({c}\right)\left({n}\right)=0$
151 148 150 eqtrd ${⊢}\left({F}\left({c}\right)\left({n}\right)\in ℝ\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|=0$
152 26 151 sylan ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|=0$
153 152 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {z}\in {I}\right)\to {F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|=0$
154 153 breq1d ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {z}\in {I}\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)↔0<{F}\left({z}\right)\left({n}\right)\right)$
155 135 134 ltnled ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {z}\in {I}\right)\to \left(0<{F}\left({z}\right)\left({n}\right)↔¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
156 155 adantllr ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {z}\in {I}\right)\to \left(0<{F}\left({z}\right)\left({n}\right)↔¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
157 156 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {z}\in {I}\right)\to \left(0<{F}\left({z}\right)\left({n}\right)↔¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
158 154 157 bitrd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {z}\in {I}\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)↔¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
159 158 biimpd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {z}\in {I}\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\to ¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
160 110 159 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge \left({v}\subseteq {I}\wedge {z}\in {v}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\to ¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
161 160 anassrs ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {v}\subseteq {I}\right)\wedge {z}\in {v}\right)\to \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\to ¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
162 161 adantrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {v}\subseteq {I}\right)\wedge {z}\in {v}\right)\to \left(\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to ¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
163 162 ralimdva ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\wedge {v}\subseteq {I}\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
164 163 an32s ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\wedge 0\le {F}\left({c}\right)\left({n}\right)\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
165 164 impancom ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\wedge \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\to \left(0\le {F}\left({c}\right)\left({n}\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
166 146 165 orim12d ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\wedge \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\right)\to \left(\left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)$
167 166 expimpd ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\to \left(\left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|<{F}\left({z}\right)\left({n}\right)\wedge {F}\left({z}\right)\left({n}\right)<{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)$
168 121 167 syland ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\subseteq {I}\right)\to \left(\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)$
169 102 168 sylan2 ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\in \left({R}{↾}_{𝑡}{I}\right)\right)\to \left(\left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)$
170 169 anim2d ${⊢}\left(\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\wedge {v}\in \left({R}{↾}_{𝑡}{I}\right)\right)\to \left(\left({c}\in {v}\wedge \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)\to \left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)\right)$
171 170 reximdva ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\left({x}\in {I}⟼{F}\left({x}\right)\left({n}\right)\right)\left[{v}\right]\subseteq \left({F}\left({c}\right)\left({n}\right)-\left|{F}\left({c}\right)\left({n}\right)\right|,{F}\left({c}\right)\left({n}\right)+\left|{F}\left({c}\right)\left({n}\right)\right|\right)\wedge \left({F}\left({c}\right)\left({n}\right)\le 0\vee 0\le {F}\left({c}\right)\left({n}\right)\right)\right)\right)\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)\right)$
172 99 171 syld ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to \exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)\right)$
173 ralnex ${⊢}\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0{r}{F}\left({z}\right)\left({n}\right)↔¬\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)$
174 173 rexbii ${⊢}\exists {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0{r}{F}\left({z}\right)\left({n}\right)↔\exists {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}¬\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)$
175 letsr ${⊢}\le \in \mathrm{TosetRel}$
176 175 elexi ${⊢}\le \in \mathrm{V}$
177 176 cnvex ${⊢}{\le }^{-1}\in \mathrm{V}$
178 breq ${⊢}{r}=\le \to \left(0{r}{F}\left({z}\right)\left({n}\right)↔0\le {F}\left({z}\right)\left({n}\right)\right)$
179 178 notbid ${⊢}{r}=\le \to \left(¬0{r}{F}\left({z}\right)\left({n}\right)↔¬0\le {F}\left({z}\right)\left({n}\right)\right)$
180 179 ralbidv ${⊢}{r}=\le \to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0{r}{F}\left({z}\right)\left({n}\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\right)$
181 breq ${⊢}{r}={\le }^{-1}\to \left(0{r}{F}\left({z}\right)\left({n}\right)↔0{\le }^{-1}{F}\left({z}\right)\left({n}\right)\right)$
182 c0ex ${⊢}0\in \mathrm{V}$
183 182 113 brcnv ${⊢}0{\le }^{-1}{F}\left({z}\right)\left({n}\right)↔{F}\left({z}\right)\left({n}\right)\le 0$
184 181 183 syl6bb ${⊢}{r}={\le }^{-1}\to \left(0{r}{F}\left({z}\right)\left({n}\right)↔{F}\left({z}\right)\left({n}\right)\le 0\right)$
185 184 notbid ${⊢}{r}={\le }^{-1}\to \left(¬0{r}{F}\left({z}\right)\left({n}\right)↔¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
186 185 ralbidv ${⊢}{r}={\le }^{-1}\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0{r}{F}\left({z}\right)\left({n}\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
187 176 177 180 186 rexpr ${⊢}\exists {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0{r}{F}\left({z}\right)\left({n}\right)↔\left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)$
188 rexnal ${⊢}\exists {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}¬\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)↔¬\forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)$
189 174 187 188 3bitr3i ${⊢}\left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)↔¬\forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)$
190 189 anbi2i ${⊢}\left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)↔\left({c}\in {v}\wedge ¬\forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
191 annim ${⊢}\left({c}\in {v}\wedge ¬\forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)↔¬\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
192 190 191 bitri ${⊢}\left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)↔¬\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
193 192 rexbii ${⊢}\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)↔\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}¬\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
194 rexnal ${⊢}\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}¬\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)↔¬\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
195 193 194 bitri ${⊢}\exists {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\wedge \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬0\le {F}\left({z}\right)\left({n}\right)\vee \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}¬{F}\left({z}\right)\left({n}\right)\le 0\right)\right)↔¬\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)$
196 172 195 syl6ib ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left({F}\left({c}\right)\left({n}\right)\ne 0\to ¬\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)\right)$
197 196 necon4ad ${⊢}\left(\left({\phi }\wedge {c}\in {I}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)\to {F}\left({c}\right)\left({n}\right)=0\right)$
198 197 ralimdva ${⊢}\left({\phi }\wedge {c}\in {I}\right)\to \left(\forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)\to \forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)\left({n}\right)=0\right)$
199 25 ffnd ${⊢}\left({\phi }\wedge {c}\in {I}\right)\to {F}\left({c}\right)Fn\left(1\dots {N}\right)$
200 198 199 jctild ${⊢}\left({\phi }\wedge {c}\in {I}\right)\to \left(\forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)\to \left({F}\left({c}\right)Fn\left(1\dots {N}\right)\wedge \forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)\left({n}\right)=0\right)\right)$
201 fconstfv ${⊢}{F}\left({c}\right):\left(1\dots {N}\right)⟶\left\{0\right\}↔\left({F}\left({c}\right)Fn\left(1\dots {N}\right)\wedge \forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)\left({n}\right)=0\right)$
202 182 fconst2 ${⊢}{F}\left({c}\right):\left(1\dots {N}\right)⟶\left\{0\right\}↔{F}\left({c}\right)=\left(1\dots {N}\right)×\left\{0\right\}$
203 201 202 bitr3i ${⊢}\left({F}\left({c}\right)Fn\left(1\dots {N}\right)\wedge \forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)\left({n}\right)=0\right)↔{F}\left({c}\right)=\left(1\dots {N}\right)×\left\{0\right\}$
204 200 203 syl6ib ${⊢}\left({\phi }\wedge {c}\in {I}\right)\to \left(\forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)\to {F}\left({c}\right)=\left(1\dots {N}\right)×\left\{0\right\}\right)$
205 204 reximdva ${⊢}{\phi }\to \left(\exists {c}\in {I}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({R}{↾}_{𝑡}{I}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in {v}\to \forall {r}\in \left\{\le ,{\le }^{-1}\right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {v}\phantom{\rule{.4em}{0ex}}0{r}{F}\left({z}\right)\left({n}\right)\right)\to \exists {c}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)=\left(1\dots {N}\right)×\left\{0\right\}\right)$
206 7 205 mpd ${⊢}{\phi }\to \exists {c}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)=\left(1\dots {N}\right)×\left\{0\right\}$