# Metamath Proof Explorer

## Theorem lhop1lem

Description: Lemma for lhop1 . (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses lhop1.a ${⊢}{\phi }\to {A}\in ℝ$
lhop1.b ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
lhop1.l ${⊢}{\phi }\to {A}<{B}$
lhop1.f ${⊢}{\phi }\to {F}:\left({A},{B}\right)⟶ℝ$
lhop1.g ${⊢}{\phi }\to {G}:\left({A},{B}\right)⟶ℝ$
lhop1.if ${⊢}{\phi }\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
lhop1.ig ${⊢}{\phi }\to \mathrm{dom}{{G}}_{ℝ}^{\prime }=\left({A},{B}\right)$
lhop1.f0 ${⊢}{\phi }\to 0\in \left({F}{lim}_{ℂ}{A}\right)$
lhop1.g0 ${⊢}{\phi }\to 0\in \left({G}{lim}_{ℂ}{A}\right)$
lhop1.gn0 ${⊢}{\phi }\to ¬0\in \mathrm{ran}{G}$
lhop1.gd0 ${⊢}{\phi }\to ¬0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
lhop1.c ${⊢}{\phi }\to {C}\in \left(\left({z}\in \left({A},{B}\right)⟼\frac{{{F}}_{ℝ}^{\prime }\left({z}\right)}{{{G}}_{ℝ}^{\prime }\left({z}\right)}\right){lim}_{ℂ}{A}\right)$
lhop1lem.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
lhop1lem.d ${⊢}{\phi }\to {D}\in ℝ$
lhop1lem.db ${⊢}{\phi }\to {D}\le {B}$
lhop1lem.x ${⊢}{\phi }\to {X}\in \left({A},{D}\right)$
lhop1lem.t ${⊢}{\phi }\to \forall {t}\in \left({A},{D}\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({t}\right)}{{{G}}_{ℝ}^{\prime }\left({t}\right)}\right)-{C}\right|<{E}$
lhop1lem.r ${⊢}{R}={A}+\left(\frac{{r}}{2}\right)$
Assertion lhop1lem ${⊢}{\phi }\to \left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|<2{E}$

### Proof

Step Hyp Ref Expression
1 lhop1.a ${⊢}{\phi }\to {A}\in ℝ$
2 lhop1.b ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
3 lhop1.l ${⊢}{\phi }\to {A}<{B}$
4 lhop1.f ${⊢}{\phi }\to {F}:\left({A},{B}\right)⟶ℝ$
5 lhop1.g ${⊢}{\phi }\to {G}:\left({A},{B}\right)⟶ℝ$
6 lhop1.if ${⊢}{\phi }\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
7 lhop1.ig ${⊢}{\phi }\to \mathrm{dom}{{G}}_{ℝ}^{\prime }=\left({A},{B}\right)$
8 lhop1.f0 ${⊢}{\phi }\to 0\in \left({F}{lim}_{ℂ}{A}\right)$
9 lhop1.g0 ${⊢}{\phi }\to 0\in \left({G}{lim}_{ℂ}{A}\right)$
10 lhop1.gn0 ${⊢}{\phi }\to ¬0\in \mathrm{ran}{G}$
11 lhop1.gd0 ${⊢}{\phi }\to ¬0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
12 lhop1.c ${⊢}{\phi }\to {C}\in \left(\left({z}\in \left({A},{B}\right)⟼\frac{{{F}}_{ℝ}^{\prime }\left({z}\right)}{{{G}}_{ℝ}^{\prime }\left({z}\right)}\right){lim}_{ℂ}{A}\right)$
13 lhop1lem.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
14 lhop1lem.d ${⊢}{\phi }\to {D}\in ℝ$
15 lhop1lem.db ${⊢}{\phi }\to {D}\le {B}$
16 lhop1lem.x ${⊢}{\phi }\to {X}\in \left({A},{D}\right)$
17 lhop1lem.t ${⊢}{\phi }\to \forall {t}\in \left({A},{D}\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({t}\right)}{{{G}}_{ℝ}^{\prime }\left({t}\right)}\right)-{C}\right|<{E}$
18 lhop1lem.r ${⊢}{R}={A}+\left(\frac{{r}}{2}\right)$
19 iooss2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {D}\le {B}\right)\to \left({A},{D}\right)\subseteq \left({A},{B}\right)$
20 2 15 19 syl2anc ${⊢}{\phi }\to \left({A},{D}\right)\subseteq \left({A},{B}\right)$
21 20 16 sseldd ${⊢}{\phi }\to {X}\in \left({A},{B}\right)$
22 4 21 ffvelrnd ${⊢}{\phi }\to {F}\left({X}\right)\in ℝ$
23 22 recnd ${⊢}{\phi }\to {F}\left({X}\right)\in ℂ$
24 5 21 ffvelrnd ${⊢}{\phi }\to {G}\left({X}\right)\in ℝ$
25 24 recnd ${⊢}{\phi }\to {G}\left({X}\right)\in ℂ$
26 5 ffnd ${⊢}{\phi }\to {G}Fn\left({A},{B}\right)$
27 fnfvelrn ${⊢}\left({G}Fn\left({A},{B}\right)\wedge {X}\in \left({A},{B}\right)\right)\to {G}\left({X}\right)\in \mathrm{ran}{G}$
28 26 21 27 syl2anc ${⊢}{\phi }\to {G}\left({X}\right)\in \mathrm{ran}{G}$
29 eleq1 ${⊢}{G}\left({X}\right)=0\to \left({G}\left({X}\right)\in \mathrm{ran}{G}↔0\in \mathrm{ran}{G}\right)$
30 28 29 syl5ibcom ${⊢}{\phi }\to \left({G}\left({X}\right)=0\to 0\in \mathrm{ran}{G}\right)$
31 30 necon3bd ${⊢}{\phi }\to \left(¬0\in \mathrm{ran}{G}\to {G}\left({X}\right)\ne 0\right)$
32 10 31 mpd ${⊢}{\phi }\to {G}\left({X}\right)\ne 0$
33 23 25 32 divcld ${⊢}{\phi }\to \frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in ℂ$
34 limccl ${⊢}\left({z}\in \left({A},{B}\right)⟼\frac{{{F}}_{ℝ}^{\prime }\left({z}\right)}{{{G}}_{ℝ}^{\prime }\left({z}\right)}\right){lim}_{ℂ}{A}\subseteq ℂ$
35 34 12 sseldi ${⊢}{\phi }\to {C}\in ℂ$
36 33 35 subcld ${⊢}{\phi }\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\in ℂ$
37 36 abscld ${⊢}{\phi }\to \left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\in ℝ$
38 13 rpred ${⊢}{\phi }\to {E}\in ℝ$
39 2re ${⊢}2\in ℝ$
40 39 a1i ${⊢}{\phi }\to 2\in ℝ$
41 40 38 remulcld ${⊢}{\phi }\to 2{E}\in ℝ$
42 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
43 42 a1i ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
44 simprl ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
45 simprr ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to {A}\in {v}$
46 eliooord ${⊢}{X}\in \left({A},{D}\right)\to \left({A}<{X}\wedge {X}<{D}\right)$
47 16 46 syl ${⊢}{\phi }\to \left({A}<{X}\wedge {X}<{D}\right)$
48 47 simpld ${⊢}{\phi }\to {A}<{X}$
49 ioossre ${⊢}\left({A},{D}\right)\subseteq ℝ$
50 49 16 sseldi ${⊢}{\phi }\to {X}\in ℝ$
51 difrp ${⊢}\left({A}\in ℝ\wedge {X}\in ℝ\right)\to \left({A}<{X}↔{X}-{A}\in {ℝ}^{+}\right)$
52 1 50 51 syl2anc ${⊢}{\phi }\to \left({A}<{X}↔{X}-{A}\in {ℝ}^{+}\right)$
53 48 52 mpbid ${⊢}{\phi }\to {X}-{A}\in {ℝ}^{+}$
54 53 adantr ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to {X}-{A}\in {ℝ}^{+}$
55 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
56 55 cnfldtopn ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
57 56 mopni3 ${⊢}\left(\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\wedge {X}-{A}\in {ℝ}^{+}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({r}<{X}-{A}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\right)$
58 43 44 45 54 57 syl31anc ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({r}<{X}-{A}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\right)$
59 ssrin ${⊢}{A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\to \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\subseteq {v}\cap \left({A},{X}\right)$
60 lbioo ${⊢}¬{A}\in \left({A},{X}\right)$
61 disjsn ${⊢}\left({A},{X}\right)\cap \left\{{A}\right\}=\varnothing ↔¬{A}\in \left({A},{X}\right)$
62 60 61 mpbir ${⊢}\left({A},{X}\right)\cap \left\{{A}\right\}=\varnothing$
63 disj3 ${⊢}\left({A},{X}\right)\cap \left\{{A}\right\}=\varnothing ↔\left({A},{X}\right)=\left({A},{X}\right)\setminus \left\{{A}\right\}$
64 62 63 mpbi ${⊢}\left({A},{X}\right)=\left({A},{X}\right)\setminus \left\{{A}\right\}$
65 64 ineq2i ${⊢}{v}\cap \left({A},{X}\right)={v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)$
66 59 65 sseqtrdi ${⊢}{A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\to \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\subseteq {v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)$
67 1 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}\in ℝ$
68 simprl ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {r}\in {ℝ}^{+}$
69 68 rpred ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {r}\in ℝ$
70 69 rehalfcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{r}}{2}\in ℝ$
71 67 70 readdcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}+\left(\frac{{r}}{2}\right)\in ℝ$
72 18 71 eqeltrid ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in ℝ$
73 72 recnd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in ℂ$
74 1 recnd ${⊢}{\phi }\to {A}\in ℂ$
75 74 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}\in ℂ$
76 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
77 76 cnmetdval ${⊢}\left({R}\in ℂ\wedge {A}\in ℂ\right)\to {R}\left(\mathrm{abs}\circ -\right){A}=\left|{R}-{A}\right|$
78 73 75 77 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\left(\mathrm{abs}\circ -\right){A}=\left|{R}-{A}\right|$
79 18 oveq1i ${⊢}{R}-{A}={A}+\left(\frac{{r}}{2}\right)-{A}$
80 69 recnd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {r}\in ℂ$
81 80 halfcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{r}}{2}\in ℂ$
82 75 81 pncan2d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}+\left(\frac{{r}}{2}\right)-{A}=\frac{{r}}{2}$
83 79 82 syl5eq ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}-{A}=\frac{{r}}{2}$
84 83 fveq2d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left|{R}-{A}\right|=\left|\frac{{r}}{2}\right|$
85 68 rphalfcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{r}}{2}\in {ℝ}^{+}$
86 85 rpred ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{r}}{2}\in ℝ$
87 85 rpge0d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to 0\le \frac{{r}}{2}$
88 86 87 absidd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left|\frac{{r}}{2}\right|=\frac{{r}}{2}$
89 78 84 88 3eqtrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\left(\mathrm{abs}\circ -\right){A}=\frac{{r}}{2}$
90 rphalflt ${⊢}{r}\in {ℝ}^{+}\to \frac{{r}}{2}<{r}$
91 68 90 syl ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{r}}{2}<{r}$
92 89 91 eqbrtrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\left(\mathrm{abs}\circ -\right){A}<{r}$
93 42 a1i ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
94 69 rexrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {r}\in {ℝ}^{*}$
95 elbl3 ${⊢}\left(\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {r}\in {ℝ}^{*}\right)\wedge \left({A}\in ℂ\wedge {R}\in ℂ\right)\right)\to \left({R}\in \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)↔{R}\left(\mathrm{abs}\circ -\right){A}<{r}\right)$
96 93 94 75 73 95 syl22anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R}\in \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)↔{R}\left(\mathrm{abs}\circ -\right){A}<{r}\right)$
97 92 96 mpbird ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)$
98 67 85 ltaddrpd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}<{A}+\left(\frac{{r}}{2}\right)$
99 98 18 breqtrrdi ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}<{R}$
100 50 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {X}\in ℝ$
101 100 67 resubcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {X}-{A}\in ℝ$
102 simprr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {r}<{X}-{A}$
103 86 69 101 91 102 lttrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{r}}{2}<{X}-{A}$
104 67 86 100 ltaddsub2d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({A}+\left(\frac{{r}}{2}\right)<{X}↔\frac{{r}}{2}<{X}-{A}\right)$
105 103 104 mpbird ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}+\left(\frac{{r}}{2}\right)<{X}$
106 18 105 eqbrtrid ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}<{X}$
107 67 rexrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}\in {ℝ}^{*}$
108 50 rexrd ${⊢}{\phi }\to {X}\in {ℝ}^{*}$
109 108 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {X}\in {ℝ}^{*}$
110 elioo2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {X}\in {ℝ}^{*}\right)\to \left({R}\in \left({A},{X}\right)↔\left({R}\in ℝ\wedge {A}<{R}\wedge {R}<{X}\right)\right)$
111 107 109 110 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R}\in \left({A},{X}\right)↔\left({R}\in ℝ\wedge {A}<{R}\wedge {R}<{X}\right)\right)$
112 72 99 106 111 mpbir3and ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in \left({A},{X}\right)$
113 97 112 elind ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in \left(\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\right)$
114 23 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}\left({X}\right)\in ℂ$
115 4 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}:\left({A},{B}\right)⟶ℝ$
116 14 rexrd ${⊢}{\phi }\to {D}\in {ℝ}^{*}$
117 47 simprd ${⊢}{\phi }\to {X}<{D}$
118 50 14 117 ltled ${⊢}{\phi }\to {X}\le {D}$
119 108 116 2 118 15 xrletrd ${⊢}{\phi }\to {X}\le {B}$
120 iooss2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {X}\le {B}\right)\to \left({A},{X}\right)\subseteq \left({A},{B}\right)$
121 2 119 120 syl2anc ${⊢}{\phi }\to \left({A},{X}\right)\subseteq \left({A},{B}\right)$
122 121 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({A},{X}\right)\subseteq \left({A},{B}\right)$
123 122 112 sseldd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in \left({A},{B}\right)$
124 115 123 ffvelrnd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}\left({R}\right)\in ℝ$
125 124 recnd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}\left({R}\right)\in ℂ$
126 114 125 subcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}\left({X}\right)-{F}\left({R}\right)\in ℂ$
127 25 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}\left({X}\right)\in ℂ$
128 5 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}:\left({A},{B}\right)⟶ℝ$
129 128 123 ffvelrnd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}\left({R}\right)\in ℝ$
130 129 recnd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}\left({R}\right)\in ℂ$
131 127 130 subcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}\left({X}\right)-{G}\left({R}\right)\in ℂ$
132 fveq2 ${⊢}{z}={R}\to {G}\left({z}\right)={G}\left({R}\right)$
133 132 oveq2d ${⊢}{z}={R}\to {G}\left({X}\right)-{G}\left({z}\right)={G}\left({X}\right)-{G}\left({R}\right)$
134 133 neeq1d ${⊢}{z}={R}\to \left({G}\left({X}\right)-{G}\left({z}\right)\ne 0↔{G}\left({X}\right)-{G}\left({R}\right)\ne 0\right)$
135 11 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to ¬0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
136 25 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {G}\left({X}\right)\in ℂ$
137 121 sselda ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {z}\in \left({A},{B}\right)$
138 5 ffvelrnda ${⊢}\left({\phi }\wedge {z}\in \left({A},{B}\right)\right)\to {G}\left({z}\right)\in ℝ$
139 137 138 syldan ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {G}\left({z}\right)\in ℝ$
140 139 recnd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {G}\left({z}\right)\in ℂ$
141 136 140 subeq0ad ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left({G}\left({X}\right)-{G}\left({z}\right)=0↔{G}\left({X}\right)={G}\left({z}\right)\right)$
142 ioossre ${⊢}\left({A},{B}\right)\subseteq ℝ$
143 142 137 sseldi ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {z}\in ℝ$
144 143 adantr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {z}\in ℝ$
145 50 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {X}\in ℝ$
146 eliooord ${⊢}{z}\in \left({A},{X}\right)\to \left({A}<{z}\wedge {z}<{X}\right)$
147 146 adantl ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left({A}<{z}\wedge {z}<{X}\right)$
148 147 simprd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {z}<{X}$
149 148 adantr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {z}<{X}$
150 1 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
151 150 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {A}\in {ℝ}^{*}$
152 2 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {B}\in {ℝ}^{*}$
153 147 simpld ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {A}<{z}$
154 108 116 2 117 15 xrltletrd ${⊢}{\phi }\to {X}<{B}$
155 154 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {X}<{B}$
156 iccssioo ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}<{z}\wedge {X}<{B}\right)\right)\to \left[{z},{X}\right]\subseteq \left({A},{B}\right)$
157 151 152 153 155 156 syl22anc ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left[{z},{X}\right]\subseteq \left({A},{B}\right)$
158 157 adantr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left[{z},{X}\right]\subseteq \left({A},{B}\right)$
159 ax-resscn ${⊢}ℝ\subseteq ℂ$
160 159 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
161 fss ${⊢}\left({G}:\left({A},{B}\right)⟶ℝ\wedge ℝ\subseteq ℂ\right)\to {G}:\left({A},{B}\right)⟶ℂ$
162 5 159 161 sylancl ${⊢}{\phi }\to {G}:\left({A},{B}\right)⟶ℂ$
163 142 a1i ${⊢}{\phi }\to \left({A},{B}\right)\subseteq ℝ$
164 dvcn ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {G}:\left({A},{B}\right)⟶ℂ\wedge \left({A},{B}\right)\subseteq ℝ\right)\wedge \mathrm{dom}{{G}}_{ℝ}^{\prime }=\left({A},{B}\right)\right)\to {G}:\left({A},{B}\right)\underset{cn}{⟶}ℂ$
165 160 162 163 7 164 syl31anc ${⊢}{\phi }\to {G}:\left({A},{B}\right)\underset{cn}{⟶}ℂ$
166 cncffvrn ${⊢}\left(ℝ\subseteq ℂ\wedge {G}:\left({A},{B}\right)\underset{cn}{⟶}ℂ\right)\to \left({G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ↔{G}:\left({A},{B}\right)⟶ℝ\right)$
167 159 165 166 sylancr ${⊢}{\phi }\to \left({G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ↔{G}:\left({A},{B}\right)⟶ℝ\right)$
168 5 167 mpbird ${⊢}{\phi }\to {G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
169 168 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
170 rescncf ${⊢}\left[{z},{X}\right]\subseteq \left({A},{B}\right)\to \left({G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ\to \left({{G}↾}_{\left[{z},{X}\right]}\right):\left[{z},{X}\right]\underset{cn}{⟶}ℝ\right)$
171 158 169 170 sylc ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left({{G}↾}_{\left[{z},{X}\right]}\right):\left[{z},{X}\right]\underset{cn}{⟶}ℝ$
172 159 a1i ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to ℝ\subseteq ℂ$
173 162 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {G}:\left({A},{B}\right)⟶ℂ$
174 142 a1i ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left({A},{B}\right)\subseteq ℝ$
175 158 142 sstrdi ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left[{z},{X}\right]\subseteq ℝ$
176 55 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
177 55 176 dvres ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {G}:\left({A},{B}\right)⟶ℂ\right)\wedge \left(\left({A},{B}\right)\subseteq ℝ\wedge \left[{z},{X}\right]\subseteq ℝ\right)\right)\to ℝ\mathrm{D}\left({{G}↾}_{\left[{z},{X}\right]}\right)={{{G}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{z},{X}\right]\right)}$
178 172 173 174 175 177 syl22anc ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to ℝ\mathrm{D}\left({{G}↾}_{\left[{z},{X}\right]}\right)={{{G}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{z},{X}\right]\right)}$
179 iccntr ${⊢}\left({z}\in ℝ\wedge {X}\in ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{z},{X}\right]\right)=\left({z},{X}\right)$
180 144 145 179 syl2anc ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{z},{X}\right]\right)=\left({z},{X}\right)$
181 180 reseq2d ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {{{G}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{z},{X}\right]\right)}={{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}$
182 178 181 eqtrd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to ℝ\mathrm{D}\left({{G}↾}_{\left[{z},{X}\right]}\right)={{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}$
183 182 dmeqd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \mathrm{dom}{\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }=\mathrm{dom}\left({{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}\right)$
184 ioossicc ${⊢}\left({z},{X}\right)\subseteq \left[{z},{X}\right]$
185 184 158 sstrid ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left({z},{X}\right)\subseteq \left({A},{B}\right)$
186 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \mathrm{dom}{{G}}_{ℝ}^{\prime }=\left({A},{B}\right)$
187 185 186 sseqtrrd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left({z},{X}\right)\subseteq \mathrm{dom}{{G}}_{ℝ}^{\prime }$
188 ssdmres ${⊢}\left({z},{X}\right)\subseteq \mathrm{dom}{{G}}_{ℝ}^{\prime }↔\mathrm{dom}\left({{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}\right)=\left({z},{X}\right)$
189 187 188 sylib ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \mathrm{dom}\left({{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}\right)=\left({z},{X}\right)$
190 183 189 eqtrd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \mathrm{dom}{\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }=\left({z},{X}\right)$
191 143 rexrd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {z}\in {ℝ}^{*}$
192 108 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {X}\in {ℝ}^{*}$
193 50 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {X}\in ℝ$
194 143 193 148 ltled ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {z}\le {X}$
195 ubicc2 ${⊢}\left({z}\in {ℝ}^{*}\wedge {X}\in {ℝ}^{*}\wedge {z}\le {X}\right)\to {X}\in \left[{z},{X}\right]$
196 191 192 194 195 syl3anc ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {X}\in \left[{z},{X}\right]$
197 196 fvresd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left({{G}↾}_{\left[{z},{X}\right]}\right)\left({X}\right)={G}\left({X}\right)$
198 lbicc2 ${⊢}\left({z}\in {ℝ}^{*}\wedge {X}\in {ℝ}^{*}\wedge {z}\le {X}\right)\to {z}\in \left[{z},{X}\right]$
199 191 192 194 198 syl3anc ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {z}\in \left[{z},{X}\right]$
200 199 fvresd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left({{G}↾}_{\left[{z},{X}\right]}\right)\left({z}\right)={G}\left({z}\right)$
201 197 200 eqeq12d ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left(\left({{G}↾}_{\left[{z},{X}\right]}\right)\left({X}\right)=\left({{G}↾}_{\left[{z},{X}\right]}\right)\left({z}\right)↔{G}\left({X}\right)={G}\left({z}\right)\right)$
202 201 biimpar ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left({{G}↾}_{\left[{z},{X}\right]}\right)\left({X}\right)=\left({{G}↾}_{\left[{z},{X}\right]}\right)\left({z}\right)$
203 202 eqcomd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left({{G}↾}_{\left[{z},{X}\right]}\right)\left({z}\right)=\left({{G}↾}_{\left[{z},{X}\right]}\right)\left({X}\right)$
204 144 145 149 171 190 203 rolle ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \exists {w}\in \left({z},{X}\right)\phantom{\rule{.4em}{0ex}}{\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=0$
205 182 fveq1d ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left({{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}\right)\left({w}\right)$
206 fvres ${⊢}{w}\in \left({z},{X}\right)\to \left({{{G}}_{ℝ}^{\prime }↾}_{\left({z},{X}\right)}\right)\left({w}\right)={{G}}_{ℝ}^{\prime }\left({w}\right)$
207 205 206 sylan9eq ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\wedge {w}\in \left({z},{X}\right)\right)\to {\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)={{G}}_{ℝ}^{\prime }\left({w}\right)$
208 dvf ${⊢}{{G}}_{ℝ}^{\prime }:\mathrm{dom}{{G}}_{ℝ}^{\prime }⟶ℂ$
209 7 feq2d ${⊢}{\phi }\to \left({{G}}_{ℝ}^{\prime }:\mathrm{dom}{{G}}_{ℝ}^{\prime }⟶ℂ↔{{G}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ\right)$
210 208 209 mpbii ${⊢}{\phi }\to {{G}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ$
211 210 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {{G}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ$
212 211 ffnd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to {{G}}_{ℝ}^{\prime }Fn\left({A},{B}\right)$
213 212 adantr ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\wedge {w}\in \left({z},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }Fn\left({A},{B}\right)$
214 185 sselda ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\wedge {w}\in \left({z},{X}\right)\right)\to {w}\in \left({A},{B}\right)$
215 fnfvelrn ${⊢}\left({{G}}_{ℝ}^{\prime }Fn\left({A},{B}\right)\wedge {w}\in \left({A},{B}\right)\right)\to {{G}}_{ℝ}^{\prime }\left({w}\right)\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
216 213 214 215 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\wedge {w}\in \left({z},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }\left({w}\right)\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
217 207 216 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\wedge {w}\in \left({z},{X}\right)\right)\to {\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
218 eleq1 ${⊢}{\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=0\to \left({\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)\in \mathrm{ran}{{G}}_{ℝ}^{\prime }↔0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
219 217 218 syl5ibcom ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\wedge {w}\in \left({z},{X}\right)\right)\to \left({\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=0\to 0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
220 219 rexlimdva ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to \left(\exists {w}\in \left({z},{X}\right)\phantom{\rule{.4em}{0ex}}{\left({{G}↾}_{\left[{z},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=0\to 0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
221 204 220 mpd ${⊢}\left(\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\wedge {G}\left({X}\right)={G}\left({z}\right)\right)\to 0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
222 221 ex ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left({G}\left({X}\right)={G}\left({z}\right)\to 0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
223 141 222 sylbid ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left({G}\left({X}\right)-{G}\left({z}\right)=0\to 0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
224 223 necon3bd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \left(¬0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\to {G}\left({X}\right)-{G}\left({z}\right)\ne 0\right)$
225 135 224 mpd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {G}\left({X}\right)-{G}\left({z}\right)\ne 0$
226 225 ralrimiva ${⊢}{\phi }\to \forall {z}\in \left({A},{X}\right)\phantom{\rule{.4em}{0ex}}{G}\left({X}\right)-{G}\left({z}\right)\ne 0$
227 226 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \forall {z}\in \left({A},{X}\right)\phantom{\rule{.4em}{0ex}}{G}\left({X}\right)-{G}\left({z}\right)\ne 0$
228 134 227 112 rspcdva ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}\left({X}\right)-{G}\left({R}\right)\ne 0$
229 126 131 228 divcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\in ℂ$
230 35 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {C}\in ℂ$
231 229 230 subcld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\in ℂ$
232 231 abscld ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|\in ℝ$
233 38 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {E}\in ℝ$
234 116 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {D}\in {ℝ}^{*}$
235 117 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {X}<{D}$
236 iccssioo ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\right)\wedge \left({A}<{R}\wedge {X}<{D}\right)\right)\to \left[{R},{X}\right]\subseteq \left({A},{D}\right)$
237 107 234 99 235 236 syl22anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left[{R},{X}\right]\subseteq \left({A},{D}\right)$
238 20 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({A},{D}\right)\subseteq \left({A},{B}\right)$
239 237 238 sstrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left[{R},{X}\right]\subseteq \left({A},{B}\right)$
240 fss ${⊢}\left({F}:\left({A},{B}\right)⟶ℝ\wedge ℝ\subseteq ℂ\right)\to {F}:\left({A},{B}\right)⟶ℂ$
241 4 159 240 sylancl ${⊢}{\phi }\to {F}:\left({A},{B}\right)⟶ℂ$
242 dvcn ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {F}:\left({A},{B}\right)⟶ℂ\wedge \left({A},{B}\right)\subseteq ℝ\right)\wedge \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)\right)\to {F}:\left({A},{B}\right)\underset{cn}{⟶}ℂ$
243 160 241 163 6 242 syl31anc ${⊢}{\phi }\to {F}:\left({A},{B}\right)\underset{cn}{⟶}ℂ$
244 cncffvrn ${⊢}\left(ℝ\subseteq ℂ\wedge {F}:\left({A},{B}\right)\underset{cn}{⟶}ℂ\right)\to \left({F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ↔{F}:\left({A},{B}\right)⟶ℝ\right)$
245 159 243 244 sylancr ${⊢}{\phi }\to \left({F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ↔{F}:\left({A},{B}\right)⟶ℝ\right)$
246 4 245 mpbird ${⊢}{\phi }\to {F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
247 246 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
248 rescncf ${⊢}\left[{R},{X}\right]\subseteq \left({A},{B}\right)\to \left({F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ\to \left({{F}↾}_{\left[{R},{X}\right]}\right):\left[{R},{X}\right]\underset{cn}{⟶}ℝ\right)$
249 239 247 248 sylc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({{F}↾}_{\left[{R},{X}\right]}\right):\left[{R},{X}\right]\underset{cn}{⟶}ℝ$
250 168 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
251 rescncf ${⊢}\left[{R},{X}\right]\subseteq \left({A},{B}\right)\to \left({G}:\left({A},{B}\right)\underset{cn}{⟶}ℝ\to \left({{G}↾}_{\left[{R},{X}\right]}\right):\left[{R},{X}\right]\underset{cn}{⟶}ℝ\right)$
252 239 250 251 sylc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({{G}↾}_{\left[{R},{X}\right]}\right):\left[{R},{X}\right]\underset{cn}{⟶}ℝ$
253 159 a1i ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to ℝ\subseteq ℂ$
254 241 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {F}:\left({A},{B}\right)⟶ℂ$
255 142 a1i ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({A},{B}\right)\subseteq ℝ$
256 iccssre ${⊢}\left({R}\in ℝ\wedge {X}\in ℝ\right)\to \left[{R},{X}\right]\subseteq ℝ$
257 72 100 256 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left[{R},{X}\right]\subseteq ℝ$
258 55 176 dvres ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {F}:\left({A},{B}\right)⟶ℂ\right)\wedge \left(\left({A},{B}\right)\subseteq ℝ\wedge \left[{R},{X}\right]\subseteq ℝ\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{\left[{R},{X}\right]}\right)={{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)}$
259 253 254 255 257 258 syl22anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{\left[{R},{X}\right]}\right)={{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)}$
260 iccntr ${⊢}\left({R}\in ℝ\wedge {X}\in ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)=\left({R},{X}\right)$
261 72 100 260 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)=\left({R},{X}\right)$
262 261 reseq2d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}$
263 259 262 eqtrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{\left[{R},{X}\right]}\right)={{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}$
264 263 dmeqd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}{\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }=\mathrm{dom}\left({{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)$
265 67 72 99 ltled ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {A}\le {R}$
266 iooss1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\le {R}\right)\to \left({R},{X}\right)\subseteq \left({A},{X}\right)$
267 107 265 266 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R},{X}\right)\subseteq \left({A},{X}\right)$
268 118 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {X}\le {D}$
269 iooss2 ${⊢}\left({D}\in {ℝ}^{*}\wedge {X}\le {D}\right)\to \left({A},{X}\right)\subseteq \left({A},{D}\right)$
270 234 268 269 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({A},{X}\right)\subseteq \left({A},{D}\right)$
271 267 270 sstrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R},{X}\right)\subseteq \left({A},{D}\right)$
272 271 238 sstrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R},{X}\right)\subseteq \left({A},{B}\right)$
273 6 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
274 272 273 sseqtrrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R},{X}\right)\subseteq \mathrm{dom}{{F}}_{ℝ}^{\prime }$
275 ssdmres ${⊢}\left({R},{X}\right)\subseteq \mathrm{dom}{{F}}_{ℝ}^{\prime }↔\mathrm{dom}\left({{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)=\left({R},{X}\right)$
276 274 275 sylib ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}\left({{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)=\left({R},{X}\right)$
277 264 276 eqtrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}{\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }=\left({R},{X}\right)$
278 162 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {G}:\left({A},{B}\right)⟶ℂ$
279 55 176 dvres ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {G}:\left({A},{B}\right)⟶ℂ\right)\wedge \left(\left({A},{B}\right)\subseteq ℝ\wedge \left[{R},{X}\right]\subseteq ℝ\right)\right)\to ℝ\mathrm{D}\left({{G}↾}_{\left[{R},{X}\right]}\right)={{{G}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)}$
280 253 278 255 257 279 syl22anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to ℝ\mathrm{D}\left({{G}↾}_{\left[{R},{X}\right]}\right)={{{G}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)}$
281 261 reseq2d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {{{G}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{R},{X}\right]\right)}={{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}$
282 280 281 eqtrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to ℝ\mathrm{D}\left({{G}↾}_{\left[{R},{X}\right]}\right)={{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}$
283 282 dmeqd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}{\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }=\mathrm{dom}\left({{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)$
284 7 adantr ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}{{G}}_{ℝ}^{\prime }=\left({A},{B}\right)$
285 272 284 sseqtrrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({R},{X}\right)\subseteq \mathrm{dom}{{G}}_{ℝ}^{\prime }$
286 ssdmres ${⊢}\left({R},{X}\right)\subseteq \mathrm{dom}{{G}}_{ℝ}^{\prime }↔\mathrm{dom}\left({{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)=\left({R},{X}\right)$
287 285 286 sylib ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}\left({{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)=\left({R},{X}\right)$
288 283 287 eqtrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \mathrm{dom}{\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }=\left({R},{X}\right)$
289 72 100 106 249 252 277 288 cmvth ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \exists {w}\in \left({R},{X}\right)\phantom{\rule{.4em}{0ex}}\left(\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left(\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)$
290 72 rexrd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\in {ℝ}^{*}$
291 290 adantr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {R}\in {ℝ}^{*}$
292 108 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {X}\in {ℝ}^{*}$
293 72 100 106 ltled ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {R}\le {X}$
294 293 adantr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {R}\le {X}$
295 ubicc2 ${⊢}\left({R}\in {ℝ}^{*}\wedge {X}\in {ℝ}^{*}\wedge {R}\le {X}\right)\to {X}\in \left[{R},{X}\right]$
296 291 292 294 295 syl3anc ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {X}\in \left[{R},{X}\right]$
297 296 fvresd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)={F}\left({X}\right)$
298 lbicc2 ${⊢}\left({R}\in {ℝ}^{*}\wedge {X}\in {ℝ}^{*}\wedge {R}\le {X}\right)\to {R}\in \left[{R},{X}\right]$
299 291 292 294 298 syl3anc ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {R}\in \left[{R},{X}\right]$
300 299 fvresd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)={F}\left({R}\right)$
301 297 300 oveq12d ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)={F}\left({X}\right)-{F}\left({R}\right)$
302 282 fveq1d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left({{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)\left({w}\right)$
303 fvres ${⊢}{w}\in \left({R},{X}\right)\to \left({{{G}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)\left({w}\right)={{G}}_{ℝ}^{\prime }\left({w}\right)$
304 302 303 sylan9eq ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)={{G}}_{ℝ}^{\prime }\left({w}\right)$
305 301 304 oveq12d ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left({F}\left({X}\right)-{F}\left({R}\right)\right){{G}}_{ℝ}^{\prime }\left({w}\right)$
306 296 fvresd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)={G}\left({X}\right)$
307 299 fvresd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)={G}\left({R}\right)$
308 306 307 oveq12d ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)={G}\left({X}\right)-{G}\left({R}\right)$
309 263 fveq1d ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to {\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left({{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)\left({w}\right)$
310 fvres ${⊢}{w}\in \left({R},{X}\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({R},{X}\right)}\right)\left({w}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)$
311 309 310 sylan9eq ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)$
312 308 311 oveq12d ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left({G}\left({X}\right)-{G}\left({R}\right)\right){{F}}_{ℝ}^{\prime }\left({w}\right)$
313 131 adantr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {G}\left({X}\right)-{G}\left({R}\right)\in ℂ$
314 dvf ${⊢}{{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℂ$
315 6 feq2d ${⊢}{\phi }\to \left({{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℂ↔{{F}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ\right)$
316 314 315 mpbii ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ$
317 316 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{F}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ$
318 272 sselda ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {w}\in \left({A},{B}\right)$
319 317 318 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{F}}_{ℝ}^{\prime }\left({w}\right)\in ℂ$
320 313 319 mulcomd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({G}\left({X}\right)-{G}\left({R}\right)\right){{F}}_{ℝ}^{\prime }\left({w}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)\left({G}\left({X}\right)-{G}\left({R}\right)\right)$
321 312 320 eqtrd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)\left({G}\left({X}\right)-{G}\left({R}\right)\right)$
322 305 321 eqeq12d ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\left(\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left(\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)↔\left({F}\left({X}\right)-{F}\left({R}\right)\right){{G}}_{ℝ}^{\prime }\left({w}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)\left({G}\left({X}\right)-{G}\left({R}\right)\right)\right)$
323 126 adantr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {F}\left({X}\right)-{F}\left({R}\right)\in ℂ$
324 210 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ$
325 324 318 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }\left({w}\right)\in ℂ$
326 228 adantr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {G}\left({X}\right)-{G}\left({R}\right)\ne 0$
327 11 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to ¬0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
328 324 ffnd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }Fn\left({A},{B}\right)$
329 328 318 215 syl2anc ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }\left({w}\right)\in \mathrm{ran}{{G}}_{ℝ}^{\prime }$
330 eleq1 ${⊢}{{G}}_{ℝ}^{\prime }\left({w}\right)=0\to \left({{G}}_{ℝ}^{\prime }\left({w}\right)\in \mathrm{ran}{{G}}_{ℝ}^{\prime }↔0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
331 329 330 syl5ibcom ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left({{G}}_{ℝ}^{\prime }\left({w}\right)=0\to 0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\right)$
332 331 necon3bd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(¬0\in \mathrm{ran}{{G}}_{ℝ}^{\prime }\to {{G}}_{ℝ}^{\prime }\left({w}\right)\ne 0\right)$
333 327 332 mpd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {{G}}_{ℝ}^{\prime }\left({w}\right)\ne 0$
334 323 313 319 325 326 333 divmuleqd ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}↔\left({F}\left({X}\right)-{F}\left({R}\right)\right){{G}}_{ℝ}^{\prime }\left({w}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)\left({G}\left({X}\right)-{G}\left({R}\right)\right)\right)$
335 322 334 bitr4d ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\left(\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left(\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)↔\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)$
336 335 rexbidva ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left(\exists {w}\in \left({R},{X}\right)\phantom{\rule{.4em}{0ex}}\left(\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{F}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{G}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)=\left(\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({X}\right)-\left({{G}↾}_{\left[{R},{X}\right]}\right)\left({R}\right)\right){\left({{F}↾}_{\left[{R},{X}\right]}\right)}_{ℝ}^{\prime }\left({w}\right)↔\exists {w}\in \left({R},{X}\right)\phantom{\rule{.4em}{0ex}}\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)$
337 289 336 mpbid ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \exists {w}\in \left({R},{X}\right)\phantom{\rule{.4em}{0ex}}\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}$
338 fveq2 ${⊢}{t}={w}\to {{F}}_{ℝ}^{\prime }\left({t}\right)={{F}}_{ℝ}^{\prime }\left({w}\right)$
339 fveq2 ${⊢}{t}={w}\to {{G}}_{ℝ}^{\prime }\left({t}\right)={{G}}_{ℝ}^{\prime }\left({w}\right)$
340 338 339 oveq12d ${⊢}{t}={w}\to \frac{{{F}}_{ℝ}^{\prime }\left({t}\right)}{{{G}}_{ℝ}^{\prime }\left({t}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}$
341 340 fvoveq1d ${⊢}{t}={w}\to \left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({t}\right)}{{{G}}_{ℝ}^{\prime }\left({t}\right)}\right)-{C}\right|=\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)-{C}\right|$
342 341 breq1d ${⊢}{t}={w}\to \left(\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({t}\right)}{{{G}}_{ℝ}^{\prime }\left({t}\right)}\right)-{C}\right|<{E}↔\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)-{C}\right|<{E}\right)$
343 17 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \forall {t}\in \left({A},{D}\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({t}\right)}{{{G}}_{ℝ}^{\prime }\left({t}\right)}\right)-{C}\right|<{E}$
344 271 sselda ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to {w}\in \left({A},{D}\right)$
345 342 343 344 rspcdva ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)-{C}\right|<{E}$
346 fvoveq1 ${⊢}\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|=\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)-{C}\right|$
347 346 breq1d ${⊢}\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\to \left(\left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|<{E}↔\left|\left(\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\right)-{C}\right|<{E}\right)$
348 345 347 syl5ibrcom ${⊢}\left(\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\wedge {w}\in \left({R},{X}\right)\right)\to \left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|<{E}\right)$
349 348 rexlimdva ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left(\exists {w}\in \left({R},{X}\right)\phantom{\rule{.4em}{0ex}}\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}=\frac{{{F}}_{ℝ}^{\prime }\left({w}\right)}{{{G}}_{ℝ}^{\prime }\left({w}\right)}\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|<{E}\right)$
350 337 349 mpd ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|<{E}$
351 232 233 350 ltled ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|\le {E}$
352 fveq2 ${⊢}{u}={R}\to {F}\left({u}\right)={F}\left({R}\right)$
353 352 oveq2d ${⊢}{u}={R}\to {F}\left({X}\right)-{F}\left({u}\right)={F}\left({X}\right)-{F}\left({R}\right)$
354 fveq2 ${⊢}{u}={R}\to {G}\left({u}\right)={G}\left({R}\right)$
355 354 oveq2d ${⊢}{u}={R}\to {G}\left({X}\right)-{G}\left({u}\right)={G}\left({X}\right)-{G}\left({R}\right)$
356 353 355 oveq12d ${⊢}{u}={R}\to \frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}=\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}$
357 356 fvoveq1d ${⊢}{u}={R}\to \left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|=\left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|$
358 357 breq1d ${⊢}{u}={R}\to \left(\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}↔\left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|\le {E}\right)$
359 358 rspcev ${⊢}\left({R}\in \left(\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\right)\wedge \left|\left(\frac{{F}\left({X}\right)-{F}\left({R}\right)}{{G}\left({X}\right)-{G}\left({R}\right)}\right)-{C}\right|\le {E}\right)\to \exists {u}\in \left(\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}$
360 113 351 359 syl2anc ${⊢}\left({\phi }\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \exists {u}\in \left(\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}$
361 360 adantlr ${⊢}\left(\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \exists {u}\in \left(\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}$
362 ssrexv ${⊢}\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\subseteq {v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\to \left(\exists {u}\in \left(\left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\right)\cap \left({A},{X}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
363 66 361 362 syl2imc ${⊢}\left(\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {r}<{X}-{A}\right)\right)\to \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
364 363 anassrs ${⊢}\left(\left(\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {r}<{X}-{A}\right)\to \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
365 364 expimpd ${⊢}\left(\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\left({r}<{X}-{A}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\right)\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
366 365 rexlimdva ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({r}<{X}-{A}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){r}\subseteq {v}\right)\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
367 58 366 mpd ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}$
368 inss2 ${⊢}{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\subseteq \left({A},{X}\right)\setminus \left\{{A}\right\}$
369 difss ${⊢}\left({A},{X}\right)\setminus \left\{{A}\right\}\subseteq \left({A},{X}\right)$
370 368 369 sstri ${⊢}{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\subseteq \left({A},{X}\right)$
371 370 sseli ${⊢}{u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\to {u}\in \left({A},{X}\right)$
372 fveq2 ${⊢}{z}={u}\to {F}\left({z}\right)={F}\left({u}\right)$
373 372 oveq2d ${⊢}{z}={u}\to {F}\left({X}\right)-{F}\left({z}\right)={F}\left({X}\right)-{F}\left({u}\right)$
374 fveq2 ${⊢}{z}={u}\to {G}\left({z}\right)={G}\left({u}\right)$
375 374 oveq2d ${⊢}{z}={u}\to {G}\left({X}\right)-{G}\left({z}\right)={G}\left({X}\right)-{G}\left({u}\right)$
376 373 375 oveq12d ${⊢}{z}={u}\to \frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}=\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}$
377 eqid ${⊢}\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)=\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)$
378 ovex ${⊢}\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\in \mathrm{V}$
379 376 377 378 fvmpt ${⊢}{u}\in \left({A},{X}\right)\to \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)=\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}$
380 379 fvoveq1d ${⊢}{u}\in \left({A},{X}\right)\to \left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|=\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|$
381 380 breq1d ${⊢}{u}\in \left({A},{X}\right)\to \left(\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}↔\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
382 371 381 syl ${⊢}{u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\to \left(\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}↔\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}\right)$
383 382 rexbiia ${⊢}\exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}↔\exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left(\frac{{F}\left({X}\right)-{F}\left({u}\right)}{{G}\left({X}\right)-{G}\left({u}\right)}\right)-{C}\right|\le {E}$
384 367 383 sylibr ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to \exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}$
385 ovex ${⊢}\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\in \mathrm{V}$
386 385 377 fnmpti ${⊢}\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)Fn\left({A},{X}\right)$
387 fvoveq1 ${⊢}{x}=\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)\to \left|{x}-{C}\right|=\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|$
388 387 breq1d ${⊢}{x}=\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)\to \left(\left|{x}-{C}\right|\le {E}↔\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}\right)$
389 388 rexima ${⊢}\left(\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)Fn\left({A},{X}\right)\wedge {v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\subseteq \left({A},{X}\right)\right)\to \left(\exists {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}\left|{x}-{C}\right|\le {E}↔\exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}\right)$
390 386 370 389 mp2an ${⊢}\exists {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}\left|{x}-{C}\right|\le {E}↔\exists {u}\in \left({v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left({u}\right)-{C}\right|\le {E}$
391 384 390 sylibr ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to \exists {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}\left|{x}-{C}\right|\le {E}$
392 dfrex2 ${⊢}\exists {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}\left|{x}-{C}\right|\le {E}↔¬\forall {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}¬\left|{x}-{C}\right|\le {E}$
393 391 392 sylib ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to ¬\forall {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}¬\left|{x}-{C}\right|\le {E}$
394 ssrab ${⊢}\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}↔\left(\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq ℂ\wedge \forall {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}¬\left|{x}-{C}\right|\le {E}\right)$
395 394 simprbi ${⊢}\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \forall {x}\in \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\phantom{\rule{.4em}{0ex}}¬\left|{x}-{C}\right|\le {E}$
396 393 395 nsyl ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {v}\right)\right)\to ¬\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}$
397 396 expr ${⊢}\left({\phi }\wedge {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \left({A}\in {v}\to ¬\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)$
398 397 ralrimiva ${⊢}{\phi }\to \forall {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\to ¬\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)$
399 ralinexa ${⊢}\forall {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\to ¬\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)↔¬\exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)$
400 398 399 sylib ${⊢}{\phi }\to ¬\exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)$
401 fvoveq1 ${⊢}{x}=\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\to \left|{x}-{C}\right|=\left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|$
402 401 breq1d ${⊢}{x}=\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\to \left(\left|{x}-{C}\right|\le {E}↔\left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\le {E}\right)$
403 402 notbid ${⊢}{x}=\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\to \left(¬\left|{x}-{C}\right|\le {E}↔¬\left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\le {E}\right)$
404 403 elrab3 ${⊢}\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in ℂ\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}↔¬\left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\le {E}\right)$
405 33 404 syl ${⊢}{\phi }\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}↔¬\left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\le {E}\right)$
406 eleq2 ${⊢}{u}=\left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in {u}↔\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)$
407 sseq2 ${⊢}{u}=\left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \left(\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}↔\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)$
408 407 anbi2d ${⊢}{u}=\left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \left(\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}\right)↔\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)\right)$
409 408 rexbidv ${⊢}{u}=\left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \left(\exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}\right)↔\exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)\right)$
410 406 409 imbi12d ${⊢}{u}=\left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \left(\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in {u}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}\right)\right)↔\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)\right)\right)$
411 23 adantr ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {F}\left({X}\right)\in ℂ$
412 4 ffvelrnda ${⊢}\left({\phi }\wedge {z}\in \left({A},{B}\right)\right)\to {F}\left({z}\right)\in ℝ$
413 137 412 syldan ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {F}\left({z}\right)\in ℝ$
414 413 recnd ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {F}\left({z}\right)\in ℂ$
415 411 414 subcld ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {F}\left({X}\right)-{F}\left({z}\right)\in ℂ$
416 136 140 subcld ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {G}\left({X}\right)-{G}\left({z}\right)\in ℂ$
417 eldifsn ${⊢}{G}\left({X}\right)-{G}\left({z}\right)\in \left(ℂ\setminus \left\{0\right\}\right)↔\left({G}\left({X}\right)-{G}\left({z}\right)\in ℂ\wedge {G}\left({X}\right)-{G}\left({z}\right)\ne 0\right)$
418 416 225 417 sylanbrc ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to {G}\left({X}\right)-{G}\left({z}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
419 ssidd ${⊢}{\phi }\to ℂ\subseteq ℂ$
420 difss ${⊢}ℂ\setminus \left\{0\right\}\subseteq ℂ$
421 420 a1i ${⊢}{\phi }\to ℂ\setminus \left\{0\right\}\subseteq ℂ$
422 55 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
423 cnex ${⊢}ℂ\in \mathrm{V}$
424 423 difexi ${⊢}ℂ\setminus \left\{0\right\}\in \mathrm{V}$
425 txrest ${⊢}\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\right)\wedge \left(ℂ\in \mathrm{V}\wedge ℂ\setminus \left\{0\right\}\in \mathrm{V}\right)\right)\to \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}\left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)$
426 422 422 423 424 425 mp4an ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}\left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)$
427 unicntop ${⊢}ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
428 427 restid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
429 422 428 ax-mp ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
430 429 oveq1i ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)$
431 426 430 eqtr2i ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}\left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)$
432 23 subid1d ${⊢}{\phi }\to {F}\left({X}\right)-0={F}\left({X}\right)$
433 txtopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ×ℂ\right)$
434 422 422 433 mp2an ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ×ℂ\right)$
435 434 toponrestid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}\left(ℂ×ℂ\right)$
436 limcresi ${⊢}\left({z}\in ℝ⟼{F}\left({X}\right)\right){lim}_{ℂ}{A}\subseteq \left({\left({z}\in ℝ⟼{F}\left({X}\right)\right)↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}$
437 ioossre ${⊢}\left({A},{X}\right)\subseteq ℝ$
438 resmpt ${⊢}\left({A},{X}\right)\subseteq ℝ\to {\left({z}\in ℝ⟼{F}\left({X}\right)\right)↾}_{\left({A},{X}\right)}=\left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)\right)$
439 437 438 ax-mp ${⊢}{\left({z}\in ℝ⟼{F}\left({X}\right)\right)↾}_{\left({A},{X}\right)}=\left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)\right)$
440 439 oveq1i ${⊢}\left({\left({z}\in ℝ⟼{F}\left({X}\right)\right)↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}=\left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)\right){lim}_{ℂ}{A}$
441 436 440 sseqtri ${⊢}\left({z}\in ℝ⟼{F}\left({X}\right)\right){lim}_{ℂ}{A}\subseteq \left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)\right){lim}_{ℂ}{A}$
442 cncfmptc ${⊢}\left({F}\left({X}\right)\in ℝ\wedge ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to \left({z}\in ℝ⟼{F}\left({X}\right)\right):ℝ\underset{cn}{⟶}ℝ$
443 22 160 160 442 syl3anc ${⊢}{\phi }\to \left({z}\in ℝ⟼{F}\left({X}\right)\right):ℝ\underset{cn}{⟶}ℝ$
444 eqidd ${⊢}{z}={A}\to {F}\left({X}\right)={F}\left({X}\right)$
445 443 1 444 cnmptlimc ${⊢}{\phi }\to {F}\left({X}\right)\in \left(\left({z}\in ℝ⟼{F}\left({X}\right)\right){lim}_{ℂ}{A}\right)$
446 441 445 sseldi ${⊢}{\phi }\to {F}\left({X}\right)\in \left(\left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)\right){lim}_{ℂ}{A}\right)$
447 limcresi ${⊢}{F}{lim}_{ℂ}{A}\subseteq \left({{F}↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}$
448 4 121 feqresmpt ${⊢}{\phi }\to {{F}↾}_{\left({A},{X}\right)}=\left({z}\in \left({A},{X}\right)⟼{F}\left({z}\right)\right)$
449 448 oveq1d ${⊢}{\phi }\to \left({{F}↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}=\left({z}\in \left({A},{X}\right)⟼{F}\left({z}\right)\right){lim}_{ℂ}{A}$
450 447 449 sseqtrid ${⊢}{\phi }\to {F}{lim}_{ℂ}{A}\subseteq \left({z}\in \left({A},{X}\right)⟼{F}\left({z}\right)\right){lim}_{ℂ}{A}$
451 450 8 sseldd ${⊢}{\phi }\to 0\in \left(\left({z}\in \left({A},{X}\right)⟼{F}\left({z}\right)\right){lim}_{ℂ}{A}\right)$
452 55 subcn ${⊢}-\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
453 0cn ${⊢}0\in ℂ$
454 opelxpi ${⊢}\left({F}\left({X}\right)\in ℂ\wedge 0\in ℂ\right)\to ⟨{F}\left({X}\right),0⟩\in \left(ℂ×ℂ\right)$
455 23 453 454 sylancl ${⊢}{\phi }\to ⟨{F}\left({X}\right),0⟩\in \left(ℂ×ℂ\right)$
456 434 toponunii ${⊢}ℂ×ℂ=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
457 456 cncnpi ${⊢}\left(-\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ⟨{F}\left({X}\right),0⟩\in \left(ℂ×ℂ\right)\right)\to -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(⟨{F}\left({X}\right),0⟩\right)$
458 452 455 457 sylancr ${⊢}{\phi }\to -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(⟨{F}\left({X}\right),0⟩\right)$
459 411 414 419 419 55 435 446 451 458 limccnp2 ${⊢}{\phi }\to {F}\left({X}\right)-0\in \left(\left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)-{F}\left({z}\right)\right){lim}_{ℂ}{A}\right)$
460 432 459 eqeltrrd ${⊢}{\phi }\to {F}\left({X}\right)\in \left(\left({z}\in \left({A},{X}\right)⟼{F}\left({X}\right)-{F}\left({z}\right)\right){lim}_{ℂ}{A}\right)$
461 25 subid1d ${⊢}{\phi }\to {G}\left({X}\right)-0={G}\left({X}\right)$
462 limcresi ${⊢}\left({z}\in ℝ⟼{G}\left({X}\right)\right){lim}_{ℂ}{A}\subseteq \left({\left({z}\in ℝ⟼{G}\left({X}\right)\right)↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}$
463 resmpt ${⊢}\left({A},{X}\right)\subseteq ℝ\to {\left({z}\in ℝ⟼{G}\left({X}\right)\right)↾}_{\left({A},{X}\right)}=\left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)\right)$
464 437 463 ax-mp ${⊢}{\left({z}\in ℝ⟼{G}\left({X}\right)\right)↾}_{\left({A},{X}\right)}=\left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)\right)$
465 464 oveq1i ${⊢}\left({\left({z}\in ℝ⟼{G}\left({X}\right)\right)↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}=\left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)\right){lim}_{ℂ}{A}$
466 462 465 sseqtri ${⊢}\left({z}\in ℝ⟼{G}\left({X}\right)\right){lim}_{ℂ}{A}\subseteq \left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)\right){lim}_{ℂ}{A}$
467 cncfmptc ${⊢}\left({G}\left({X}\right)\in ℝ\wedge ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to \left({z}\in ℝ⟼{G}\left({X}\right)\right):ℝ\underset{cn}{⟶}ℝ$
468 24 160 160 467 syl3anc ${⊢}{\phi }\to \left({z}\in ℝ⟼{G}\left({X}\right)\right):ℝ\underset{cn}{⟶}ℝ$
469 eqidd ${⊢}{z}={A}\to {G}\left({X}\right)={G}\left({X}\right)$
470 468 1 469 cnmptlimc ${⊢}{\phi }\to {G}\left({X}\right)\in \left(\left({z}\in ℝ⟼{G}\left({X}\right)\right){lim}_{ℂ}{A}\right)$
471 466 470 sseldi ${⊢}{\phi }\to {G}\left({X}\right)\in \left(\left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)\right){lim}_{ℂ}{A}\right)$
472 limcresi ${⊢}{G}{lim}_{ℂ}{A}\subseteq \left({{G}↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}$
473 5 121 feqresmpt ${⊢}{\phi }\to {{G}↾}_{\left({A},{X}\right)}=\left({z}\in \left({A},{X}\right)⟼{G}\left({z}\right)\right)$
474 473 oveq1d ${⊢}{\phi }\to \left({{G}↾}_{\left({A},{X}\right)}\right){lim}_{ℂ}{A}=\left({z}\in \left({A},{X}\right)⟼{G}\left({z}\right)\right){lim}_{ℂ}{A}$
475 472 474 sseqtrid ${⊢}{\phi }\to {G}{lim}_{ℂ}{A}\subseteq \left({z}\in \left({A},{X}\right)⟼{G}\left({z}\right)\right){lim}_{ℂ}{A}$
476 475 9 sseldd ${⊢}{\phi }\to 0\in \left(\left({z}\in \left({A},{X}\right)⟼{G}\left({z}\right)\right){lim}_{ℂ}{A}\right)$
477 opelxpi ${⊢}\left({G}\left({X}\right)\in ℂ\wedge 0\in ℂ\right)\to ⟨{G}\left({X}\right),0⟩\in \left(ℂ×ℂ\right)$
478 25 453 477 sylancl ${⊢}{\phi }\to ⟨{G}\left({X}\right),0⟩\in \left(ℂ×ℂ\right)$
479 456 cncnpi ${⊢}\left(-\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ⟨{G}\left({X}\right),0⟩\in \left(ℂ×ℂ\right)\right)\to -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(⟨{G}\left({X}\right),0⟩\right)$
480 452 478 479 sylancr ${⊢}{\phi }\to -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(⟨{G}\left({X}\right),0⟩\right)$
481 136 140 419 419 55 435 471 476 480 limccnp2 ${⊢}{\phi }\to {G}\left({X}\right)-0\in \left(\left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)-{G}\left({z}\right)\right){lim}_{ℂ}{A}\right)$
482 461 481 eqeltrrd ${⊢}{\phi }\to {G}\left({X}\right)\in \left(\left({z}\in \left({A},{X}\right)⟼{G}\left({X}\right)-{G}\left({z}\right)\right){lim}_{ℂ}{A}\right)$
483 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)$
484 55 483 divcn ${⊢}÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
485 eldifsn ${⊢}{G}\left({X}\right)\in \left(ℂ\setminus \left\{0\right\}\right)↔\left({G}\left({X}\right)\in ℂ\wedge {G}\left({X}\right)\ne 0\right)$
486 25 32 485 sylanbrc ${⊢}{\phi }\to {G}\left({X}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
487 23 486 opelxpd ${⊢}{\phi }\to ⟨{F}\left({X}\right),{G}\left({X}\right)⟩\in \left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)$
488 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge ℂ\setminus \left\{0\right\}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\in \mathrm{TopOn}\left(ℂ\setminus \left\{0\right\}\right)$
489 422 420 488 mp2an ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\in \mathrm{TopOn}\left(ℂ\setminus \left\{0\right\}\right)$
490 txtopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\in \mathrm{TopOn}\left(ℂ\setminus \left\{0\right\}\right)\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\in \mathrm{TopOn}\left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)$
491 422 489 490 mp2an ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\in \mathrm{TopOn}\left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)$
492 491 toponunii ${⊢}ℂ×\left(ℂ\setminus \left\{0\right\}\right)=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)$
493 492 cncnpi ${⊢}\left(÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ⟨{F}\left({X}\right),{G}\left({X}\right)⟩\in \left(ℂ×\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\to ÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(⟨{F}\left({X}\right),{G}\left({X}\right)⟩\right)$
494 484 487 493 sylancr ${⊢}{\phi }\to ÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(⟨{F}\left({X}\right),{G}\left({X}\right)⟩\right)$
495 415 418 419 421 55 431 460 482 494 limccnp2 ${⊢}{\phi }\to \frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left(\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right){lim}_{ℂ}{A}\right)$
496 415 416 225 divcld ${⊢}\left({\phi }\wedge {z}\in \left({A},{X}\right)\right)\to \frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\in ℂ$
497 496 fmpttd ${⊢}{\phi }\to \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right):\left({A},{X}\right)⟶ℂ$
498 437 159 sstri ${⊢}\left({A},{X}\right)\subseteq ℂ$
499 498 a1i ${⊢}{\phi }\to \left({A},{X}\right)\subseteq ℂ$
500 497 499 74 55 ellimc2 ${⊢}{\phi }\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left(\left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right){lim}_{ℂ}{A}\right)↔\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in ℂ\wedge \forall {u}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in {u}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}\right)\right)\right)\right)$
501 495 500 mpbid ${⊢}{\phi }\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in ℂ\wedge \forall {u}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in {u}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}\right)\right)\right)$
502 501 simprd ${⊢}{\phi }\to \forall {u}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in {u}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq {u}\right)\right)$
503 notrab ${⊢}ℂ\setminus \left\{{x}\in ℂ|\left|{x}-{C}\right|\le {E}\right\}=\left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}$
504 76 cnmetdval ${⊢}\left({C}\in ℂ\wedge {x}\in ℂ\right)\to {C}\left(\mathrm{abs}\circ -\right){x}=\left|{C}-{x}\right|$
505 abssub ${⊢}\left({C}\in ℂ\wedge {x}\in ℂ\right)\to \left|{C}-{x}\right|=\left|{x}-{C}\right|$
506 504 505 eqtrd ${⊢}\left({C}\in ℂ\wedge {x}\in ℂ\right)\to {C}\left(\mathrm{abs}\circ -\right){x}=\left|{x}-{C}\right|$
507 35 506 sylan ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {C}\left(\mathrm{abs}\circ -\right){x}=\left|{x}-{C}\right|$
508 507 breq1d ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left({C}\left(\mathrm{abs}\circ -\right){x}\le {E}↔\left|{x}-{C}\right|\le {E}\right)$
509 508 rabbidva ${⊢}{\phi }\to \left\{{x}\in ℂ|{C}\left(\mathrm{abs}\circ -\right){x}\le {E}\right\}=\left\{{x}\in ℂ|\left|{x}-{C}\right|\le {E}\right\}$
510 42 a1i ${⊢}{\phi }\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
511 38 rexrd ${⊢}{\phi }\to {E}\in {ℝ}^{*}$
512 eqid ${⊢}\left\{{x}\in ℂ|{C}\left(\mathrm{abs}\circ -\right){x}\le {E}\right\}=\left\{{x}\in ℂ|{C}\left(\mathrm{abs}\circ -\right){x}\le {E}\right\}$
513 56 512 blcld ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {C}\in ℂ\wedge {E}\in {ℝ}^{*}\right)\to \left\{{x}\in ℂ|{C}\left(\mathrm{abs}\circ -\right){x}\le {E}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
514 510 35 511 513 syl3anc ${⊢}{\phi }\to \left\{{x}\in ℂ|{C}\left(\mathrm{abs}\circ -\right){x}\le {E}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
515 509 514 eqeltrrd ${⊢}{\phi }\to \left\{{x}\in ℂ|\left|{x}-{C}\right|\le {E}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
516 427 cldopn ${⊢}\left\{{x}\in ℂ|\left|{x}-{C}\right|\le {E}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to ℂ\setminus \left\{{x}\in ℂ|\left|{x}-{C}\right|\le {E}\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
517 515 516 syl ${⊢}{\phi }\to ℂ\setminus \left\{{x}\in ℂ|\left|{x}-{C}\right|\le {E}\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
518 503 517 eqeltrrid ${⊢}{\phi }\to \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
519 410 502 518 rspcdva ${⊢}{\phi }\to \left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\in \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)\right)$
520 405 519 sylbird ${⊢}{\phi }\to \left(¬\left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\le {E}\to \exists {v}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\phantom{\rule{.4em}{0ex}}\left({A}\in {v}\wedge \left({z}\in \left({A},{X}\right)⟼\frac{{F}\left({X}\right)-{F}\left({z}\right)}{{G}\left({X}\right)-{G}\left({z}\right)}\right)\left[{v}\cap \left(\left({A},{X}\right)\setminus \left\{{A}\right\}\right)\right]\subseteq \left\{{x}\in ℂ|¬\left|{x}-{C}\right|\le {E}\right\}\right)\right)$
521 400 520 mt3d ${⊢}{\phi }\to \left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|\le {E}$
522 38 recnd ${⊢}{\phi }\to {E}\in ℂ$
523 522 mulid2d ${⊢}{\phi }\to 1{E}={E}$
524 1red ${⊢}{\phi }\to 1\in ℝ$
525 1lt2 ${⊢}1<2$
526 525 a1i ${⊢}{\phi }\to 1<2$
527 524 40 13 526 ltmul1dd ${⊢}{\phi }\to 1{E}<2{E}$
528 523 527 eqbrtrrd ${⊢}{\phi }\to {E}<2{E}$
529 37 38 41 521 528 lelttrd ${⊢}{\phi }\to \left|\left(\frac{{F}\left({X}\right)}{{G}\left({X}\right)}\right)-{C}\right|<2{E}$