Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	lhop2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	lhop2.l	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	lhop2.f	⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
	lhop2.g	⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
	lhop2.if	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
	lhop2.ig	⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
	lhop2.f0	⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝐵 ) )
	lhop2.g0	⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝐵 ) )
	lhop2.gn0	⊢ ( 𝜑 → ¬ 0 ∈ ran 𝐺 )
	lhop2.gd0	⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
	lhop2.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
Assertion	lhop2	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )

Proof

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