lhop

Description: L'Hôpital's Rule. If I is an open set of the reals, F and G are real functions on A containing all of I except possibly B , which are differentiable everywhere on I \ { B } , F and G both approach 0, and the limit of F ' ( x ) / G ' ( x ) at B is C , then the limit F ( x ) / G ( x ) at B also exists and equals C . This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	lhop.a	$⊢ φ \to A \subseteq ℝ$
	lhop.f	$⊢ φ \to F : A ⟶ ℝ$
	lhop.g	$⊢ φ \to G : A ⟶ ℝ$
	lhop.i	$⊢ φ \to I \in topGen (ran (.))$
	lhop.b	$⊢ φ \to B \in I$
	lhop.d	$⊢ D = I ∖ \{B\}$
	lhop.if	$⊢ φ \to D \subseteq dom F_{ℝ}^{'}$
	lhop.ig	$⊢ φ \to D \subseteq dom G_{ℝ}^{'}$
	lhop.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} B)$
	lhop.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} B)$
	lhop.gn0	$⊢ φ \to \neg 0 \in G [D]$
	lhop.gd0	$⊢ φ \to \neg 0 \in G_{ℝ}^{'} [D]$
	lhop.c	$⊢ φ \to C \in ((z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
Assertion	lhop	$⊢ φ \to C \in ((z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		lhop.a	$⊢ φ \to A \subseteq ℝ$
2		lhop.f	$⊢ φ \to F : A ⟶ ℝ$
3		lhop.g	$⊢ φ \to G : A ⟶ ℝ$
4		lhop.i	$⊢ φ \to I \in topGen (ran (.))$
5		lhop.b	$⊢ φ \to B \in I$
6		lhop.d	$⊢ D = I ∖ \{B\}$
7		lhop.if	$⊢ φ \to D \subseteq dom F_{ℝ}^{'}$
8		lhop.ig	$⊢ φ \to D \subseteq dom G_{ℝ}^{'}$
9		lhop.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} B)$
10		lhop.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} B)$
11		lhop.gn0	$⊢ φ \to \neg 0 \in G [D]$
12		lhop.gd0	$⊢ φ \to \neg 0 \in G_{ℝ}^{'} [D]$
13		lhop.c	$⊢ φ \to C \in ((z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
14		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
15	14	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
16	15	a1i	$⊢ φ \to {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
17		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
18	14 17	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
19	18	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land I \in topGen (ran (.)) \land B \in I) \to \exists r \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq I$
20	16 4 5 19	syl3anc	$⊢ φ \to \exists r \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq I$
21		elssuni	$⊢ I \in topGen (ran (.)) \to I \subseteq ⋃ topGen (ran (.))$
22		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
23	21 22	sseqtrrdi	$⊢ I \in topGen (ran (.)) \to I \subseteq ℝ$
24	4 23	syl	$⊢ φ \to I \subseteq ℝ$
25	24 5	sseldd	$⊢ φ \to B \in ℝ$
26		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
27	14	bl2ioo	$⊢ (B \in ℝ \land r \in ℝ) \to B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (B - r, B + r)$
28	25 26 27	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (B - r, B + r)$
29	28	sseq1d	$⊢ (φ \land r \in ℝ^{+}) \to (B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq I \leftrightarrow (B - r, B + r) \subseteq I)$
30	25	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B \in ℝ$
31		simprl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to r \in ℝ^{+}$
32	31	rpred	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to r \in ℝ$
33	30 32	resubcld	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B - r \in ℝ$
34	33	rexrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B - r \in ℝ^{*}$
35	30 31	ltsubrpd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B - r < B$
36	2	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to F : A ⟶ ℝ$
37		ssun1	$⊢ (B - r, B) \subseteq (B - r, B) \cup (B, B + r)$
38		unass	$⊢ (\{B\} \cup (B - r, B)) \cup (B, B + r) = \{B\} \cup ((B - r, B) \cup (B, B + r))$
39		uncom	$⊢ \{B\} \cup (B - r, B) = (B - r, B) \cup \{B\}$
40	39	uneq1i	$⊢ (\{B\} \cup (B - r, B)) \cup (B, B + r) = ((B - r, B) \cup \{B\}) \cup (B, B + r)$
41	38 40	eqtr3i	$⊢ \{B\} \cup ((B - r, B) \cup (B, B + r)) = ((B - r, B) \cup \{B\}) \cup (B, B + r)$
42	30	rexrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B \in ℝ^{*}$
43	30 32	readdcld	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B + r \in ℝ$
44	43	rexrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B + r \in ℝ^{*}$
45	30 31	ltaddrpd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B < B + r$
46		ioojoin	$⊢ ((B - r \in ℝ^{} \land B \in ℝ^{} \land B + r \in ℝ^{*}) \land (B - r < B \land B < B + r)) \to ((B - r, B) \cup \{B\}) \cup (B, B + r) = (B - r, B + r)$
47	34 42 44 35 45 46	syl32anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ((B - r, B) \cup \{B\}) \cup (B, B + r) = (B - r, B + r)$
48	41 47	syl5eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \{B\} \cup ((B - r, B) \cup (B, B + r)) = (B - r, B + r)$
49		elioo2	$⊢ (B - r \in ℝ^{} \land B + r \in ℝ^{}) \to (B \in (B - r, B + r) \leftrightarrow (B \in ℝ \land B - r < B \land B < B + r))$
50	34 44 49	syl2anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B \in (B - r, B + r) \leftrightarrow (B \in ℝ \land B - r < B \land B < B + r))$
51	30 35 45 50	mpbir3and	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B \in (B - r, B + r)$
52	51	snssd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \{B\} \subseteq (B - r, B + r)$
53		incom	$⊢ \{B\} \cap ((B - r, B) \cup (B, B + r)) = ((B - r, B) \cup (B, B + r)) \cap \{B\}$
54		ubioo	$⊢ \neg B \in (B - r, B)$
55		lbioo	$⊢ \neg B \in (B, B + r)$
56	54 55	pm3.2ni	$⊢ \neg (B \in (B - r, B) \lor B \in (B, B + r))$
57		elun	$⊢ B \in ((B - r, B) \cup (B, B + r)) \leftrightarrow (B \in (B - r, B) \lor B \in (B, B + r))$
58	56 57	mtbir	$⊢ \neg B \in ((B - r, B) \cup (B, B + r))$
59		disjsn	$⊢ ((B - r, B) \cup (B, B + r)) \cap \{B\} = \emptyset \leftrightarrow \neg B \in ((B - r, B) \cup (B, B + r))$
60	58 59	mpbir	$⊢ ((B - r, B) \cup (B, B + r)) \cap \{B\} = \emptyset$
61	53 60	eqtri	$⊢ \{B\} \cap ((B - r, B) \cup (B, B + r)) = \emptyset$
62		uneqdifeq	$⊢ (\{B\} \subseteq (B - r, B + r) \land \{B\} \cap ((B - r, B) \cup (B, B + r)) = \emptyset) \to (\{B\} \cup ((B - r, B) \cup (B, B + r)) = (B - r, B + r) \leftrightarrow (B - r, B + r) ∖ \{B\} = (B - r, B) \cup (B, B + r))$
63	52 61 62	sylancl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (\{B\} \cup ((B - r, B) \cup (B, B + r)) = (B - r, B + r) \leftrightarrow (B - r, B + r) ∖ \{B\} = (B - r, B) \cup (B, B + r))$
64	48 63	mpbid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) ∖ \{B\} = (B - r, B) \cup (B, B + r)$
65	37 64	sseqtrrid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq (B - r, B + r) ∖ \{B\}$
66		ssdif	$⊢ (B - r, B + r) \subseteq I \to (B - r, B + r) ∖ \{B\} \subseteq I ∖ \{B\}$
67	66	ad2antll	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) ∖ \{B\} \subseteq I ∖ \{B\}$
68	67 6	sseqtrrdi	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) ∖ \{B\} \subseteq D$
69		ax-resscn	$⊢ ℝ \subseteq ℂ$
70	69	a1i	$⊢ φ \to ℝ \subseteq ℂ$
71		fss	$⊢ (F : A ⟶ ℝ \land ℝ \subseteq ℂ) \to F : A ⟶ ℂ$
72	2 69 71	sylancl	$⊢ φ \to F : A ⟶ ℂ$
73	70 72 1	dvbss	$⊢ φ \to dom F_{ℝ}^{'} \subseteq A$
74	7 73	sstrd	$⊢ φ \to D \subseteq A$
75	74	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to D \subseteq A$
76	68 75	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) ∖ \{B\} \subseteq A$
77	65 76	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq A$
78	36 77	fssresd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({F ↾}_{(B - r, B)}) : (B - r, B) ⟶ ℝ$
79	3	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to G : A ⟶ ℝ$
80	79 77	fssresd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({G ↾}_{(B - r, B)}) : (B - r, B) ⟶ ℝ$
81	69	a1i	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ \subseteq ℂ$
82	72	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to F : A ⟶ ℂ$
83	1	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to A \subseteq ℝ$
84		ioossre	$⊢ (B - r, B) \subseteq ℝ$
85	84	a1i	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq ℝ$
86		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
87	86	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
88	86 87	dvres	$⊢ ((ℝ \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq ℝ \land (B - r, B) \subseteq ℝ)) \to ℝ D ({F ↾}_{(B - r, B)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B - r, B))}$
89	81 82 83 85 88	syl22anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({F ↾}_{(B - r, B)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B - r, B))}$
90		retop	$⊢ topGen (ran (.)) \in Top$
91		iooretop	$⊢ (B - r, B) \in topGen (ran (.))$
92		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (B - r, B) \in topGen (ran (.))) \to int (topGen (ran (.))) ((B - r, B)) = (B - r, B)$
93	90 91 92	mp2an	$⊢ int (topGen (ran (.))) ((B - r, B)) = (B - r, B)$
94	93	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B - r, B))} = {F_{ℝ}^{'} ↾}_{(B - r, B)}$
95	89 94	syl6eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({F ↾}_{(B - r, B)}) = {F_{ℝ}^{'} ↾}_{(B - r, B)}$
96	95	dmeqd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({F ↾}_{(B - r, B)})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{(B - r, B)})$
97	65 68	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq D$
98	7	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to D \subseteq dom F_{ℝ}^{'}$
99	97 98	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq dom F_{ℝ}^{'}$
100		ssdmres	$⊢ (B - r, B) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(B - r, B)}) = (B - r, B)$
101	99 100	sylib	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom ({F_{ℝ}^{'} ↾}_{(B - r, B)}) = (B - r, B)$
102	96 101	eqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({F ↾}_{(B - r, B)})}_{ℝ}^{'} = (B - r, B)$
103		fss	$⊢ (G : A ⟶ ℝ \land ℝ \subseteq ℂ) \to G : A ⟶ ℂ$
104	3 69 103	sylancl	$⊢ φ \to G : A ⟶ ℂ$
105	104	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to G : A ⟶ ℂ$
106	86 87	dvres	$⊢ ((ℝ \subseteq ℂ \land G : A ⟶ ℂ) \land (A \subseteq ℝ \land (B - r, B) \subseteq ℝ)) \to ℝ D ({G ↾}_{(B - r, B)}) = {G_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B - r, B))}$
107	81 105 83 85 106	syl22anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({G ↾}_{(B - r, B)}) = {G_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B - r, B))}$
108	93	reseq2i	$⊢ {G_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B - r, B))} = {G_{ℝ}^{'} ↾}_{(B - r, B)}$
109	107 108	syl6eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({G ↾}_{(B - r, B)}) = {G_{ℝ}^{'} ↾}_{(B - r, B)}$
110	109	dmeqd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({G ↾}_{(B - r, B)})}_{ℝ}^{'} = dom ({G_{ℝ}^{'} ↾}_{(B - r, B)})$
111	8	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to D \subseteq dom G_{ℝ}^{'}$
112	97 111	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq dom G_{ℝ}^{'}$
113		ssdmres	$⊢ (B - r, B) \subseteq dom G_{ℝ}^{'} \leftrightarrow dom ({G_{ℝ}^{'} ↾}_{(B - r, B)}) = (B - r, B)$
114	112 113	sylib	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom ({G_{ℝ}^{'} ↾}_{(B - r, B)}) = (B - r, B)$
115	110 114	eqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({G ↾}_{(B - r, B)})}_{ℝ}^{'} = (B - r, B)$
116		limcresi	$⊢ F {lim}_{ℂ} B \subseteq ({F ↾}_{(B - r, B)}) {lim}_{ℂ} B$
117	9	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to 0 \in (F {lim}_{ℂ} B)$
118	116 117	sseldi	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to 0 \in (({F ↾}_{(B - r, B)}) {lim}_{ℂ} B)$
119		limcresi	$⊢ G {lim}_{ℂ} B \subseteq ({G ↾}_{(B - r, B)}) {lim}_{ℂ} B$
120	10	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to 0 \in (G {lim}_{ℂ} B)$
121	119 120	sseldi	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to 0 \in (({G ↾}_{(B - r, B)}) {lim}_{ℂ} B)$
122		df-ima	$⊢ G [(B - r, B)] = ran ({G ↾}_{(B - r, B)})$
123		imass2	$⊢ (B - r, B) \subseteq D \to G [(B - r, B)] \subseteq G [D]$
124	97 123	syl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to G [(B - r, B)] \subseteq G [D]$
125	122 124	eqsstrrid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran ({G ↾}_{(B - r, B)}) \subseteq G [D]$
126	11	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \neg 0 \in G [D]$
127	125 126	ssneldd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \neg 0 \in ran ({G ↾}_{(B - r, B)})$
128	109	rneqd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran {({G ↾}_{(B - r, B)})}_{ℝ}^{'} = ran ({G_{ℝ}^{'} ↾}_{(B - r, B)})$
129		df-ima	$⊢ G_{ℝ}^{'} [(B - r, B)] = ran ({G_{ℝ}^{'} ↾}_{(B - r, B)})$
130	128 129	syl6eqr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran {({G ↾}_{(B - r, B)})}_{ℝ}^{'} = G_{ℝ}^{'} [(B - r, B)]$
131		imass2	$⊢ (B - r, B) \subseteq D \to G_{ℝ}^{'} [(B - r, B)] \subseteq G_{ℝ}^{'} [D]$
132	97 131	syl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to G_{ℝ}^{'} [(B - r, B)] \subseteq G_{ℝ}^{'} [D]$
133	130 132	eqsstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran {({G ↾}_{(B - r, B)})}_{ℝ}^{'} \subseteq G_{ℝ}^{'} [D]$
134	12	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \neg 0 \in G_{ℝ}^{'} [D]$
135	133 134	ssneldd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \neg 0 \in ran {({G ↾}_{(B - r, B)})}_{ℝ}^{'}$
136		limcresi	$⊢ (z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B \subseteq ({(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B$
137	97	resmptd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B - r, B)} = (z \in (B - r, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)})$
138	95	fveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z) = ({F_{ℝ}^{'} ↾}_{(B - r, B)}) (z)$
139		fvres	$⊢ z \in (B - r, B) \to ({F_{ℝ}^{'} ↾}_{(B - r, B)}) (z) = F_{ℝ}^{'} (z)$
140	138 139	sylan9eq	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in (B - r, B)) \to {({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z) = F_{ℝ}^{'} (z)$
141	109	fveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z) = ({G_{ℝ}^{'} ↾}_{(B - r, B)}) (z)$
142		fvres	$⊢ z \in (B - r, B) \to ({G_{ℝ}^{'} ↾}_{(B - r, B)}) (z) = G_{ℝ}^{'} (z)$
143	141 142	sylan9eq	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in (B - r, B)) \to {({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z) = G_{ℝ}^{'} (z)$
144	140 143	oveq12d	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in (B - r, B)) \to \frac{{({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z)} = \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}$
145	144	mpteq2dva	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in (B - r, B) ⟼ \frac{{({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}) = (z \in (B - r, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)})$
146	137 145	eqtr4d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B - r, B)} = (z \in (B - r, B) ⟼ \frac{{({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z)})$
147	146	oveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B = (z \in (B - r, B) ⟼ \frac{{({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}) {lim}_{ℂ} B$
148	136 147	sseqtrid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B \subseteq (z \in (B - r, B) ⟼ \frac{{({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}) {lim}_{ℂ} B$
149	13	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
150	148 149	sseldd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((z \in (B - r, B) ⟼ \frac{{({F ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B - r, B)})}_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
151	34 30 35 78 80 102 115 118 121 127 135 150	lhop2	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((z \in (B - r, B) ⟼ \frac{({F ↾}_{(B - r, B)}) (z)}{({G ↾}_{(B - r, B)}) (z)}) {lim}_{ℂ} B)$
152	65	resmptd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)} = (z \in (B - r, B) ⟼ \frac{F (z)}{G (z)})$
153		fvres	$⊢ z \in (B - r, B) \to ({F ↾}_{(B - r, B)}) (z) = F (z)$
154		fvres	$⊢ z \in (B - r, B) \to ({G ↾}_{(B - r, B)}) (z) = G (z)$
155	153 154	oveq12d	$⊢ z \in (B - r, B) \to \frac{({F ↾}_{(B - r, B)}) (z)}{({G ↾}_{(B - r, B)}) (z)} = \frac{F (z)}{G (z)}$
156	155	mpteq2ia	$⊢ (z \in (B - r, B) ⟼ \frac{({F ↾}_{(B - r, B)}) (z)}{({G ↾}_{(B - r, B)}) (z)}) = (z \in (B - r, B) ⟼ \frac{F (z)}{G (z)})$
157	152 156	syl6eqr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)} = (z \in (B - r, B) ⟼ \frac{({F ↾}_{(B - r, B)}) (z)}{({G ↾}_{(B - r, B)}) (z)})$
158	157	oveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B = (z \in (B - r, B) ⟼ \frac{({F ↾}_{(B - r, B)}) (z)}{({G ↾}_{(B - r, B)}) (z)}) {lim}_{ℂ} B$
159	151 158	eleqtrrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B)$
160		ssun2	$⊢ (B, B + r) \subseteq (B - r, B) \cup (B, B + r)$
161	160 64	sseqtrrid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq (B - r, B + r) ∖ \{B\}$
162	161 76	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq A$
163	36 162	fssresd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({F ↾}_{(B, B + r)}) : (B, B + r) ⟶ ℝ$
164	79 162	fssresd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({G ↾}_{(B, B + r)}) : (B, B + r) ⟶ ℝ$
165		ioossre	$⊢ (B, B + r) \subseteq ℝ$
166	165	a1i	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq ℝ$
167	86 87	dvres	$⊢ ((ℝ \subseteq ℂ \land F : A ⟶ ℂ) \land (A \subseteq ℝ \land (B, B + r) \subseteq ℝ)) \to ℝ D ({F ↾}_{(B, B + r)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, B + r))}$
168	81 82 83 166 167	syl22anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({F ↾}_{(B, B + r)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, B + r))}$
169		iooretop	$⊢ (B, B + r) \in topGen (ran (.))$
170		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (B, B + r) \in topGen (ran (.))) \to int (topGen (ran (.))) ((B, B + r)) = (B, B + r)$
171	90 169 170	mp2an	$⊢ int (topGen (ran (.))) ((B, B + r)) = (B, B + r)$
172	171	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, B + r))} = {F_{ℝ}^{'} ↾}_{(B, B + r)}$
173	168 172	syl6eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({F ↾}_{(B, B + r)}) = {F_{ℝ}^{'} ↾}_{(B, B + r)}$
174	173	dmeqd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({F ↾}_{(B, B + r)})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{(B, B + r)})$
175	161 68	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq D$
176	175 98	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq dom F_{ℝ}^{'}$
177		ssdmres	$⊢ (B, B + r) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(B, B + r)}) = (B, B + r)$
178	176 177	sylib	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom ({F_{ℝ}^{'} ↾}_{(B, B + r)}) = (B, B + r)$
179	174 178	eqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({F ↾}_{(B, B + r)})}_{ℝ}^{'} = (B, B + r)$
180	86 87	dvres	$⊢ ((ℝ \subseteq ℂ \land G : A ⟶ ℂ) \land (A \subseteq ℝ \land (B, B + r) \subseteq ℝ)) \to ℝ D ({G ↾}_{(B, B + r)}) = {G_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, B + r))}$
181	81 105 83 166 180	syl22anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({G ↾}_{(B, B + r)}) = {G_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, B + r))}$
182	171	reseq2i	$⊢ {G_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((B, B + r))} = {G_{ℝ}^{'} ↾}_{(B, B + r)}$
183	181 182	syl6eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ℝ D ({G ↾}_{(B, B + r)}) = {G_{ℝ}^{'} ↾}_{(B, B + r)}$
184	183	dmeqd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({G ↾}_{(B, B + r)})}_{ℝ}^{'} = dom ({G_{ℝ}^{'} ↾}_{(B, B + r)})$
185	175 111	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq dom G_{ℝ}^{'}$
186		ssdmres	$⊢ (B, B + r) \subseteq dom G_{ℝ}^{'} \leftrightarrow dom ({G_{ℝ}^{'} ↾}_{(B, B + r)}) = (B, B + r)$
187	185 186	sylib	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom ({G_{ℝ}^{'} ↾}_{(B, B + r)}) = (B, B + r)$
188	184 187	eqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to dom {({G ↾}_{(B, B + r)})}_{ℝ}^{'} = (B, B + r)$
189		limcresi	$⊢ F {lim}_{ℂ} B \subseteq ({F ↾}_{(B, B + r)}) {lim}_{ℂ} B$
190	189 117	sseldi	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to 0 \in (({F ↾}_{(B, B + r)}) {lim}_{ℂ} B)$
191		limcresi	$⊢ G {lim}_{ℂ} B \subseteq ({G ↾}_{(B, B + r)}) {lim}_{ℂ} B$
192	191 120	sseldi	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to 0 \in (({G ↾}_{(B, B + r)}) {lim}_{ℂ} B)$
193		df-ima	$⊢ G [(B, B + r)] = ran ({G ↾}_{(B, B + r)})$
194		imass2	$⊢ (B, B + r) \subseteq D \to G [(B, B + r)] \subseteq G [D]$
195	175 194	syl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to G [(B, B + r)] \subseteq G [D]$
196	193 195	eqsstrrid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran ({G ↾}_{(B, B + r)}) \subseteq G [D]$
197	196 126	ssneldd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \neg 0 \in ran ({G ↾}_{(B, B + r)})$
198	183	rneqd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran {({G ↾}_{(B, B + r)})}_{ℝ}^{'} = ran ({G_{ℝ}^{'} ↾}_{(B, B + r)})$
199		df-ima	$⊢ G_{ℝ}^{'} [(B, B + r)] = ran ({G_{ℝ}^{'} ↾}_{(B, B + r)})$
200	198 199	syl6eqr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran {({G ↾}_{(B, B + r)})}_{ℝ}^{'} = G_{ℝ}^{'} [(B, B + r)]$
201		imass2	$⊢ (B, B + r) \subseteq D \to G_{ℝ}^{'} [(B, B + r)] \subseteq G_{ℝ}^{'} [D]$
202	175 201	syl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to G_{ℝ}^{'} [(B, B + r)] \subseteq G_{ℝ}^{'} [D]$
203	200 202	eqsstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ran {({G ↾}_{(B, B + r)})}_{ℝ}^{'} \subseteq G_{ℝ}^{'} [D]$
204	203 134	ssneldd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \neg 0 \in ran {({G ↾}_{(B, B + r)})}_{ℝ}^{'}$
205		limcresi	$⊢ (z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B \subseteq ({(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B$
206	175	resmptd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B, B + r)} = (z \in (B, B + r) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)})$
207	173	fveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z) = ({F_{ℝ}^{'} ↾}_{(B, B + r)}) (z)$
208		fvres	$⊢ z \in (B, B + r) \to ({F_{ℝ}^{'} ↾}_{(B, B + r)}) (z) = F_{ℝ}^{'} (z)$
209	207 208	sylan9eq	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in (B, B + r)) \to {({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z) = F_{ℝ}^{'} (z)$
210	183	fveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z) = ({G_{ℝ}^{'} ↾}_{(B, B + r)}) (z)$
211		fvres	$⊢ z \in (B, B + r) \to ({G_{ℝ}^{'} ↾}_{(B, B + r)}) (z) = G_{ℝ}^{'} (z)$
212	210 211	sylan9eq	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in (B, B + r)) \to {({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z) = G_{ℝ}^{'} (z)$
213	209 212	oveq12d	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in (B, B + r)) \to \frac{{({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z)} = \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}$
214	213	mpteq2dva	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in (B, B + r) ⟼ \frac{{({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}) = (z \in (B, B + r) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)})$
215	206 214	eqtr4d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B, B + r)} = (z \in (B, B + r) ⟼ \frac{{({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z)})$
216	215	oveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({(z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B = (z \in (B, B + r) ⟼ \frac{{({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}) {lim}_{ℂ} B$
217	205 216	sseqtrid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in D ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B \subseteq (z \in (B, B + r) ⟼ \frac{{({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}) {lim}_{ℂ} B$
218	217 149	sseldd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((z \in (B, B + r) ⟼ \frac{{({F ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}{{({G ↾}_{(B, B + r)})}_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
219	30 44 45 163 164 179 188 190 192 197 204 218	lhop1	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((z \in (B, B + r) ⟼ \frac{({F ↾}_{(B, B + r)}) (z)}{({G ↾}_{(B, B + r)}) (z)}) {lim}_{ℂ} B)$
220	161	resmptd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)} = (z \in (B, B + r) ⟼ \frac{F (z)}{G (z)})$
221		fvres	$⊢ z \in (B, B + r) \to ({F ↾}_{(B, B + r)}) (z) = F (z)$
222		fvres	$⊢ z \in (B, B + r) \to ({G ↾}_{(B, B + r)}) (z) = G (z)$
223	221 222	oveq12d	$⊢ z \in (B, B + r) \to \frac{({F ↾}_{(B, B + r)}) (z)}{({G ↾}_{(B, B + r)}) (z)} = \frac{F (z)}{G (z)}$
224	223	mpteq2ia	$⊢ (z \in (B, B + r) ⟼ \frac{({F ↾}_{(B, B + r)}) (z)}{({G ↾}_{(B, B + r)}) (z)}) = (z \in (B, B + r) ⟼ \frac{F (z)}{G (z)})$
225	220 224	syl6eqr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)} = (z \in (B, B + r) ⟼ \frac{({F ↾}_{(B, B + r)}) (z)}{({G ↾}_{(B, B + r)}) (z)})$
226	225	oveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B = (z \in (B, B + r) ⟼ \frac{({F ↾}_{(B, B + r)}) (z)}{({G ↾}_{(B, B + r)}) (z)}) {lim}_{ℂ} B$
227	219 226	eleqtrrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B)$
228	159 227	elind	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B) \cap (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B))$
229	68	resmptd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to {(z \in D ⟼ \frac{F (z)}{G (z)}) ↾}_{((B - r, B + r) ∖ \{B\})} = (z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)})$
230	229	oveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({(z \in D ⟼ \frac{F (z)}{G (z)}) ↾}_{((B - r, B + r) ∖ \{B\})}) {lim}_{ℂ} B = (z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
231	74	sselda	$⊢ (φ \land z \in D) \to z \in A$
232	2	ffvelrnda	$⊢ (φ \land z \in A) \to F (z) \in ℝ$
233	231 232	syldan	$⊢ (φ \land z \in D) \to F (z) \in ℝ$
234	233	recnd	$⊢ (φ \land z \in D) \to F (z) \in ℂ$
235	3	ffvelrnda	$⊢ (φ \land z \in A) \to G (z) \in ℝ$
236	231 235	syldan	$⊢ (φ \land z \in D) \to G (z) \in ℝ$
237	236	recnd	$⊢ (φ \land z \in D) \to G (z) \in ℂ$
238	11	adantr	$⊢ (φ \land z \in D) \to \neg 0 \in G [D]$
239	3	ffnd	$⊢ φ \to G Fn A$
240	239	adantr	$⊢ (φ \land z \in D) \to G Fn A$
241	74	adantr	$⊢ (φ \land z \in D) \to D \subseteq A$
242		simpr	$⊢ (φ \land z \in D) \to z \in D$
243		fnfvima	$⊢ (G Fn A \land D \subseteq A \land z \in D) \to G (z) \in G [D]$
244	240 241 242 243	syl3anc	$⊢ (φ \land z \in D) \to G (z) \in G [D]$
245		eleq1	$⊢ G (z) = 0 \to (G (z) \in G [D] \leftrightarrow 0 \in G [D])$
246	244 245	syl5ibcom	$⊢ (φ \land z \in D) \to (G (z) = 0 \to 0 \in G [D])$
247	246	necon3bd	$⊢ (φ \land z \in D) \to (\neg 0 \in G [D] \to G (z) \neq 0)$
248	238 247	mpd	$⊢ (φ \land z \in D) \to G (z) \neq 0$
249	234 237 248	divcld	$⊢ (φ \land z \in D) \to \frac{F (z)}{G (z)} \in ℂ$
250	249	adantlr	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in D) \to \frac{F (z)}{G (z)} \in ℂ$
251	250	fmpttd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in D ⟼ \frac{F (z)}{G (z)}) : D ⟶ ℂ$
252		difss	$⊢ I ∖ \{B\} \subseteq I$
253	6 252	eqsstri	$⊢ D \subseteq I$
254	24 69	sstrdi	$⊢ φ \to I \subseteq ℂ$
255	253 254	sstrid	$⊢ φ \to D \subseteq ℂ$
256	255	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to D \subseteq ℂ$
257		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})$
258	6	uneq1i	$⊢ D \cup \{B\} = (I ∖ \{B\}) \cup \{B\}$
259		undif1	$⊢ (I ∖ \{B\}) \cup \{B\} = I \cup \{B\}$
260	258 259	eqtri	$⊢ D \cup \{B\} = I \cup \{B\}$
261		simprr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) \subseteq I$
262	52 261	sstrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to \{B\} \subseteq I$
263		ssequn2	$⊢ \{B\} \subseteq I \leftrightarrow I \cup \{B\} = I$
264	262 263	sylib	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to I \cup \{B\} = I$
265	260 264	syl5eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to D \cup \{B\} = I$
266	265	oveq2d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} I$
267	24	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to I \subseteq ℝ$
268		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
269	86 268	rerest	$⊢ I \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} I = topGen (ran (.)) ↾_{𝑡} I$
270	267 269	syl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} I = topGen (ran (.)) ↾_{𝑡} I$
271	266 270	eqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\}) = topGen (ran (.)) ↾_{𝑡} I$
272	271	fveq2d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) = int (topGen (ran (.)) ↾_{𝑡} I)$
273	272	fveq1d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) ((B - r, B + r)) = int (topGen (ran (.)) ↾_{𝑡} I) ((B - r, B + r))$
274	86	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
275	254	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to I \subseteq ℂ$
276		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land I \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} I \in TopOn (I)$
277	274 275 276	sylancr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} I \in TopOn (I)$
278		topontop	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} I \in TopOn (I) \to TopOpen (ℂ_{fld}) ↾_{𝑡} I \in Top$
279	277 278	syl	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} I \in Top$
280	270 279	eqeltrrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to topGen (ran (.)) ↾_{𝑡} I \in Top$
281		iooretop	$⊢ (B - r, B + r) \in topGen (ran (.))$
282	281	a1i	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) \in topGen (ran (.))$
283	4	adantr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to I \in topGen (ran (.))$
284		restopn2	$⊢ (topGen (ran (.)) \in Top \land I \in topGen (ran (.))) \to ((B - r, B + r) \in (topGen (ran (.)) ↾_{𝑡} I) \leftrightarrow ((B - r, B + r) \in topGen (ran (.)) \land (B - r, B + r) \subseteq I))$
285	90 283 284	sylancr	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ((B - r, B + r) \in (topGen (ran (.)) ↾_{𝑡} I) \leftrightarrow ((B - r, B + r) \in topGen (ran (.)) \land (B - r, B + r) \subseteq I))$
286	282 261 285	mpbir2and	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) \in (topGen (ran (.)) ↾_{𝑡} I)$
287		isopn3i	$⊢ (topGen (ran (.)) ↾_{𝑡} I \in Top \land (B - r, B + r) \in (topGen (ran (.)) ↾_{𝑡} I)) \to int (topGen (ran (.)) ↾_{𝑡} I) ((B - r, B + r)) = (B - r, B + r)$
288	280 286 287	syl2anc	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to int (topGen (ran (.)) ↾_{𝑡} I) ((B - r, B + r)) = (B - r, B + r)$
289	273 288	eqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) ((B - r, B + r)) = (B - r, B + r)$
290	51 289	eleqtrrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) ((B - r, B + r))$
291		undif1	$⊢ ((B - r, B + r) ∖ \{B\}) \cup \{B\} = (B - r, B + r) \cup \{B\}$
292		ssequn2	$⊢ \{B\} \subseteq (B - r, B + r) \leftrightarrow (B - r, B + r) \cup \{B\} = (B - r, B + r)$
293	52 292	sylib	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B + r) \cup \{B\} = (B - r, B + r)$
294	291 293	syl5eq	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ((B - r, B + r) ∖ \{B\}) \cup \{B\} = (B - r, B + r)$
295	294	fveq2d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) (((B - r, B + r) ∖ \{B\}) \cup \{B\}) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) ((B - r, B + r))$
296	290 295	eleqtrrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} (D \cup \{B\})) (((B - r, B + r) ∖ \{B\}) \cup \{B\})$
297	251 68 256 86 257 296	limcres	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ({(z \in D ⟼ \frac{F (z)}{G (z)}) ↾}_{((B - r, B + r) ∖ \{B\})}) {lim}_{ℂ} B = (z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
298	84 69	sstri	$⊢ (B - r, B) \subseteq ℂ$
299	298	a1i	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B - r, B) \subseteq ℂ$
300	165 69	sstri	$⊢ (B, B + r) \subseteq ℂ$
301	300	a1i	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (B, B + r) \subseteq ℂ$
302	68	sselda	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in ((B - r, B + r) ∖ \{B\})) \to z \in D$
303	302 250	syldan	$⊢ ((φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \land z \in ((B - r, B + r) ∖ \{B\})) \to \frac{F (z)}{G (z)} \in ℂ$
304	303	fmpttd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) : (B - r, B + r) ∖ \{B\} ⟶ ℂ$
305	64	feq2d	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to ((z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) : (B - r, B + r) ∖ \{B\} ⟶ ℂ \leftrightarrow (z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) : (B - r, B) \cup (B, B + r) ⟶ ℂ)$
306	304 305	mpbid	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) : (B - r, B) \cup (B, B + r) ⟶ ℂ$
307	299 301 306	limcun	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B = (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B) \cap (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B)$
308	230 297 307	3eqtr3rd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B - r, B)}) {lim}_{ℂ} B) \cap (({(z \in ((B - r, B + r) ∖ \{B\}) ⟼ \frac{F (z)}{G (z)}) ↾}_{(B, B + r)}) {lim}_{ℂ} B) = (z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
309	228 308	eleqtrd	$⊢ (φ \land (r \in ℝ^{+} \land (B - r, B + r) \subseteq I)) \to C \in ((z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B)$
310	309	expr	$⊢ (φ \land r \in ℝ^{+}) \to ((B - r, B + r) \subseteq I \to C \in ((z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B))$
311	29 310	sylbid	$⊢ (φ \land r \in ℝ^{+}) \to (B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq I \to C \in ((z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B))$
312	311	rexlimdva	$⊢ φ \to (\exists r \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq I \to C \in ((z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B))$
313	20 312	mpd	$⊢ φ \to C \in ((z \in D ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem lhop

Proof