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 23582

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 11674	. . 3 ⊢ ℚ ⊆ ℝ
2		lhop2.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
3		lhop2.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 9968	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
5		lhop2.l	. . . 4 ⊢ (𝜑 → 𝐴 < 𝐵)
6		qbtwnxr 11905	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))
7	2, 4, 5, 6	syl3anc 1318	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))
8		ssrexv 3630	. . 3 ⊢ (ℚ ⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)))
9	1, 7, 8	mpsyl 66	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))
10		simpr 476	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵))
11		simprl 790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ)
12	11	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ)
13	3	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ)
14		elioore 12076	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ)
15	14	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ)
16		iooneg 12163	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
17	12, 13, 15, 16	syl3anc 1318	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
18	10, 17	mpbid 221	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
19	18	adantrr 749	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
20		lhop2.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
21	20	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
22		elioore 12076	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ)
23	22	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ)
24	23	recnd 9947	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ)
25	24	negnegd 10262	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥)
26		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎))
27	25, 26	eqeltrd 2688	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎))
28	11	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ)
29	3	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ)
30	23	renegcld 10336	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ)
31		iooneg 12163	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
32	28, 29, 30, 31	syl3anc 1318	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
33	27, 32	mpbird 246	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵))
34	2	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ∈ ℝ^*)
35		simprrl 800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 < 𝑎)
36	11	rexrd 9968	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ^*)
37		xrltle 11858	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑎 ∈ ℝ^*) → (𝐴 < 𝑎 → 𝐴 ≤ 𝑎))
38	34, 36, 37	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴 < 𝑎 → 𝐴 ≤ 𝑎))
39	35, 38	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ≤ 𝑎)
40		iooss1 12081	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ 𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
41	34, 39, 40	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
42	41	sselda 3568	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
43	33, 42	syldan 486	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵))
44	21, 43	ffvelrnd 6268	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ)
45	44	recnd 9947	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ)
46		lhop2.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ)
47	46	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
48	47, 43	ffvelrnd 6268	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ)
49	48	recnd 9947	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ)
50		lhop2.gn0	. . . . . . 7 ⊢ (𝜑 → ¬ 0 ∈ ran 𝐺)
51	50	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺)
52	46	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
53		ax-resscn 9872	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℂ
54		fss 5969	. . . . . . . . . . . 12 ⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
55	52, 53, 54	sylancl 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
56	55	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
57		ffn 5958	. . . . . . . . . 10 ⊢ (𝐺:(𝐴(,)𝐵)⟶ℂ → 𝐺 Fn (𝐴(,)𝐵))
58	56, 57	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵))
59		fnfvelrn 6264	. . . . . . . . 9 ⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺)
60	58, 43, 59	syl2anc 691	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺)
61		eleq1 2676	. . . . . . . 8 ⊢ ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
62	60, 61	syl5ibcom 234	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺))
63	62	necon3bd 2796	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0))
64	51, 63	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0)
65	45, 49, 64	divcld 10680	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ)
66		limcresi 23455	. . . . . 6 ⊢ ((𝑧 ∈ ℝ ↦ -𝑧) lim_ℂ 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵)
67		ioossre 12106	. . . . . . . 8 ⊢ (𝑎(,)𝐵) ⊆ ℝ
68		resmpt 5369	. . . . . . . 8 ⊢ ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧))
69	67, 68	ax-mp 5	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)
70	69	oveq1i 6559	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim_ℂ 𝐵)
71	66, 70	sseqtri 3600	. . . . 5 ⊢ ((𝑧 ∈ ℝ ↦ -𝑧) lim_ℂ 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim_ℂ 𝐵)
72		eqid 2610	. . . . . . . 8 ⊢ (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧)
73	72	negcncf 22529	. . . . . . 7 ⊢ (ℝ ⊆ ℂ → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
74	53, 73	mp1i 13	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
75	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℝ)
76		negeq 10152	. . . . . 6 ⊢ (𝑧 = 𝐵 → -𝑧 = -𝐵)
77	74, 75, 76	cnmptlimc 23460	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) lim_ℂ 𝐵))
78	71, 77	sseldi 3566	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim_ℂ 𝐵))
79	75	renegcld 10336	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ℝ)
80	11	renegcld 10336	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ)
81	80	rexrd 9968	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ^*)
82		simprrr 801	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 < 𝐵)
83	11, 75	ltnegd 10484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎))
84	82, 83	mpbid 221	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 < -𝑎)
85		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
86	44, 85	fmptd 6292	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
87		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
88	48, 87	fmptd 6292	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
89		reelprrecn 9907	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
90	89	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ℝ ∈ {ℝ, ℂ})
91		neg1cn 11001	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
92	91	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ)
93	20	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
94	93	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℝ)
95	94	recnd 9947	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℂ)
96		fvex 6113	. . . . . . . . . . 11 ⊢ ((ℝ D 𝐹)‘𝑦) ∈ V
97	96	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V)
98		1cnd 9935	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ)
99		simpr 476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
100	99	recnd 9947	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
101		1cnd 9935	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
102	90	dvmptid 23526	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
103		ioossre 12106	. . . . . . . . . . . . 13 ⊢ (-𝐵(,)-𝑎) ⊆ ℝ
104	103	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ)
105		eqid 2610	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
106	105	tgioo2 22414	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
107		iooretop 22379	. . . . . . . . . . . . 13 ⊢ (-𝐵(,)-𝑎) ∈ (topGen‘ran (,))
108	107	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran (,)))
109	90, 100, 101, 102, 104, 106, 105, 108	dvmptres 23532	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1))
110	90, 24, 98, 109	dvmptneg 23535	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1))
111	93	feqmptd 6159	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)))
112	111	oveq2d 6565	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))))
113		dvf 23477	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
114		lhop2.if	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
115	114	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
116	115	feq2d 5944	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
117	113, 116	mpbii 222	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
118	117	feqmptd 6159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
119	112, 118	eqtr3d 2646	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
120		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → (𝐹‘𝑦) = (𝐹‘-𝑥))
121		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥))
122	90, 90, 43, 92, 95, 97, 110, 119, 120, 121	dvmptco 23541	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)))
123	117	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
124	123, 43	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ)
125	124, 92	mulcomd 9940	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐹)‘-𝑥)))
126	124	mulm1d 10361	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥))
127	125, 126	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥))
128	127	mpteq2dva 4672	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
129	122, 128	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
130	129	dmeqd 5248	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
131		negex 10158	. . . . . . . 8 ⊢ -((ℝ D 𝐹)‘-𝑥) ∈ V
132		eqid 2610	. . . . . . . 8 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))
133	131, 132	dmmpti 5936	. . . . . . 7 ⊢ dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎)
134	130, 133	syl6eq 2660	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎))
135	52	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℝ)
136	135	recnd 9947	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℂ)
137		fvex 6113	. . . . . . . . . . 11 ⊢ ((ℝ D 𝐺)‘𝑦) ∈ V
138	137	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V)
139	52	feqmptd 6159	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)))
140	139	oveq2d 6565	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))))
141		dvf 23477	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
142		lhop2.ig	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
143	142	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
144	143	feq2d 5944	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
145	141, 144	mpbii 222	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
146	145	feqmptd 6159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
147	140, 146	eqtr3d 2646	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
148		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → (𝐺‘𝑦) = (𝐺‘-𝑥))
149		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥))
150	90, 90, 43, 92, 136, 138, 110, 147, 148, 149	dvmptco 23541	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)))
151	145	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
152	151, 43	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ)
153	152, 92	mulcomd 9940	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐺)‘-𝑥)))
154	152	mulm1d 10361	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥))
155	153, 154	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥))
156	155	mpteq2dva 4672	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
157	150, 156	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
158	157	dmeqd 5248	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
159		negex 10158	. . . . . . . 8 ⊢ -((ℝ D 𝐺)‘-𝑥) ∈ V
160		eqid 2610	. . . . . . . 8 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))
161	159, 160	dmmpti 5936	. . . . . . 7 ⊢ dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎)
162	158, 161	syl6eq 2660	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎))
163	43	adantrr 749	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 ≠ 𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
164		limcresi 23455	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim_ℂ -𝐵)
165		resmpt 5369	. . . . . . . . . . 11 ⊢ ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥))
166	103, 165	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)
167	166	oveq1i 6559	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim_ℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim_ℂ -𝐵)
168	164, 167	sseqtri 3600	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim_ℂ -𝐵)
169	75	recnd 9947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℂ)
170	169	negnegd 10262	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 = 𝐵)
171		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥)
172	171	negcncf 22529	. . . . . . . . . . 11 ⊢ (ℝ ⊆ ℂ → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
173	53, 172	mp1i 13	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
174		negeq 10152	. . . . . . . . . 10 ⊢ (𝑥 = -𝐵 → -𝑥 = --𝐵)
175	173, 79, 174	cnmptlimc 23460	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵))
176	170, 175	eqeltrrd 2689	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim_ℂ -𝐵))
177	168, 176	sseldi 3566	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim_ℂ -𝐵))
178		lhop2.f0	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐵))
179	178	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐹 lim_ℂ 𝐵))
180	111	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐹 lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) lim_ℂ 𝐵))
181	179, 180	eleqtrd 2690	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) lim_ℂ 𝐵))
182		eliooord 12104	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎))
183	182	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎))
184	183	simpld 474	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥)
185	29, 23, 184	ltnegcon1d 10486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵)
186	30, 185	ltned 10052	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ≠ 𝐵)
187	186	neneqd 2787	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵)
188	187	pm2.21d 117	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0))
189	188	impr 647	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0)
190	163, 95, 177, 181, 120, 189	limcco 23463	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) lim_ℂ -𝐵))
191		lhop2.g0	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (𝐺 lim_ℂ 𝐵))
192	191	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐺 lim_ℂ 𝐵))
193	139	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐺 lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) lim_ℂ 𝐵))
194	192, 193	eleqtrd 2690	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) lim_ℂ 𝐵))
195	187	pm2.21d 117	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0))
196	195	impr 647	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0)
197	163, 136, 177, 194, 148, 196	limcco 23463	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) lim_ℂ -𝐵))
198	60, 87	fmptd 6292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺)
199		frn 5966	. . . . . . . 8 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺 → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
200	198, 199	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
201	50	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺)
202	200, 201	ssneldd 3571	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
203		lhop2.gd0	. . . . . . . 8 ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
204	203	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D 𝐺))
205	157	rneqd 5274	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
206	205	eleq2d 2673	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))))
207	160, 159	elrnmpti 5297	. . . . . . . . 9 ⊢ (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥))
208		eqcom 2617	. . . . . . . . . . 11 ⊢ (0 = -((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0)
209	152	negeq0d 10263	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0))
210		ffn 5958	. . . . . . . . . . . . . . 15 ⊢ ((ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
211	151, 210	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
212		fnfvelrn 6264	. . . . . . . . . . . . . 14 ⊢ (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
213	211, 43, 212	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
214		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
215	213, 214	syl5ibcom 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
216	209, 215	sylbird 249	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
217	208, 216	syl5bi 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
218	217	rexlimdva 3013	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
219	207, 218	syl5bi 231	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺)))
220	206, 219	sylbid 229	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺)))
221	204, 220	mtod 188	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))))
222	117	ffvelrnda 6267	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ)
223	145	ffvelrnda 6267	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ)
224	203	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D 𝐺))
225	145, 210	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
226		fnfvelrn 6264	. . . . . . . . . . . . 13 ⊢ (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
227	225, 226	sylan 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
228		eleq1 2676	. . . . . . . . . . . 12 ⊢ (((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
229	227, 228	syl5ibcom 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺)))
230	229	necon3bd 2796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0))
231	224, 230	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0)
232	222, 223, 231	divcld 10680	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ)
233		lhop2.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim_ℂ 𝐵))
234	233	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim_ℂ 𝐵))
235		fveq2 6103	. . . . . . . . 9 ⊢ (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥))
236		fveq2 6103	. . . . . . . . 9 ⊢ (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥))
237	235, 236	oveq12d 6567	. . . . . . . 8 ⊢ (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
238	187	pm2.21d 117	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶))
239	238	impr 647	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)
240	163, 232, 177, 234, 237, 239	limcco 23463	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim_ℂ -𝐵))
241		nfcv 2751	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ℝ
242		nfcv 2751	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 D
243		nfmpt1 4675	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
244	241, 242, 243	nfov 6575	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))
245		nfcv 2751	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑦
246	244, 245	nffv 6110	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦)
247		nfcv 2751	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 /
248		nfmpt1 4675	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
249	241, 242, 248	nfov 6575	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
250	249, 245	nffv 6110	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)
251	246, 247, 250	nfov 6575	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))
252		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
253		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥))
254		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
255	253, 254	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
256	251, 252, 255	cbvmpt 4677	. . . . . . . . 9 ⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
257	129	fveq1d 6105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥))
258	132	fvmpt2 6200	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
259	131, 258	mpan2 703	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
260	257, 259	sylan9eq 2664	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
261	157	fveq1d 6105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥))
262	160	fvmpt2 6200	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
263	159, 262	mpan2 703	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
264	261, 263	sylan9eq 2664	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
265	260, 264	oveq12d 6567	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)))
266	203	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺))
267	215	necon3bd 2796	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0))
268	266, 267	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)
269	124, 152, 268	div2negd 10695	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
270	265, 269	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
271	270	mpteq2dva 4672	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
272	256, 271	syl5eq 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
273	272	oveq1d 6564	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim_ℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim_ℂ -𝐵))
274	240, 273	eleqtrrd 2691	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim_ℂ -𝐵))
275	79, 81, 84, 86, 88, 134, 162, 190, 197, 202, 221, 274	lhop1 23581	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim_ℂ -𝐵))
276		nffvmpt1 6111	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦)
277		nffvmpt1 6111	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)
278	276, 247, 277	nfov 6575	. . . . . . . 8 ⊢ Ⅎ𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))
279		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
280		fveq2 6103	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥))
281		fveq2 6103	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
282	280, 281	oveq12d 6567	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
283	278, 279, 282	cbvmpt 4677	. . . . . . 7 ⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
284		fvex 6113	. . . . . . . . . 10 ⊢ (𝐹‘-𝑥) ∈ V
285	85	fvmpt2 6200	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
286	26, 284, 285	sylancl 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
287		fvex 6113	. . . . . . . . . 10 ⊢ (𝐺‘-𝑥) ∈ V
288	87	fvmpt2 6200	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
289	26, 287, 288	sylancl 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
290	286, 289	oveq12d 6567	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥)))
291	290	mpteq2dva 4672	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
292	283, 291	syl5eq 2656	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
293	292	oveq1d 6564	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim_ℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim_ℂ -𝐵))
294	275, 293	eleqtrd 2690	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim_ℂ -𝐵))
295		negeq 10152	. . . . . 6 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
296	295	fveq2d 6107	. . . . 5 ⊢ (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧))
297	295	fveq2d 6107	. . . . 5 ⊢ (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧))
298	296, 297	oveq12d 6567	. . . 4 ⊢ (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧)))
299	79	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ)
300		eliooord 12104	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵))
301	300	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵))
302	301	simprd 478	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵)
303	15, 13	ltnegd 10484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧))
304	302, 303	mpbid 221	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧)
305	299, 304	gtned 10051	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵)
306	305	neneqd 2787	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵)
307	306	pm2.21d 117	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶))
308	307	impr 647	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)
309	19, 65, 78, 294, 298, 308	limcco 23463	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim_ℂ 𝐵))
310	15	recnd 9947	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ)
311	310	negnegd 10262	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧)
312	311	fveq2d 6107	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹‘𝑧))
313	311	fveq2d 6107	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺‘𝑧))
314	312, 313	oveq12d 6567	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹‘𝑧) / (𝐺‘𝑧)))
315	314	mpteq2dva 4672	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))))
316	315	oveq1d 6564	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim_ℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
317	41	resmptd 5371	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))))
318	317	oveq1d 6564	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
319		fss 5969	. . . . . . . . 9 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
320	93, 53, 319	sylancl 693	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
321	320	ffvelrnda 6267	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ)
322	55	ffvelrnda 6267	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ)
323	50	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺)
324	55, 57	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵))
325		fnfvelrn 6264	. . . . . . . . . . 11 ⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺)
326	324, 325	sylan 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺)
327		eleq1 2676	. . . . . . . . . 10 ⊢ ((𝐺‘𝑧) = 0 → ((𝐺‘𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
328	326, 327	syl5ibcom 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝑧) = 0 → 0 ∈ ran 𝐺))
329	328	necon3bd 2796	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘𝑧) ≠ 0))
330	323, 329	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ≠ 0)
331	321, 322, 330	divcld 10680	. . . . . 6 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ)
332		eqid 2610	. . . . . 6 ⊢ (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))
333	331, 332	fmptd 6292	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(𝐴(,)𝐵)⟶ℂ)
334		ioossre 12106	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ ℝ
335	334, 53	sstri 3577	. . . . . 6 ⊢ (𝐴(,)𝐵) ⊆ ℂ
336	335	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ)
337		eqid 2610	. . . . 5 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵}))
338		ssun2 3739	. . . . . . 7 ⊢ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})
339		snssg 4268	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
340	75, 339	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
341	338, 340	mpbiri 247	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}))
342	105	cnfldtopon 22396	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
343	334	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ)
344	75	snssd 4281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ ℝ)
345	343, 344	unssd 3751	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ)
346	345, 53	syl6ss 3580	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ)
347		resttopon 20775	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
348	342, 346, 347	sylancr 694	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
349		topontop 20541	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
350	348, 349	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
351		indi 3832	. . . . . . . . . 10 ⊢ ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵}))
352		pnfxr 9971	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
353	352	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → +∞ ∈ ℝ^*)
354	4	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℝ^*)
355		iooin 12080	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℝ^* ∧ +∞ ∈ ℝ^) ∧ (𝐴 ∈ ℝ^ ∧ 𝐵 ∈ ℝ^*)) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
356	36, 353, 34, 354, 355	syl22anc 1319	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
357		xrltnle 9984	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑎 ∈ ℝ^*) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴))
358	34, 36, 357	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴))
359	35, 358	mpbid 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 𝑎 ≤ 𝐴)
360	359	iffalsed 4047	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎)
361		ltpnf 11830	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
362	75, 361	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 < +∞)
363		xrltnle 9984	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
364	354, 352, 363	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
365	362, 364	mpbid 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵)
366	365	iffalsed 4047	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵)
367	360, 366	oveq12d 6567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵))
368	356, 367	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵))
369		elioopnf 12138	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℝ^* → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
370	36, 369	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
371	75, 82, 370	mpbir2and 959	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞))
372	371	snssd 4281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞))
373		sseqin2 3779	. . . . . . . . . . . 12 ⊢ ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
374	372, 373	sylib 207	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
375	368, 374	uneq12d 3730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
376	351, 375	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
377		retop 22375	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) ∈ Top
378	377	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (topGen‘ran (,)) ∈ Top)
379		reex 9906	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
380	379	ssex 4730	. . . . . . . . . . 11 ⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
381	345, 380	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
382		iooretop 22379	. . . . . . . . . . 11 ⊢ (𝑎(,)+∞) ∈ (topGen‘ran (,))
383	382	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran (,)))
384		elrestr 15912	. . . . . . . . . 10 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
385	378, 381, 383, 384	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
386	376, 385	eqeltrrd 2689	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
387		eqid 2610	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
388	105, 387	rerest 22415	. . . . . . . . 9 ⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
389	345, 388	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
390	386, 389	eleqtrrd 2691	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))
391		isopn3i 20696	. . . . . . 7 ⊢ ((((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵}))) → ((int‘((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
392	350, 390, 391	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((int‘((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
393	341, 392	eleqtrrd 2691	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})))
394	333, 41, 336, 105, 337, 393	limcres 23456	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
395	316, 318, 394	3eqtr2d 2650	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
396	309, 395	eleqtrd 2690	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))
397	9, 396	rexlimddv 3017	1 ⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∃wrex 2897 Vcvv 3173 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ifcif 4036 {csn 4125 {cpr 4127 class class class wbr 4583 ↦ cmpt 4643 dom cdm 5038 ran crn 5039 ↾ cres 5040 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 · cmul 9820 +∞cpnf 9950 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 -cneg 10146 / cdiv 10563 ℚcq 11664 (,)cioo 12046 ↾_t crest 15904 TopOpenctopn 15905 topGenctg 15921 ℂ_fldccnfld 19567 Topctop 20517 TopOnctopon 20518 intcnt 20631 –cn→ccncf 22487 lim_ℂ climc 23432 D cdv 23433

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ioc 12051 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-rest 15906 df-topn 15907 df-0g 15925 df-gsum 15926 df-topgen 15927 df-pt 15928 df-prds 15931 df-xrs 15985 df-qtop 15990 df-imas 15991 df-xps 15993 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-mulg 17364 df-cntz 17573 df-cmn 18018 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-fbas 19564 df-fg 19565 df-cnfld 19568 df-top 20521 df-bases 20522 df-topon 20523 df-topsp 20524 df-cld 20633 df-ntr 20634 df-cls 20635 df-nei 20712 df-lp 20750 df-perf 20751 df-cn 20841 df-cnp 20842 df-haus 20929 df-cmp 21000 df-tx 21175 df-hmeo 21368 df-fil 21460 df-fm 21552 df-flim 21553 df-flf 21554 df-xms 21935 df-ms 21936 df-tms 21937 df-cncf 22489 df-limc 23436 df-dv 23437

This theorem is referenced by: lhop 23583 fourierdlem60 39059

W3C validator