Metamath Proof Explorer

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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
106 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
107 iooretop ⊢ ( - 𝐵 (,) - 𝑎 ) ∈ ( topGen ‘ ran (,) )
108 107 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( - 𝐵 (,) - 𝑎 ) ∈ ( topGen ‘ ran (,) ) )
109 91 100 101 102 104 105 106 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 106 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 106 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 106 329 383 limcres ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝑎 (,) 𝐵 ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
385 309 311 384 3eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
386 302 385 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
387 18 386 rexlimddv ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )