lhop2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lhop2		Structured version Visualization version GIF version

Theorem lhop2 26001

Description: L'Hôpital's Rule for limits from the left. If 𝐹 and 𝐺 are differentiable real functions on (𝐴, 𝐵), and 𝐹 and 𝐺 both approach 0 at 𝐵, and 𝐺(𝑥) and 𝐺' (𝑥) are not zero on (𝐴, 𝐵), and the limit of 𝐹' (𝑥) / 𝐺' (𝑥) at 𝐵 is 𝐶, then the limit 𝐹(𝑥) / 𝐺(𝑥) at 𝐵 also exists and equals 𝐶. (Contributed by Mario Carneiro, 29-Dec-2016.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
lhop2	⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))

Distinct variable groups: 𝑧,𝐴 𝑧,𝐵 𝑧,𝐶 𝜑,𝑧 𝑧,𝐹 𝑧,𝐺

Proof of Theorem lhop2 Dummy variables 𝑥 𝑎 𝑦 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∃wrex 3063 Vcvv 3431 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ifcif 4455 {csn 4556 {cpr 4558 class class class wbr 5073 ↦ cmpt 5154 dom cdm 5619 ran crn 5620 ↾ cres 5621 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 (class class class)co 7357 ℂcc 11028 ℝcr 11029 0cc0 11030 1c1 11031 · cmul 11035 +∞cpnf 11168 ℝ^*cxr 11170 < clt 11171 ≤ cle 11172 -cneg 11370 / cdiv 11799 ℚcq 12890 (,)cioo 13290 ↾_t crest 17375 TopOpenctopn 17376 topGenctg 17392 ℂ_fldccnfld 21348 Topctop 22877 TopOnctopon 22894 intcnt 23001 –cn→ccncf 24862 lim_ℂ climc 25848 D cdv 25849

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108 ax-addf 11109

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-iin 4925 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7621 df-om 7808 df-1st 7932 df-2nd 7933 df-supp 8102 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-pm 8767 df-ixp 8837 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-fi 9315 df-sup 9346 df-inf 9347 df-oi 9416 df-card 9855 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-div 11800 df-nn 12167 df-2 12236 df-3 12237 df-4 12238 df-5 12239 df-6 12240 df-7 12241 df-8 12242 df-9 12243 df-n0 12430 df-z 12517 df-dec 12637 df-uz 12781 df-q 12891 df-rp 12935 df-xneg 13055 df-xadd 13056 df-xmul 13057 df-ioo 13294 df-ioc 13295 df-ico 13296 df-icc 13297 df-fz 13454 df-fzo 13601 df-seq 13956 df-exp 14016 df-hash 14285 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-struct 17109 df-sets 17126 df-slot 17144 df-ndx 17156 df-base 17172 df-ress 17193 df-plusg 17225 df-mulr 17226 df-starv 17227 df-sca 17228 df-vsca 17229 df-ip 17230 df-tset 17231 df-ple 17232 df-ds 17234 df-unif 17235 df-hom 17236 df-cco 17237 df-rest 17377 df-topn 17378 df-0g 17396 df-gsum 17397 df-topgen 17398 df-pt 17399 df-prds 17402 df-xrs 17458 df-qtop 17463 df-imas 17464 df-xps 17466 df-mre 17540 df-mrc 17541 df-acs 17543 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-submnd 18744 df-mulg 19036 df-cntz 19284 df-cmn 19749 df-psmet 21340 df-xmet 21341 df-met 21342 df-bl 21343 df-mopn 21344 df-fbas 21345 df-fg 21346 df-cnfld 21349 df-top 22878 df-topon 22895 df-topsp 22917 df-bases 22930 df-cld 23003 df-ntr 23004 df-cls 23005 df-nei 23082 df-lp 23120 df-perf 23121 df-cn 23211 df-cnp 23212 df-haus 23299 df-cmp 23371 df-tx 23546 df-hmeo 23739 df-fil 23830 df-fm 23922 df-flim 23923 df-flf 23924 df-xms 24304 df-ms 24305 df-tms 24306 df-cncf 24864 df-limc 25852 df-dv 25853

This theorem is referenced by: lhop 26002 fourierdlem60 46617

W3C validator