lhop1lem

	Ref	Expression
Hypotheses	lhop1.a	$⊢ φ \to A \in ℝ$
	lhop1.b	$⊢ φ \to B \in ℝ^{*}$
	lhop1.l	$⊢ φ \to A < B$
	lhop1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	lhop1.g	$⊢ φ \to G : (A, B) ⟶ ℝ$
	lhop1.if	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	lhop1.ig	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
	lhop1.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} A)$
	lhop1.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} A)$
	lhop1.gn0	$⊢ φ \to \neg 0 \in ran G$
	lhop1.gd0	$⊢ φ \to \neg 0 \in ran G_{ℝ}^{'}$
	lhop1.c	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} A)$
	lhop1lem.e	$⊢ φ \to E \in ℝ^{+}$
	lhop1lem.d	$⊢ φ \to D \in ℝ$
	lhop1lem.db	$⊢ φ \to D \leq B$
	lhop1lem.x	$⊢ φ \to X \in (A, D)$
	lhop1lem.t	$⊢ φ \to \forall t \in (A, D) \|(\frac{F_{ℝ}^{'} (t)}{G_{ℝ}^{'} (t)}) - C\| < E$
	lhop1lem.r	$⊢ R = A + (\frac{r}{2})$
Assertion	lhop1lem	$⊢ φ \to \|(\frac{F (X)}{G (X)}) - C\| < 2 E$

Proof

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

Metamath Proof Explorer

Theorem lhop1lem

Proof