lhop2

Description: L'Hôpital's Rule for limits from the left. If F and G are differentiable real functions on ( A , B ) , and F and G both approach 0 at B , and G ( x ) and G ' ( x ) are not zero on ( A , B ) , 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 . (Contributed by Mario Carneiro, 29-Dec-2016)

	Ref	Expression
Hypotheses	lhop2.a	$⊢ φ \to A \in ℝ^{*}$
	lhop2.b	$⊢ φ \to B \in ℝ$
	lhop2.l	$⊢ φ \to A < B$
	lhop2.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	lhop2.g	$⊢ φ \to G : (A, B) ⟶ ℝ$
	lhop2.if	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	lhop2.ig	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
	lhop2.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} B)$
	lhop2.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} B)$
	lhop2.gn0	$⊢ φ \to \neg 0 \in ran G$
	lhop2.gd0	$⊢ φ \to \neg 0 \in ran G_{ℝ}^{'}$
	lhop2.c	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
Assertion	lhop2	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		lhop2.a	$⊢ φ \to A \in ℝ^{*}$
2		lhop2.b	$⊢ φ \to B \in ℝ$
3		lhop2.l	$⊢ φ \to A < B$
4		lhop2.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
5		lhop2.g	$⊢ φ \to G : (A, B) ⟶ ℝ$
6		lhop2.if	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
7		lhop2.ig	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
8		lhop2.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} B)$
9		lhop2.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} B)$
10		lhop2.gn0	$⊢ φ \to \neg 0 \in ran G$
11		lhop2.gd0	$⊢ φ \to \neg 0 \in ran G_{ℝ}^{'}$
12		lhop2.c	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
13		qssre	$⊢ ℚ \subseteq ℝ$
14	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
15		qbtwnxr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists a \in ℚ (A < a \land a < B)$
16	1 14 3 15	syl3anc	$⊢ φ \to \exists a \in ℚ (A < a \land a < B)$
17		ssrexv	$⊢ ℚ \subseteq ℝ \to (\exists a \in ℚ (A < a \land a < B) \to \exists a \in ℝ (A < a \land a < B))$
18	13 16 17	mpsyl	$⊢ φ \to \exists a \in ℝ (A < a \land a < B)$
19		simpr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to z \in (a, B)$
20		simprl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to a \in ℝ$
21	20	adantr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to a \in ℝ$
22	2	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to B \in ℝ$
23		elioore	$⊢ z \in (a, B) \to z \in ℝ$
24	23	adantl	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to z \in ℝ$
25		iooneg	$⊢ (a \in ℝ \land B \in ℝ \land z \in ℝ) \to (z \in (a, B) \leftrightarrow - z \in (- B, - a))$
26	21 22 24 25	syl3anc	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to (z \in (a, B) \leftrightarrow - z \in (- B, - a))$
27	19 26	mpbid	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to - z \in (- B, - a)$
28	27	adantrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land (z \in (a, B) \land - z \neq - B)) \to - z \in (- B, - a)$
29	4	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F : (A, B) ⟶ ℝ$
30		elioore	$⊢ x \in (- B, - a) \to x \in ℝ$
31	30	adantl	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to x \in ℝ$
32	31	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to x \in ℂ$
33	32	negnegd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - (- x) = x$
34		simpr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to x \in (- B, - a)$
35	33 34	eqeltrd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - (- x) \in (- B, - a)$
36	20	adantr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to a \in ℝ$
37	2	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to B \in ℝ$
38	31	renegcld	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - x \in ℝ$
39		iooneg	$⊢ (a \in ℝ \land B \in ℝ \land - x \in ℝ) \to (- x \in (a, B) \leftrightarrow - (- x) \in (- B, - a))$
40	36 37 38 39	syl3anc	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (- x \in (a, B) \leftrightarrow - (- x) \in (- B, - a))$
41	35 40	mpbird	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - x \in (a, B)$
42	1	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to A \in ℝ^{*}$
43	20	rexrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to a \in ℝ^{*}$
44		simprrl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to A < a$
45	42 43 44	xrltled	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to A \leq a$
46		iooss1	$⊢ (A \in ℝ^{*} \land A \leq a) \to (a, B) \subseteq (A, B)$
47	42 45 46	syl2anc	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, B) \subseteq (A, B)$
48	47	sselda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land - x \in (a, B)) \to - x \in (A, B)$
49	41 48	syldan	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - x \in (A, B)$
50	29 49	ffvelrnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F (- x) \in ℝ$
51	50	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F (- x) \in ℂ$
52	5	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G : (A, B) ⟶ ℝ$
53	52 49	ffvelrnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G (- x) \in ℝ$
54	53	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G (- x) \in ℂ$
55	10	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \neg 0 \in ran G$
56	5	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G : (A, B) ⟶ ℝ$
57		ax-resscn	$⊢ ℝ \subseteq ℂ$
58		fss	$⊢ (G : (A, B) ⟶ ℝ \land ℝ \subseteq ℂ) \to G : (A, B) ⟶ ℂ$
59	56 57 58	sylancl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G : (A, B) ⟶ ℂ$
60	59	adantr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G : (A, B) ⟶ ℂ$
61	60	ffnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G Fn (A, B)$
62		fnfvelrn	$⊢ (G Fn (A, B) \land - x \in (A, B)) \to G (- x) \in ran G$
63	61 49 62	syl2anc	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G (- x) \in ran G$
64		eleq1	$⊢ G (- x) = 0 \to (G (- x) \in ran G \leftrightarrow 0 \in ran G)$
65	63 64	syl5ibcom	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (G (- x) = 0 \to 0 \in ran G)$
66	65	necon3bd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (\neg 0 \in ran G \to G (- x) \neq 0)$
67	55 66	mpd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G (- x) \neq 0$
68	51 54 67	divcld	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{F (- x)}{G (- x)} \in ℂ$
69		limcresi	$⊢ (z \in ℝ ⟼ - z) {lim}_{ℂ} B \subseteq ({(z \in ℝ ⟼ - z) ↾}_{(a, B)}) {lim}_{ℂ} B$
70		ioossre	$⊢ (a, B) \subseteq ℝ$
71		resmpt	$⊢ (a, B) \subseteq ℝ \to {(z \in ℝ ⟼ - z) ↾}_{(a, B)} = (z \in (a, B) ⟼ - z)$
72	70 71	ax-mp	$⊢ {(z \in ℝ ⟼ - z) ↾}_{(a, B)} = (z \in (a, B) ⟼ - z)$
73	72	oveq1i	$⊢ ({(z \in ℝ ⟼ - z) ↾}_{(a, B)}) {lim}_{ℂ} B = (z \in (a, B) ⟼ - z) {lim}_{ℂ} B$
74	69 73	sseqtri	$⊢ (z \in ℝ ⟼ - z) {lim}_{ℂ} B \subseteq (z \in (a, B) ⟼ - z) {lim}_{ℂ} B$
75		eqid	$⊢ (z \in ℝ ⟼ - z) = (z \in ℝ ⟼ - z)$
76	75	negcncf	$⊢ ℝ \subseteq ℂ \to (z \in ℝ ⟼ - z) : ℝ \underset{cn}{⟶} ℂ$
77	57 76	mp1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (z \in ℝ ⟼ - z) : ℝ \underset{cn}{⟶} ℂ$
78	2	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in ℝ$
79		negeq	$⊢ z = B \to - z = - B$
80	77 78 79	cnmptlimc	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - B \in ((z \in ℝ ⟼ - z) {lim}_{ℂ} B)$
81	74 80	sselid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - B \in ((z \in (a, B) ⟼ - z) {lim}_{ℂ} B)$
82	78	renegcld	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - B \in ℝ$
83	20	renegcld	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - a \in ℝ$
84	83	rexrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - a \in ℝ^{*}$
85		simprrr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to a < B$
86	20 78	ltnegd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a < B \leftrightarrow - B < - a)$
87	85 86	mpbid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - B < - a$
88	50	fmpttd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ F (- x)) : (- B, - a) ⟶ ℝ$
89	53	fmpttd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ G (- x)) : (- B, - a) ⟶ ℝ$
90		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
91	90	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ℝ \in \{ℝ, ℂ\}$
92		neg1cn	$⊢ - 1 \in ℂ$
93	92	a1i	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - 1 \in ℂ$
94	4	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to F : (A, B) ⟶ ℝ$
95	94	ffvelrnda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land y \in (A, B)) \to F (y) \in ℝ$
96	95	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land y \in (A, B)) \to F (y) \in ℂ$
97		fvexd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land y \in (A, B)) \to F_{ℝ}^{'} (y) \in V$
98		1cnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to 1 \in ℂ$
99		simpr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in ℝ) \to x \in ℝ$
100	99	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in ℝ) \to x \in ℂ$
101		1cnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in ℝ) \to 1 \in ℂ$
102	91	dvmptid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
103		ioossre	$⊢ (- B, - a) \subseteq ℝ$
104	103	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (- B, - a) \subseteq ℝ$
105		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
106	105	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
107		iooretop	$⊢ (- B, - a) \in topGen (ran (.))$
108	107	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (- B, - a) \in topGen (ran (.))$
109	91 100 101 102 104 106 105 108	dvmptres	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ x)}{d_{ℝ} x} = (x \in (- B, - a) ⟼ 1)$
110	91 32 98 109	dvmptneg	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ - x)}{d_{ℝ} x} = (x \in (- B, - a) ⟼ - 1)$
111	94	feqmptd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to F = (y \in (A, B) ⟼ F (y))$
112	111	oveq2d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ℝ D F = \frac{d (y \in (A, B)⟼ F (y))}{d_{ℝ} y}$
113		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
114	6	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to dom F_{ℝ}^{'} = (A, B)$
115	114	feq2d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
116	113 115	mpbii	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
117	116	feqmptd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ℝ D F = (y \in (A, B) ⟼ F_{ℝ}^{'} (y))$
118	112 117	eqtr3d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (y \in (A, B)⟼ F (y))}{d_{ℝ} y} = (y \in (A, B) ⟼ F_{ℝ}^{'} (y))$
119		fveq2	$⊢ y = - x \to F (y) = F (- x)$
120		fveq2	$⊢ y = - x \to F_{ℝ}^{'} (y) = F_{ℝ}^{'} (- x)$
121	91 91 49 93 96 97 110 118 119 120	dvmptco	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} = (x \in (- B, - a) ⟼ F_{ℝ}^{'} (- x) -1)$
122	116	adantr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
123	122 49	ffvelrnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F_{ℝ}^{'} (- x) \in ℂ$
124	123 93	mulcomd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F_{ℝ}^{'} (- x) -1 = -1 F_{ℝ}^{'} (- x)$
125	123	mulm1d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to -1 F_{ℝ}^{'} (- x) = - F_{ℝ}^{'} (- x)$
126	124 125	eqtrd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to F_{ℝ}^{'} (- x) -1 = - F_{ℝ}^{'} (- x)$
127	126	mpteq2dva	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ F_{ℝ}^{'} (- x) -1) = (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x))$
128	121 127	eqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} = (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x))$
129	128	dmeqd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to dom \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} = dom (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x))$
130		negex	$⊢ - F_{ℝ}^{'} (- x) \in V$
131		eqid	$⊢ (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x)) = (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x))$
132	130 131	dmmpti	$⊢ dom (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x)) = (- B, - a)$
133	129 132	eqtrdi	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to dom \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} = (- B, - a)$
134	56	ffvelrnda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land y \in (A, B)) \to G (y) \in ℝ$
135	134	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land y \in (A, B)) \to G (y) \in ℂ$
136		fvexd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land y \in (A, B)) \to G_{ℝ}^{'} (y) \in V$
137	56	feqmptd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G = (y \in (A, B) ⟼ G (y))$
138	137	oveq2d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ℝ D G = \frac{d (y \in (A, B)⟼ G (y))}{d_{ℝ} y}$
139		dvf	$⊢ G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
140	7	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to dom G_{ℝ}^{'} = (A, B)$
141	140	feq2d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ \leftrightarrow G_{ℝ}^{'} : (A, B) ⟶ ℂ)$
142	139 141	mpbii	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G_{ℝ}^{'} : (A, B) ⟶ ℂ$
143	142	feqmptd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ℝ D G = (y \in (A, B) ⟼ G_{ℝ}^{'} (y))$
144	138 143	eqtr3d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (y \in (A, B)⟼ G (y))}{d_{ℝ} y} = (y \in (A, B) ⟼ G_{ℝ}^{'} (y))$
145		fveq2	$⊢ y = - x \to G (y) = G (- x)$
146		fveq2	$⊢ y = - x \to G_{ℝ}^{'} (y) = G_{ℝ}^{'} (- x)$
147	91 91 49 93 135 136 110 144 145 146	dvmptco	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} = (x \in (- B, - a) ⟼ G_{ℝ}^{'} (- x) -1)$
148	142	adantr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} : (A, B) ⟶ ℂ$
149	148 49	ffvelrnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} (- x) \in ℂ$
150	149 93	mulcomd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} (- x) -1 = -1 G_{ℝ}^{'} (- x)$
151	149	mulm1d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to -1 G_{ℝ}^{'} (- x) = - G_{ℝ}^{'} (- x)$
152	150 151	eqtrd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} (- x) -1 = - G_{ℝ}^{'} (- x)$
153	152	mpteq2dva	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ G_{ℝ}^{'} (- x) -1) = (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x))$
154	147 153	eqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} = (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x))$
155	154	dmeqd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to dom \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} = dom (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x))$
156		negex	$⊢ - G_{ℝ}^{'} (- x) \in V$
157		eqid	$⊢ (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) = (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x))$
158	156 157	dmmpti	$⊢ dom (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) = (- B, - a)$
159	155 158	eqtrdi	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to dom \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} = (- B, - a)$
160	49	adantrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land (x \in (- B, - a) \land - x \neq B)) \to - x \in (A, B)$
161		limcresi	$⊢ (x \in ℝ ⟼ - x) {lim}_{ℂ} (- B) \subseteq ({(x \in ℝ ⟼ - x) ↾}_{(- B, - a)}) {lim}_{ℂ} (- B)$
162		resmpt	$⊢ (- B, - a) \subseteq ℝ \to {(x \in ℝ ⟼ - x) ↾}_{(- B, - a)} = (x \in (- B, - a) ⟼ - x)$
163	103 162	ax-mp	$⊢ {(x \in ℝ ⟼ - x) ↾}_{(- B, - a)} = (x \in (- B, - a) ⟼ - x)$
164	163	oveq1i	$⊢ ({(x \in ℝ ⟼ - x) ↾}_{(- B, - a)}) {lim}_{ℂ} (- B) = (x \in (- B, - a) ⟼ - x) {lim}_{ℂ} (- B)$
165	161 164	sseqtri	$⊢ (x \in ℝ ⟼ - x) {lim}_{ℂ} (- B) \subseteq (x \in (- B, - a) ⟼ - x) {lim}_{ℂ} (- B)$
166	78	recnd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in ℂ$
167	166	negnegd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - (- B) = B$
168		eqid	$⊢ (x \in ℝ ⟼ - x) = (x \in ℝ ⟼ - x)$
169	168	negcncf	$⊢ ℝ \subseteq ℂ \to (x \in ℝ ⟼ - x) : ℝ \underset{cn}{⟶} ℂ$
170	57 169	mp1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in ℝ ⟼ - x) : ℝ \underset{cn}{⟶} ℂ$
171		negeq	$⊢ x = - B \to - x = - (- B)$
172	170 82 171	cnmptlimc	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to - (- B) \in ((x \in ℝ ⟼ - x) {lim}_{ℂ} (- B))$
173	167 172	eqeltrrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in ((x \in ℝ ⟼ - x) {lim}_{ℂ} (- B))$
174	165 173	sselid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in ((x \in (- B, - a) ⟼ - x) {lim}_{ℂ} (- B))$
175	8	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to 0 \in (F {lim}_{ℂ} B)$
176	111	oveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to F {lim}_{ℂ} B = (y \in (A, B) ⟼ F (y)) {lim}_{ℂ} B$
177	175 176	eleqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to 0 \in ((y \in (A, B) ⟼ F (y)) {lim}_{ℂ} B)$
178		eliooord	$⊢ x \in (- B, - a) \to (- B < x \land x < - a)$
179	178	adantl	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (- B < x \land x < - a)$
180	179	simpld	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - B < x$
181	37 31 180	ltnegcon1d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - x < B$
182	38 181	ltned	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to - x \neq B$
183	182	neneqd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \neg - x = B$
184	183	pm2.21d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (- x = B \to F (- x) = 0)$
185	184	impr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land (x \in (- B, - a) \land - x = B)) \to F (- x) = 0$
186	160 96 174 177 119 185	limcco	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to 0 \in ((x \in (- B, - a) ⟼ F (- x)) {lim}_{ℂ} (- B))$
187	9	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to 0 \in (G {lim}_{ℂ} B)$
188	137	oveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G {lim}_{ℂ} B = (y \in (A, B) ⟼ G (y)) {lim}_{ℂ} B$
189	187 188	eleqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to 0 \in ((y \in (A, B) ⟼ G (y)) {lim}_{ℂ} B)$
190	183	pm2.21d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (- x = B \to G (- x) = 0)$
191	190	impr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land (x \in (- B, - a) \land - x = B)) \to G (- x) = 0$
192	160 135 174 189 145 191	limcco	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to 0 \in ((x \in (- B, - a) ⟼ G (- x)) {lim}_{ℂ} (- B))$
193	63	fmpttd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ G (- x)) : (- B, - a) ⟶ ran G$
194	193	frnd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ran (x \in (- B, - a) ⟼ G (- x)) \subseteq ran G$
195	10	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \neg 0 \in ran G$
196	194 195	ssneldd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \neg 0 \in ran (x \in (- B, - a) ⟼ G (- x))$
197	11	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \neg 0 \in ran G_{ℝ}^{'}$
198	154	rneqd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ran \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} = ran (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x))$
199	198	eleq2d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (0 \in ran \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} \leftrightarrow 0 \in ran (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)))$
200	157 156	elrnmpti	$⊢ 0 \in ran (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) \leftrightarrow \exists x \in (- B, - a) 0 = - G_{ℝ}^{'} (- x)$
201		eqcom	$⊢ 0 = - G_{ℝ}^{'} (- x) \leftrightarrow - G_{ℝ}^{'} (- x) = 0$
202	149	negeq0d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (G_{ℝ}^{'} (- x) = 0 \leftrightarrow - G_{ℝ}^{'} (- x) = 0)$
203	148	ffnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} Fn (A, B)$
204		fnfvelrn	$⊢ (G_{ℝ}^{'} Fn (A, B) \land - x \in (A, B)) \to G_{ℝ}^{'} (- x) \in ran G_{ℝ}^{'}$
205	203 49 204	syl2anc	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} (- x) \in ran G_{ℝ}^{'}$
206		eleq1	$⊢ G_{ℝ}^{'} (- x) = 0 \to (G_{ℝ}^{'} (- x) \in ran G_{ℝ}^{'} \leftrightarrow 0 \in ran G_{ℝ}^{'})$
207	205 206	syl5ibcom	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (G_{ℝ}^{'} (- x) = 0 \to 0 \in ran G_{ℝ}^{'})$
208	202 207	sylbird	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (- G_{ℝ}^{'} (- x) = 0 \to 0 \in ran G_{ℝ}^{'})$
209	201 208	syl5bi	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (0 = - G_{ℝ}^{'} (- x) \to 0 \in ran G_{ℝ}^{'})$
210	209	rexlimdva	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (\exists x \in (- B, - a) 0 = - G_{ℝ}^{'} (- x) \to 0 \in ran G_{ℝ}^{'})$
211	200 210	syl5bi	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (0 \in ran (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) \to 0 \in ran G_{ℝ}^{'})$
212	199 211	sylbid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (0 \in ran \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} \to 0 \in ran G_{ℝ}^{'})$
213	197 212	mtod	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \neg 0 \in ran \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x}$
214	116	ffvelrnda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to F_{ℝ}^{'} (z) \in ℂ$
215	142	ffvelrnda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in ℂ$
216	11	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to \neg 0 \in ran G_{ℝ}^{'}$
217	142	ffnd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G_{ℝ}^{'} Fn (A, B)$
218		fnfvelrn	$⊢ (G_{ℝ}^{'} Fn (A, B) \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in ran G_{ℝ}^{'}$
219	217 218	sylan	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in ran G_{ℝ}^{'}$
220		eleq1	$⊢ G_{ℝ}^{'} (z) = 0 \to (G_{ℝ}^{'} (z) \in ran G_{ℝ}^{'} \leftrightarrow 0 \in ran G_{ℝ}^{'})$
221	219 220	syl5ibcom	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to (G_{ℝ}^{'} (z) = 0 \to 0 \in ran G_{ℝ}^{'})$
222	221	necon3bd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to (\neg 0 \in ran G_{ℝ}^{'} \to G_{ℝ}^{'} (z) \neq 0)$
223	216 222	mpd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to G_{ℝ}^{'} (z) \neq 0$
224	214 215 223	divcld	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)} \in ℂ$
225	12	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} B)$
226		fveq2	$⊢ z = - x \to F_{ℝ}^{'} (z) = F_{ℝ}^{'} (- x)$
227		fveq2	$⊢ z = - x \to G_{ℝ}^{'} (z) = G_{ℝ}^{'} (- x)$
228	226 227	oveq12d	$⊢ z = - x \to \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)} = \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)}$
229	183	pm2.21d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (- x = B \to \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)} = C)$
230	229	impr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land (x \in (- B, - a) \land - x = B)) \to \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)} = C$
231	160 224 174 225 228 230	limcco	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((x \in (- B, - a) ⟼ \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)}) {lim}_{ℂ} (- B))$
232		nfcv	$⊢ \underline{Ⅎ} x ℝ$
233		nfcv	$⊢ \underline{Ⅎ} x D$
234		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (- B, - a) ⟼ F (- x))$
235	232 233 234	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x}$
236		nfcv	$⊢ \underline{Ⅎ} x y$
237	235 236	nffv	$⊢ \underline{Ⅎ} x \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)$
238		nfcv	$⊢ \underline{Ⅎ} x \div$
239		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (- B, - a) ⟼ G (- x))$
240	232 233 239	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x}$
241	240 236	nffv	$⊢ \underline{Ⅎ} x \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)$
242	237 238 241	nfov	$⊢ \underline{Ⅎ} x (\frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)})$
243		nfcv	$⊢ \underline{Ⅎ} y (\frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)})$
244		fveq2	$⊢ y = x \to \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y) = \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)$
245		fveq2	$⊢ y = x \to \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y) = \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)$
246	244 245	oveq12d	$⊢ y = x \to \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)} = \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)}$
247	242 243 246	cbvmpt	$⊢ (y \in (- B, - a) ⟼ \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)}) = (x \in (- B, - a) ⟼ \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)})$
248	128	fveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x) = (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x)) (x)$
249	131	fvmpt2	$⊢ (x \in (- B, - a) \land - F_{ℝ}^{'} (- x) \in V) \to (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x)) (x) = - F_{ℝ}^{'} (- x)$
250	130 249	mpan2	$⊢ x \in (- B, - a) \to (x \in (- B, - a) ⟼ - F_{ℝ}^{'} (- x)) (x) = - F_{ℝ}^{'} (- x)$
251	248 250	sylan9eq	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x) = - F_{ℝ}^{'} (- x)$
252	154	fveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x) = (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) (x)$
253	157	fvmpt2	$⊢ (x \in (- B, - a) \land - G_{ℝ}^{'} (- x) \in V) \to (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) (x) = - G_{ℝ}^{'} (- x)$
254	156 253	mpan2	$⊢ x \in (- B, - a) \to (x \in (- B, - a) ⟼ - G_{ℝ}^{'} (- x)) (x) = - G_{ℝ}^{'} (- x)$
255	252 254	sylan9eq	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x) = - G_{ℝ}^{'} (- x)$
256	251 255	oveq12d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)} = \frac{- F_{ℝ}^{'} (- x)}{- G_{ℝ}^{'} (- x)}$
257	11	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \neg 0 \in ran G_{ℝ}^{'}$
258	207	necon3bd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (\neg 0 \in ran G_{ℝ}^{'} \to G_{ℝ}^{'} (- x) \neq 0)$
259	257 258	mpd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to G_{ℝ}^{'} (- x) \neq 0$
260	123 149 259	div2negd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{- F_{ℝ}^{'} (- x)}{- G_{ℝ}^{'} (- x)} = \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)}$
261	256 260	eqtrd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)} = \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)}$
262	261	mpteq2dva	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (x)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (x)}) = (x \in (- B, - a) ⟼ \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)})$
263	247 262	syl5eq	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (y \in (- B, - a) ⟼ \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)}) = (x \in (- B, - a) ⟼ \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)})$
264	263	oveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (y \in (- B, - a) ⟼ \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)}) {lim}_{ℂ} (- B) = (x \in (- B, - a) ⟼ \frac{F_{ℝ}^{'} (- x)}{G_{ℝ}^{'} (- x)}) {lim}_{ℂ} (- B)$
265	231 264	eleqtrrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((y \in (- B, - a) ⟼ \frac{\frac{d (x \in (- B, - a)⟼ F (- x))}{d_{ℝ} x} (y)}{\frac{d (x \in (- B, - a)⟼ G (- x))}{d_{ℝ} x} (y)}) {lim}_{ℂ} (- B))$
266	82 84 87 88 89 133 159 186 192 196 213 265	lhop1	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((y \in (- B, - a) ⟼ \frac{(x \in (- B, - a) ⟼ F (- x)) (y)}{(x \in (- B, - a) ⟼ G (- x)) (y)}) {lim}_{ℂ} (- B))$
267		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in (- B, - a) ⟼ F (- x)) (y)$
268		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in (- B, - a) ⟼ G (- x)) (y)$
269	267 238 268	nfov	$⊢ \underline{Ⅎ} x (\frac{(x \in (- B, - a) ⟼ F (- x)) (y)}{(x \in (- B, - a) ⟼ G (- x)) (y)})$
270		nfcv	$⊢ \underline{Ⅎ} y (\frac{(x \in (- B, - a) ⟼ F (- x)) (x)}{(x \in (- B, - a) ⟼ G (- x)) (x)})$
271		fveq2	$⊢ y = x \to (x \in (- B, - a) ⟼ F (- x)) (y) = (x \in (- B, - a) ⟼ F (- x)) (x)$
272		fveq2	$⊢ y = x \to (x \in (- B, - a) ⟼ G (- x)) (y) = (x \in (- B, - a) ⟼ G (- x)) (x)$
273	271 272	oveq12d	$⊢ y = x \to \frac{(x \in (- B, - a) ⟼ F (- x)) (y)}{(x \in (- B, - a) ⟼ G (- x)) (y)} = \frac{(x \in (- B, - a) ⟼ F (- x)) (x)}{(x \in (- B, - a) ⟼ G (- x)) (x)}$
274	269 270 273	cbvmpt	$⊢ (y \in (- B, - a) ⟼ \frac{(x \in (- B, - a) ⟼ F (- x)) (y)}{(x \in (- B, - a) ⟼ G (- x)) (y)}) = (x \in (- B, - a) ⟼ \frac{(x \in (- B, - a) ⟼ F (- x)) (x)}{(x \in (- B, - a) ⟼ G (- x)) (x)})$
275		fvex	$⊢ F (- x) \in V$
276		eqid	$⊢ (x \in (- B, - a) ⟼ F (- x)) = (x \in (- B, - a) ⟼ F (- x))$
277	276	fvmpt2	$⊢ (x \in (- B, - a) \land F (- x) \in V) \to (x \in (- B, - a) ⟼ F (- x)) (x) = F (- x)$
278	34 275 277	sylancl	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (x \in (- B, - a) ⟼ F (- x)) (x) = F (- x)$
279		fvex	$⊢ G (- x) \in V$
280		eqid	$⊢ (x \in (- B, - a) ⟼ G (- x)) = (x \in (- B, - a) ⟼ G (- x))$
281	280	fvmpt2	$⊢ (x \in (- B, - a) \land G (- x) \in V) \to (x \in (- B, - a) ⟼ G (- x)) (x) = G (- x)$
282	34 279 281	sylancl	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to (x \in (- B, - a) ⟼ G (- x)) (x) = G (- x)$
283	278 282	oveq12d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land x \in (- B, - a)) \to \frac{(x \in (- B, - a) ⟼ F (- x)) (x)}{(x \in (- B, - a) ⟼ G (- x)) (x)} = \frac{F (- x)}{G (- x)}$
284	283	mpteq2dva	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (x \in (- B, - a) ⟼ \frac{(x \in (- B, - a) ⟼ F (- x)) (x)}{(x \in (- B, - a) ⟼ G (- x)) (x)}) = (x \in (- B, - a) ⟼ \frac{F (- x)}{G (- x)})$
285	274 284	syl5eq	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (y \in (- B, - a) ⟼ \frac{(x \in (- B, - a) ⟼ F (- x)) (y)}{(x \in (- B, - a) ⟼ G (- x)) (y)}) = (x \in (- B, - a) ⟼ \frac{F (- x)}{G (- x)})$
286	285	oveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (y \in (- B, - a) ⟼ \frac{(x \in (- B, - a) ⟼ F (- x)) (y)}{(x \in (- B, - a) ⟼ G (- x)) (y)}) {lim}_{ℂ} (- B) = (x \in (- B, - a) ⟼ \frac{F (- x)}{G (- x)}) {lim}_{ℂ} (- B)$
287	266 286	eleqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((x \in (- B, - a) ⟼ \frac{F (- x)}{G (- x)}) {lim}_{ℂ} (- B))$
288		negeq	$⊢ x = - z \to - x = - (- z)$
289	288	fveq2d	$⊢ x = - z \to F (- x) = F (- (- z))$
290	288	fveq2d	$⊢ x = - z \to G (- x) = G (- (- z))$
291	289 290	oveq12d	$⊢ x = - z \to \frac{F (- x)}{G (- x)} = \frac{F (- (- z))}{G (- (- z))}$
292	82	adantr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to - B \in ℝ$
293		eliooord	$⊢ z \in (a, B) \to (a < z \land z < B)$
294	293	adantl	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to (a < z \land z < B)$
295	294	simprd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to z < B$
296	24 22	ltnegd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to (z < B \leftrightarrow - B < - z)$
297	295 296	mpbid	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to - B < - z$
298	292 297	gtned	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to - z \neq - B$
299	298	neneqd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to \neg - z = - B$
300	299	pm2.21d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to (- z = - B \to \frac{F (- (- z))}{G (- (- z))} = C)$
301	300	impr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land (z \in (a, B) \land - z = - B)) \to \frac{F (- (- z))}{G (- (- z))} = C$
302	28 68 81 287 291 301	limcco	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((z \in (a, B) ⟼ \frac{F (- (- z))}{G (- (- z))}) {lim}_{ℂ} B)$
303	24	recnd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to z \in ℂ$
304	303	negnegd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to - (- z) = z$
305	304	fveq2d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to F (- (- z)) = F (z)$
306	304	fveq2d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to G (- (- z)) = G (z)$
307	305 306	oveq12d	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (a, B)) \to \frac{F (- (- z))}{G (- (- z))} = \frac{F (z)}{G (z)}$
308	307	mpteq2dva	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (z \in (a, B) ⟼ \frac{F (- (- z))}{G (- (- z))}) = (z \in (a, B) ⟼ \frac{F (z)}{G (z)})$
309	308	oveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (z \in (a, B) ⟼ \frac{F (- (- z))}{G (- (- z))}) {lim}_{ℂ} B = (z \in (a, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
310	47	resmptd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to {(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) ↾}_{(a, B)} = (z \in (a, B) ⟼ \frac{F (z)}{G (z)})$
311	310	oveq1d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ({(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) ↾}_{(a, B)}) {lim}_{ℂ} B = (z \in (a, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
312		fss	$⊢ (F : (A, B) ⟶ ℝ \land ℝ \subseteq ℂ) \to F : (A, B) ⟶ ℂ$
313	94 57 312	sylancl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to F : (A, B) ⟶ ℂ$
314	313	ffvelrnda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to F (z) \in ℂ$
315	59	ffvelrnda	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to G (z) \in ℂ$
316	10	ad2antrr	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to \neg 0 \in ran G$
317	56	ffnd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to G Fn (A, B)$
318		fnfvelrn	$⊢ (G Fn (A, B) \land z \in (A, B)) \to G (z) \in ran G$
319	317 318	sylan	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to G (z) \in ran G$
320		eleq1	$⊢ G (z) = 0 \to (G (z) \in ran G \leftrightarrow 0 \in ran G)$
321	319 320	syl5ibcom	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to (G (z) = 0 \to 0 \in ran G)$
322	321	necon3bd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to (\neg 0 \in ran G \to G (z) \neq 0)$
323	316 322	mpd	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to G (z) \neq 0$
324	314 315 323	divcld	$⊢ ((φ \land (a \in ℝ \land (A < a \land a < B))) \land z \in (A, B)) \to \frac{F (z)}{G (z)} \in ℂ$
325	324	fmpttd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (z \in (A, B) ⟼ \frac{F (z)}{G (z)}) : (A, B) ⟶ ℂ$
326		ioossre	$⊢ (A, B) \subseteq ℝ$
327	326 57	sstri	$⊢ (A, B) \subseteq ℂ$
328	327	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (A, B) \subseteq ℂ$
329		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\})$
330		ssun2	$⊢ \{B\} \subseteq (a, B) \cup \{B\}$
331		snssg	$⊢ B \in ℝ \to (B \in ((a, B) \cup \{B\}) \leftrightarrow \{B\} \subseteq (a, B) \cup \{B\})$
332	78 331	syl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (B \in ((a, B) \cup \{B\}) \leftrightarrow \{B\} \subseteq (a, B) \cup \{B\})$
333	330 332	mpbiri	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in ((a, B) \cup \{B\})$
334	105	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
335	326	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (A, B) \subseteq ℝ$
336	78	snssd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \{B\} \subseteq ℝ$
337	335 336	unssd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (A, B) \cup \{B\} \subseteq ℝ$
338	337 57	sstrdi	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (A, B) \cup \{B\} \subseteq ℂ$
339		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (A, B) \cup \{B\} \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) \in TopOn ((A, B) \cup \{B\})$
340	334 338 339	sylancr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) \in TopOn ((A, B) \cup \{B\})$
341		topontop	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) \in TopOn ((A, B) \cup \{B\}) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) \in Top$
342	340 341	syl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) \in Top$
343		indi	$⊢ (a, +∞) \cap ((A, B) \cup \{B\}) = ((a, +∞) \cap (A, B)) \cup ((a, +∞) \cap \{B\})$
344		pnfxr	$⊢ +∞ \in ℝ^{*}$
345	344	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to +∞ \in ℝ^{*}$
346	14	adantr	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in ℝ^{*}$
347		iooin	$⊢ ((a \in ℝ^{} \land +∞ \in ℝ^{}) \land (A \in ℝ^{} \land B \in ℝ^{})) \to (a, +∞) \cap (A, B) = (if (a \leq A, A, a), if (+∞ \leq B, +∞, B))$
348	43 345 42 346 347	syl22anc	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, +∞) \cap (A, B) = (if (a \leq A, A, a), if (+∞ \leq B, +∞, B))$
349		xrltnle	$⊢ (A \in ℝ^{} \land a \in ℝ^{}) \to (A < a \leftrightarrow \neg a \leq A)$
350	42 43 349	syl2anc	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (A < a \leftrightarrow \neg a \leq A)$
351	44 350	mpbid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \neg a \leq A$
352	351	iffalsed	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to if (a \leq A, A, a) = a$
353	78	ltpnfd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B < +∞$
354		xrltnle	$⊢ (B \in ℝ^{} \land +∞ \in ℝ^{}) \to (B < +∞ \leftrightarrow \neg +∞ \leq B)$
355	346 344 354	sylancl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (B < +∞ \leftrightarrow \neg +∞ \leq B)$
356	353 355	mpbid	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \neg +∞ \leq B$
357	356	iffalsed	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to if (+∞ \leq B, +∞, B) = B$
358	352 357	oveq12d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (if (a \leq A, A, a), if (+∞ \leq B, +∞, B)) = (a, B)$
359	348 358	eqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, +∞) \cap (A, B) = (a, B)$
360		elioopnf	$⊢ a \in ℝ^{*} \to (B \in (a, +∞) \leftrightarrow (B \in ℝ \land a < B))$
361	43 360	syl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (B \in (a, +∞) \leftrightarrow (B \in ℝ \land a < B))$
362	78 85 361	mpbir2and	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in (a, +∞)$
363	362	snssd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to \{B\} \subseteq (a, +∞)$
364		sseqin2	$⊢ \{B\} \subseteq (a, +∞) \leftrightarrow (a, +∞) \cap \{B\} = \{B\}$
365	363 364	sylib	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, +∞) \cap \{B\} = \{B\}$
366	359 365	uneq12d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ((a, +∞) \cap (A, B)) \cup ((a, +∞) \cap \{B\}) = (a, B) \cup \{B\}$
367	343 366	syl5eq	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, +∞) \cap ((A, B) \cup \{B\}) = (a, B) \cup \{B\}$
368		retop	$⊢ topGen (ran (.)) \in Top$
369		reex	$⊢ ℝ \in V$
370	369	ssex	$⊢ (A, B) \cup \{B\} \subseteq ℝ \to (A, B) \cup \{B\} \in V$
371	337 370	syl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (A, B) \cup \{B\} \in V$
372		iooretop	$⊢ (a, +∞) \in topGen (ran (.))$
373	372	a1i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, +∞) \in topGen (ran (.))$
374		elrestr	$⊢ (topGen (ran (.)) \in Top \land (A, B) \cup \{B\} \in V \land (a, +∞) \in topGen (ran (.))) \to (a, +∞) \cap ((A, B) \cup \{B\}) \in (topGen (ran (.)) ↾_{𝑡} ((A, B) \cup \{B\}))$
375	368 371 373 374	mp3an2i	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, +∞) \cap ((A, B) \cup \{B\}) \in (topGen (ran (.)) ↾_{𝑡} ((A, B) \cup \{B\}))$
376	367 375	eqeltrrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, B) \cup \{B\} \in (topGen (ran (.)) ↾_{𝑡} ((A, B) \cup \{B\}))$
377		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
378	105 377	rerest	$⊢ (A, B) \cup \{B\} \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) = topGen (ran (.)) ↾_{𝑡} ((A, B) \cup \{B\})$
379	337 378	syl	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) = topGen (ran (.)) ↾_{𝑡} ((A, B) \cup \{B\})$
380	376 379	eleqtrrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (a, B) \cup \{B\} \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}))$
381		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}) \in Top \land (a, B) \cup \{B\} \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\}))) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\})) ((a, B) \cup \{B\}) = (a, B) \cup \{B\}$
382	342 380 381	syl2anc	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\})) ((a, B) \cup \{B\}) = (a, B) \cup \{B\}$
383	333 382	eleqtrrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\})) ((a, B) \cup \{B\})$
384	325 47 328 105 329 383	limcres	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to ({(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) ↾}_{(a, B)}) {lim}_{ℂ} B = (z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
385	309 311 384	3eqtr2d	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to (z \in (a, B) ⟼ \frac{F (- (- z))}{G (- (- z))}) {lim}_{ℂ} B = (z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B$
386	302 385	eleqtrd	$⊢ (φ \land (a \in ℝ \land (A < a \land a < B))) \to C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B)$
387	18 386	rexlimddv	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem lhop2

Proof