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 25982

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 12909	. . 3 ⊢ ℚ ⊆ ℝ
2		lhop2.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
3		lhop2.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 11195	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
5		lhop2.l	. . . 4 ⊢ (𝜑 → 𝐴 < 𝐵)
6		qbtwnxr 13152	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))
7	2, 4, 5, 6	syl3anc 1374	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))
8		ssrexv 3991	. . 3 ⊢ (ℚ ⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)))
9	1, 7, 8	mpsyl 68	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))
10		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵))
11		simprl 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ)
12	11	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ)
13	3	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ)
14		elioore 13328	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ)
15	14	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ)
16		iooneg 13424	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
17	12, 13, 15, 16	syl3anc 1374	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
18	10, 17	mpbid 232	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
19	18	adantrr 718	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
20		lhop2.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
21	20	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
22		elioore 13328	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ)
23	22	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ)
24	23	recnd 11173	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ)
25	24	negnegd 11496	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥)
26		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎))
27	25, 26	eqeltrd 2836	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎))
28	11	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ)
29	3	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ)
30	23	renegcld 11577	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ)
31		iooneg 13424	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
32	28, 29, 30, 31	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
33	27, 32	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵))
34	2	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ∈ ℝ^*)
35	11	rexrd 11195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ^*)
36		simprrl 781	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 < 𝑎)
37	34, 35, 36	xrltled 13101	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ≤ 𝑎)
38		iooss1 13333	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ 𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
39	34, 37, 38	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
40	39	sselda 3921	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
41	33, 40	syldan 592	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵))
42	21, 41	ffvelcdmd 7037	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ)
43	42	recnd 11173	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ)
44		lhop2.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ)
45	44	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
46	45, 41	ffvelcdmd 7037	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ)
47	46	recnd 11173	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ)
48		lhop2.gn0	. . . . . . 7 ⊢ (𝜑 → ¬ 0 ∈ ran 𝐺)
49	48	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺)
50	44	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
51		ax-resscn 11095	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℂ
52		fss 6684	. . . . . . . . . . . 12 ⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
53	50, 51, 52	sylancl 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
54	53	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
55	54	ffnd 6669	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵))
56		fnfvelrn 7032	. . . . . . . . 9 ⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺)
57	55, 41, 56	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺)
58		eleq1 2824	. . . . . . . 8 ⊢ ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
59	57, 58	syl5ibcom 245	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺))
60	59	necon3bd 2946	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0))
61	49, 60	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0)
62	43, 47, 61	divcld 11931	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ)
63		limcresi 25852	. . . . . 6 ⊢ ((𝑧 ∈ ℝ ↦ -𝑧) lim_ℂ 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵)
64		ioossre 13360	. . . . . . . 8 ⊢ (𝑎(,)𝐵) ⊆ ℝ
65		resmpt 6002	. . . . . . . 8 ⊢ ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧))
66	64, 65	ax-mp 5	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)
67	66	oveq1i 7377	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim_ℂ 𝐵)
68	63, 67	sseqtri 3970	. . . . 5 ⊢ ((𝑧 ∈ ℝ ↦ -𝑧) lim_ℂ 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim_ℂ 𝐵)
69		eqid 2736	. . . . . . . 8 ⊢ (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧)
70	69	negcncf 24889	. . . . . . 7 ⊢ (ℝ ⊆ ℂ → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
71	51, 70	mp1i 13	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
72	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℝ)
73		negeq 11385	. . . . . 6 ⊢ (𝑧 = 𝐵 → -𝑧 = -𝐵)
74	71, 72, 73	cnmptlimc 25857	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) lim_ℂ 𝐵))
75	68, 74	sselid 3919	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim_ℂ 𝐵))
76	72	renegcld 11577	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ℝ)
77	11	renegcld 11577	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ)
78	77	rexrd 11195	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ^*)
79		simprrr 782	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 < 𝐵)
80	11, 72	ltnegd 11728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎))
81	79, 80	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 < -𝑎)
82	42	fmpttd 7067	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
83	46	fmpttd 7067	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
84		reelprrecn 11130	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
85	84	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ℝ ∈ {ℝ, ℂ})
86		neg1cn 12144	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
87	86	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ)
88	20	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
89	88	ffvelcdmda 7036	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℝ)
90	89	recnd 11173	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℂ)
91		fvexd 6855	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V)
92		1cnd 11139	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ)
93		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
94	93	recnd 11173	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
95		1cnd 11139	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
96	85	dvmptid 25924	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
97		ioossre 13360	. . . . . . . . . . . . 13 ⊢ (-𝐵(,)-𝑎) ⊆ ℝ
98	97	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ)
99		tgioo4 24770	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
100		eqid 2736	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
101		iooretop 24730	. . . . . . . . . . . . 13 ⊢ (-𝐵(,)-𝑎) ∈ (topGen‘ran (,))
102	101	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran (,)))
103	85, 94, 95, 96, 98, 99, 100, 102	dvmptres 25930	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1))
104	85, 24, 92, 103	dvmptneg 25933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1))
105	88	feqmptd 6908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)))
106	105	oveq2d 7383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))))
107		dvf 25874	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
108		lhop2.if	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
109	108	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110	109	feq2d 6652	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
111	107, 110	mpbii 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
112	111	feqmptd 6908	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
113	106, 112	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
114		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → (𝐹‘𝑦) = (𝐹‘-𝑥))
115		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥))
116	85, 85, 41, 87, 90, 91, 104, 113, 114, 115	dvmptco 25939	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)))
117	111	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
118	117, 41	ffvelcdmd 7037	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ)
119	118, 87	mulcomd 11166	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐹)‘-𝑥)))
120	118	mulm1d 11602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥))
121	119, 120	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥))
122	121	mpteq2dva 5178	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
123	116, 122	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
124	123	dmeqd 5860	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
125		negex 11391	. . . . . . . 8 ⊢ -((ℝ D 𝐹)‘-𝑥) ∈ V
126		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))
127	125, 126	dmmpti 6642	. . . . . . 7 ⊢ dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎)
128	124, 127	eqtrdi 2787	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎))
129	50	ffvelcdmda 7036	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℝ)
130	129	recnd 11173	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℂ)
131		fvexd 6855	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V)
132	50	feqmptd 6908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)))
133	132	oveq2d 7383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))))
134		dvf 25874	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
135		lhop2.ig	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
136	135	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
137	136	feq2d 6652	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
138	134, 137	mpbii 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
139	138	feqmptd 6908	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
140	133, 139	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
141		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → (𝐺‘𝑦) = (𝐺‘-𝑥))
142		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥))
143	85, 85, 41, 87, 130, 131, 104, 140, 141, 142	dvmptco 25939	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)))
144	138	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
145	144, 41	ffvelcdmd 7037	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ)
146	145, 87	mulcomd 11166	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐺)‘-𝑥)))
147	145	mulm1d 11602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥))
148	146, 147	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥))
149	148	mpteq2dva 5178	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
150	143, 149	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
151	150	dmeqd 5860	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
152		negex 11391	. . . . . . . 8 ⊢ -((ℝ D 𝐺)‘-𝑥) ∈ V
153		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))
154	152, 153	dmmpti 6642	. . . . . . 7 ⊢ dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎)
155	151, 154	eqtrdi 2787	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎))
156	41	adantrr 718	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 ≠ 𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
157		limcresi 25852	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim_ℂ -𝐵)
158		resmpt 6002	. . . . . . . . . . 11 ⊢ ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥))
159	97, 158	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)
160	159	oveq1i 7377	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim_ℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim_ℂ -𝐵)
161	157, 160	sseqtri 3970	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim_ℂ -𝐵)
162	72	recnd 11173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℂ)
163	162	negnegd 11496	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 = 𝐵)
164		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥)
165	164	negcncf 24889	. . . . . . . . . . 11 ⊢ (ℝ ⊆ ℂ → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
166	51, 165	mp1i 13	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
167		negeq 11385	. . . . . . . . . 10 ⊢ (𝑥 = -𝐵 → -𝑥 = --𝐵)
168	166, 76, 167	cnmptlimc 25857	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵))
169	163, 168	eqeltrrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵))
170	161, 169	sselid 3919	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim_ℂ -𝐵))
171		lhop2.f0	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐵))
172	171	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐹 lim_ℂ 𝐵))
173	105	oveq1d 7382	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐹 lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) lim_ℂ 𝐵))
174	172, 173	eleqtrd 2838	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) lim_ℂ 𝐵))
175		eliooord 13358	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎))
176	175	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎))
177	176	simpld 494	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥)
178	29, 23, 177	ltnegcon1d 11730	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵)
179	30, 178	ltned 11282	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ≠ 𝐵)
180	179	neneqd 2937	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵)
181	180	pm2.21d 121	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0))
182	181	impr 454	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0)
183	156, 90, 170, 174, 114, 182	limcco 25860	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) lim_ℂ -𝐵))
184		lhop2.g0	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (𝐺 lim_ℂ 𝐵))
185	184	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐺 lim_ℂ 𝐵))
186	132	oveq1d 7382	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐺 lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) lim_ℂ 𝐵))
187	185, 186	eleqtrd 2838	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) lim_ℂ 𝐵))
188	180	pm2.21d 121	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0))
189	188	impr 454	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0)
190	156, 130, 170, 187, 141, 189	limcco 25860	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) lim_ℂ -𝐵))
191	57	fmpttd 7067	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺)
192	191	frnd 6676	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
193	48	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺)
194	192, 193	ssneldd 3924	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
195		lhop2.gd0	. . . . . . . 8 ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
196	195	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D 𝐺))
197	150	rneqd 5893	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
198	197	eleq2d 2822	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))))
199	153, 152	elrnmpti 5917	. . . . . . . . 9 ⊢ (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥))
200		eqcom 2743	. . . . . . . . . . 11 ⊢ (0 = -((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0)
201	145	negeq0d 11497	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0))
202	144	ffnd 6669	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
203		fnfvelrn 7032	. . . . . . . . . . . . . 14 ⊢ (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
204	202, 41, 203	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
205		eleq1 2824	. . . . . . . . . . . . 13 ⊢ (((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
206	204, 205	syl5ibcom 245	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
207	201, 206	sylbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
208	200, 207	biimtrid 242	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
209	208	rexlimdva 3138	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
210	199, 209	biimtrid 242	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺)))
211	198, 210	sylbid 240	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺)))
212	196, 211	mtod 198	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))))
213	111	ffvelcdmda 7036	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ)
214	138	ffvelcdmda 7036	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ)
215	195	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D 𝐺))
216	138	ffnd 6669	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
217		fnfvelrn 7032	. . . . . . . . . . . . 13 ⊢ (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
218	216, 217	sylan 581	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
219		eleq1 2824	. . . . . . . . . . . 12 ⊢ (((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
220	218, 219	syl5ibcom 245	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺)))
221	220	necon3bd 2946	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0))
222	215, 221	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0)
223	213, 214, 222	divcld 11931	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ)
224		lhop2.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim_ℂ 𝐵))
225	224	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim_ℂ 𝐵))
226		fveq2 6840	. . . . . . . . 9 ⊢ (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥))
227		fveq2 6840	. . . . . . . . 9 ⊢ (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥))
228	226, 227	oveq12d 7385	. . . . . . . 8 ⊢ (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
229	180	pm2.21d 121	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶))
230	229	impr 454	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)
231	156, 223, 170, 225, 228, 230	limcco 25860	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim_ℂ -𝐵))
232		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ℝ
233		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 D
234		nfmpt1 5184	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
235	232, 233, 234	nfov 7397	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))
236		nfcv 2898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑦
237	235, 236	nffv 6850	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦)
238		nfcv 2898	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 /
239		nfmpt1 5184	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
240	232, 233, 239	nfov 7397	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
241	240, 236	nffv 6850	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)
242	237, 238, 241	nfov 7397	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))
243		nfcv 2898	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
244		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥))
245		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
246	244, 245	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
247	242, 243, 246	cbvmpt 5187	. . . . . . . . 9 ⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
248	123	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥))
249	126	fvmpt2 6959	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
250	125, 249	mpan2 692	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
251	248, 250	sylan9eq 2791	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
252	150	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥))
253	153	fvmpt2 6959	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
254	152, 253	mpan2 692	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
255	252, 254	sylan9eq 2791	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
256	251, 255	oveq12d 7385	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)))
257	195	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺))
258	206	necon3bd 2946	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0))
259	257, 258	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)
260	118, 145, 259	div2negd 11946	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
261	256, 260	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
262	261	mpteq2dva 5178	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
263	247, 262	eqtrid 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
264	263	oveq1d 7382	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim_ℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim_ℂ -𝐵))
265	231, 264	eleqtrrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim_ℂ -𝐵))
266	76, 78, 81, 82, 83, 128, 155, 183, 190, 194, 212, 265	lhop1 25981	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim_ℂ -𝐵))
267		nffvmpt1 6851	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦)
268		nffvmpt1 6851	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)
269	267, 238, 268	nfov 7397	. . . . . . . 8 ⊢ Ⅎ𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))
270		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
271		fveq2 6840	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥))
272		fveq2 6840	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
273	271, 272	oveq12d 7385	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
274	269, 270, 273	cbvmpt 5187	. . . . . . 7 ⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
275		fvex 6853	. . . . . . . . . 10 ⊢ (𝐹‘-𝑥) ∈ V
276		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
277	276	fvmpt2 6959	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
278	26, 275, 277	sylancl 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
279		fvex 6853	. . . . . . . . . 10 ⊢ (𝐺‘-𝑥) ∈ V
280		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
281	280	fvmpt2 6959	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
282	26, 279, 281	sylancl 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
283	278, 282	oveq12d 7385	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥)))
284	283	mpteq2dva 5178	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
285	274, 284	eqtrid 2783	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
286	285	oveq1d 7382	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim_ℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim_ℂ -𝐵))
287	266, 286	eleqtrd 2838	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim_ℂ -𝐵))
288		negeq 11385	. . . . . 6 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
289	288	fveq2d 6844	. . . . 5 ⊢ (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧))
290	288	fveq2d 6844	. . . . 5 ⊢ (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧))
291	289, 290	oveq12d 7385	. . . 4 ⊢ (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧)))
292	76	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ)
293		eliooord 13358	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵))
294	293	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵))
295	294	simprd 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵)
296	15, 13	ltnegd 11728	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧))
297	295, 296	mpbid 232	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧)
298	292, 297	gtned 11281	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵)
299	298	neneqd 2937	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵)
300	299	pm2.21d 121	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶))
301	300	impr 454	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)
302	19, 62, 75, 287, 291, 301	limcco 25860	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim_ℂ 𝐵))
303	15	recnd 11173	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ)
304	303	negnegd 11496	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧)
305	304	fveq2d 6844	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹‘𝑧))
306	304	fveq2d 6844	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺‘𝑧))
307	305, 306	oveq12d 7385	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹‘𝑧) / (𝐺‘𝑧)))
308	307	mpteq2dva 5178	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))))
309	308	oveq1d 7382	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim_ℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
310	39	resmptd 6005	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))))
311	310	oveq1d 7382	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
312		fss 6684	. . . . . . . . 9 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
313	88, 51, 312	sylancl 587	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
314	313	ffvelcdmda 7036	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ)
315	53	ffvelcdmda 7036	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ)
316	48	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺)
317	50	ffnd 6669	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵))
318		fnfvelrn 7032	. . . . . . . . . . 11 ⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺)
319	317, 318	sylan 581	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺)
320		eleq1 2824	. . . . . . . . . 10 ⊢ ((𝐺‘𝑧) = 0 → ((𝐺‘𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
321	319, 320	syl5ibcom 245	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝑧) = 0 → 0 ∈ ran 𝐺))
322	321	necon3bd 2946	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘𝑧) ≠ 0))
323	316, 322	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ≠ 0)
324	314, 315, 323	divcld 11931	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ)
325	324	fmpttd 7067	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(𝐴(,)𝐵)⟶ℂ)
326		ioossre 13360	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ ℝ
327	326, 51	sstri 3931	. . . . . 6 ⊢ (𝐴(,)𝐵) ⊆ ℂ
328	327	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ)
329		eqid 2736	. . . . 5 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵}))
330		ssun2 4119	. . . . . . 7 ⊢ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})
331		snssg 4727	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
332	72, 331	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
333	330, 332	mpbiri 258	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}))
334	100	cnfldtopon 24747	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
335	326	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ)
336	72	snssd 4730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ ℝ)
337	335, 336	unssd 4132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ)
338	337, 51	sstrdi 3934	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ)
339		resttopon 23126	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
340	334, 338, 339	sylancr 588	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
341		topontop 22878	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
342	340, 341	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
343		indi 4224	. . . . . . . . . 10 ⊢ ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵}))
344		pnfxr 11199	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
345	344	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → +∞ ∈ ℝ^*)
346	4	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℝ^*)
347		iooin 13332	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℝ^* ∧ +∞ ∈ ℝ^) ∧ (𝐴 ∈ ℝ^ ∧ 𝐵 ∈ ℝ^*)) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
348	35, 345, 34, 346, 347	syl22anc 839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
349		xrltnle 11212	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑎 ∈ ℝ^*) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴))
350	34, 35, 349	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴))
351	36, 350	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 𝑎 ≤ 𝐴)
352	351	iffalsed 4477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎)
353	72	ltpnfd 13072	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 < +∞)
354		xrltnle 11212	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
355	346, 344, 354	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
356	353, 355	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵)
357	356	iffalsed 4477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵)
358	352, 357	oveq12d 7385	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵))
359	348, 358	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵))
360		elioopnf 13396	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℝ^* → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
361	35, 360	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
362	72, 79, 361	mpbir2and 714	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞))
363	362	snssd 4730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞))
364		sseqin2 4163	. . . . . . . . . . . 12 ⊢ ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
365	363, 364	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
366	359, 365	uneq12d 4109	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
367	343, 366	eqtrid 2783	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
368		retop 24726	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ Top
369		reex 11129	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
370	369	ssex 5262	. . . . . . . . . . 11 ⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
371	337, 370	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
372		iooretop 24730	. . . . . . . . . . 11 ⊢ (𝑎(,)+∞) ∈ (topGen‘ran (,))
373	372	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran (,)))
374		elrestr 17391	. . . . . . . . . 10 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
375	368, 371, 373, 374	mp3an2i 1469	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
376	367, 375	eqeltrrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
377		eqid 2736	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
378	100, 377	rerest 24769	. . . . . . . . 9 ⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
379	337, 378	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
380	376, 379	eleqtrrd 2839	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
381		isopn3i 23047	. . . . . . 7 ⊢ ((((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵}))) → ((int‘((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
382	342, 380, 381	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((int‘((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
383	333, 382	eleqtrrd 2839	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})))
384	325, 39, 328, 100, 329, 383	limcres 25853	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
385	309, 311, 384	3eqtr2d 2777	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
386	302, 385	eleqtrd 2838	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
387	9, 386	rexlimddv 3144	1 ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∃wrex 3061 Vcvv 3429 ∪ cun 3887 ∩ cin 3888 ⊆ wss 3889 ifcif 4466 {csn 4567 {cpr 4569 class class class wbr 5085 ↦ cmpt 5166 dom cdm 5631 ran crn 5632 ↾ cres 5633 Fn wfn 6493 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 · cmul 11043 +∞cpnf 11176 ℝ^*cxr 11178 < clt 11179 ≤ cle 11180 -cneg 11378 / cdiv 11807 ℚcq 12898 (,)cioo 13298 ↾_t crest 17383 TopOpenctopn 17384 topGenctg 17400 ℂ_fldccnfld 21352 Topctop 22858 TopOnctopon 22875 intcnt 22982 –cn→ccncf 24843 lim_ℂ climc 25829 D cdv 25830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-fi 9324 df-sup 9355 df-inf 9356 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-ioo 13302 df-ioc 13303 df-ico 13304 df-icc 13305 df-fz 13462 df-fzo 13609 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17466 df-qtop 17471 df-imas 17472 df-xps 17474 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-mulg 19044 df-cntz 19292 df-cmn 19757 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-fbas 21349 df-fg 21350 df-cnfld 21353 df-top 22859 df-topon 22876 df-topsp 22898 df-bases 22911 df-cld 22984 df-ntr 22985 df-cls 22986 df-nei 23063 df-lp 23101 df-perf 23102 df-cn 23192 df-cnp 23193 df-haus 23280 df-cmp 23352 df-tx 23527 df-hmeo 23720 df-fil 23811 df-fm 23903 df-flim 23904 df-flf 23905 df-xms 24285 df-ms 24286 df-tms 24287 df-cncf 24845 df-limc 25833 df-dv 25834

This theorem is referenced by: lhop 25983 fourierdlem60 46594

W3C validator