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

Theorem lhop 23998
Description: L'Hôpital's Rule. If 𝐼 is an open set of the reals, 𝐹 and 𝐺 are real functions on 𝐴 containing all of 𝐼 except possibly 𝐵, which are differentiable everywhere on 𝐼 ∖ {𝐵}, 𝐹 and 𝐺 both approach 0, and the limit of 𝐹' (𝑥) / 𝐺' (𝑥) at 𝐵 is 𝐶, then the limit 𝐹(𝑥) / 𝐺(𝑥) at 𝐵 also exists and equals 𝐶. This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016.)
Hypotheses
Ref Expression
lhop.a (𝜑𝐴 ⊆ ℝ)
lhop.f (𝜑𝐹:𝐴⟶ℝ)
lhop.g (𝜑𝐺:𝐴⟶ℝ)
lhop.i (𝜑𝐼 ∈ (topGen‘ran (,)))
lhop.b (𝜑𝐵𝐼)
lhop.d 𝐷 = (𝐼 ∖ {𝐵})
lhop.if (𝜑𝐷 ⊆ dom (ℝ D 𝐹))
lhop.ig (𝜑𝐷 ⊆ dom (ℝ D 𝐺))
lhop.f0 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
lhop.g0 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
lhop.gn0 (𝜑 → ¬ 0 ∈ (𝐺𝐷))
lhop.gd0 (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
lhop.c (𝜑𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
Assertion
Ref Expression
lhop (𝜑𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Distinct variable groups:   𝑧,𝐵   𝑧,𝐶   𝑧,𝐷   𝑧,𝐹   𝜑,𝑧   𝑧,𝐺   𝑧,𝐼
Allowed substitution hint:   𝐴(𝑧)

Proof of Theorem lhop
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 eqid 2771 . . . . 5 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
21rexmet 22813 . . . 4 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32a1i 11 . . 3 (𝜑 → ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ))
4 lhop.i . . 3 (𝜑𝐼 ∈ (topGen‘ran (,)))
5 lhop.b . . 3 (𝜑𝐵𝐼)
6 eqid 2771 . . . . 5 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
71, 6tgioo 22818 . . . 4 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
87mopni2 22517 . . 3 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐼 ∈ (topGen‘ran (,)) ∧ 𝐵𝐼) → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼)
93, 4, 5, 8syl3anc 1476 . 2 (𝜑 → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼)
10 elssuni 4604 . . . . . . . . 9 (𝐼 ∈ (topGen‘ran (,)) → 𝐼 (topGen‘ran (,)))
11 uniretop 22785 . . . . . . . . 9 ℝ = (topGen‘ran (,))
1210, 11syl6sseqr 3801 . . . . . . . 8 (𝐼 ∈ (topGen‘ran (,)) → 𝐼 ⊆ ℝ)
134, 12syl 17 . . . . . . 7 (𝜑𝐼 ⊆ ℝ)
1413, 5sseldd 3753 . . . . . 6 (𝜑𝐵 ∈ ℝ)
15 rpre 12041 . . . . . 6 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
161bl2ioo 22814 . . . . . 6 ((𝐵 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
1714, 15, 16syl2an 583 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
1817sseq1d 3781 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼 ↔ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼))
1914adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ)
20 simprl 754 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ+)
2120rpred 12074 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ)
2219, 21resubcld 10663 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) ∈ ℝ)
2322rexrd 10294 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) ∈ ℝ*)
2419, 20ltsubrpd 12106 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) < 𝐵)
25 lhop.f . . . . . . . . . . 11 (𝜑𝐹:𝐴⟶ℝ)
2625adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℝ)
27 ssun1 3927 . . . . . . . . . . . 12 ((𝐵𝑟)(,)𝐵) ⊆ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
28 unass 3921 . . . . . . . . . . . . . . 15 (({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
29 uncom 3908 . . . . . . . . . . . . . . . 16 ({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) = (((𝐵𝑟)(,)𝐵) ∪ {𝐵})
3029uneq1i 3914 . . . . . . . . . . . . . . 15 (({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟)))
3128, 30eqtr3i 2795 . . . . . . . . . . . . . 14 ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟)))
3219rexrd 10294 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ*)
3319, 21readdcld 10274 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ)
3433rexrd 10294 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ*)
3519, 20ltaddrpd 12107 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 < (𝐵 + 𝑟))
36 ioojoin 12509 . . . . . . . . . . . . . . 15 ((((𝐵𝑟) ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) ∧ ((𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))) → ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
3723, 32, 34, 24, 35, 36syl32anc 1484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
3831, 37syl5eq 2817 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
39 elioo2 12420 . . . . . . . . . . . . . . . . 17 (((𝐵𝑟) ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) → (𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))))
4023, 34, 39syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))))
4119, 24, 35, 40mpbir3and 1427 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)))
4241snssd 4476 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)))
43 incom 3956 . . . . . . . . . . . . . . 15 ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵})
44 ubioo 12411 . . . . . . . . . . . . . . . . . 18 ¬ 𝐵 ∈ ((𝐵𝑟)(,)𝐵)
45 lbioo 12410 . . . . . . . . . . . . . . . . . 18 ¬ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))
4644, 45pm3.2ni 867 . . . . . . . . . . . . . . . . 17 ¬ (𝐵 ∈ ((𝐵𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟)))
47 elun 3904 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ↔ (𝐵 ∈ ((𝐵𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))))
4846, 47mtbir 312 . . . . . . . . . . . . . . . 16 ¬ 𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
49 disjsn 4384 . . . . . . . . . . . . . . . 16 (((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
5048, 49mpbir 221 . . . . . . . . . . . . . . 15 ((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅
5143, 50eqtri 2793 . . . . . . . . . . . . . 14 ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅
52 uneqdifeq 4200 . . . . . . . . . . . . . 14 (({𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∧ ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅) → (({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))))
5342, 51, 52sylancl 574 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))))
5438, 53mpbid 222 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
5527, 54syl5sseqr 3803 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}))
56 ssdif 3896 . . . . . . . . . . . . . 14 (((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼 → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵}))
5756ad2antll 708 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵}))
58 lhop.d . . . . . . . . . . . . 13 𝐷 = (𝐼 ∖ {𝐵})
5957, 58syl6sseqr 3801 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐷)
60 lhop.if . . . . . . . . . . . . . 14 (𝜑𝐷 ⊆ dom (ℝ D 𝐹))
61 ax-resscn 10198 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ⊆ ℂ)
63 fss 6197 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
6425, 61, 63sylancl 574 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐴⟶ℂ)
65 lhop.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ ℝ)
6662, 64, 65dvbss 23884 . . . . . . . . . . . . . 14 (𝜑 → dom (ℝ D 𝐹) ⊆ 𝐴)
6760, 66sstrd 3762 . . . . . . . . . . . . 13 (𝜑𝐷𝐴)
6867adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷𝐴)
6959, 68sstrd 3762 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐴)
7055, 69sstrd 3762 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ 𝐴)
7126, 70fssresd 6212 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ ((𝐵𝑟)(,)𝐵)):((𝐵𝑟)(,)𝐵)⟶ℝ)
72 lhop.g . . . . . . . . . . 11 (𝜑𝐺:𝐴⟶ℝ)
7372adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℝ)
7473, 70fssresd 6212 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ ((𝐵𝑟)(,)𝐵)):((𝐵𝑟)(,)𝐵)⟶ℝ)
7561a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ℝ ⊆ ℂ)
7664adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℂ)
7765adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐴 ⊆ ℝ)
78 ioossre 12439 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)𝐵) ⊆ ℝ
7978a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ ℝ)
80 eqid 2771 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8180tgioo2 22825 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
8280, 81dvres 23894 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
8375, 76, 77, 79, 82syl22anc 1477 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
84 retop 22784 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
85 iooretop 22788 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)𝐵) ∈ (topGen‘ran (,))
86 isopn3i 21106 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ ((𝐵𝑟)(,)𝐵) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
8784, 85, 86mp2an 672 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵)
8887reseq2i 5530 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))
8983, 88syl6eq 2821 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)))
9089dmeqd 5463 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)))
9155, 59sstrd 3762 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ 𝐷)
9260adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐹))
9391, 92sstrd 3762 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹))
94 ssdmres 5560 . . . . . . . . . . 11 (((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
9593, 94sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
9690, 95eqtrd 2805 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((𝐵𝑟)(,)𝐵))
97 fss 6197 . . . . . . . . . . . . . . 15 ((𝐺:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:𝐴⟶ℂ)
9872, 61, 97sylancl 574 . . . . . . . . . . . . . 14 (𝜑𝐺:𝐴⟶ℂ)
9998adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℂ)
10080, 81dvres 23894 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
10175, 99, 77, 79, 100syl22anc 1477 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
10287reseq2i 5530 . . . . . . . . . . . 12 ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))
103101, 102syl6eq 2821 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
104103dmeqd 5463 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
105 lhop.ig . . . . . . . . . . . . 13 (𝜑𝐷 ⊆ dom (ℝ D 𝐺))
106105adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐺))
10791, 106sstrd 3762 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺))
108 ssdmres 5560 . . . . . . . . . . 11 (((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
109107, 108sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
110104, 109eqtrd 2805 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((𝐵𝑟)(,)𝐵))
111 limcresi 23868 . . . . . . . . . 10 (𝐹 lim 𝐵) ⊆ ((𝐹 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
112 lhop.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
113112adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐹 lim 𝐵))
114111, 113sseldi 3750 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
115 limcresi 23868 . . . . . . . . . 10 (𝐺 lim 𝐵) ⊆ ((𝐺 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
116 lhop.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
117116adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐺 lim 𝐵))
118115, 117sseldi 3750 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
119 df-ima 5263 . . . . . . . . . . 11 (𝐺 “ ((𝐵𝑟)(,)𝐵)) = ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵))
120 imass2 5641 . . . . . . . . . . . 12 (((𝐵𝑟)(,)𝐵) ⊆ 𝐷 → (𝐺 “ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
12191, 120syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
122119, 121syl5eqssr 3799 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
123 lhop.gn0 . . . . . . . . . . 11 (𝜑 → ¬ 0 ∈ (𝐺𝐷))
124123adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ (𝐺𝐷))
125122, 124ssneldd 3755 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))
126103rneqd 5490 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ran ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
127 df-ima 5263 . . . . . . . . . . . 12 ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) = ran ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))
128126, 127syl6eqr 2823 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)))
129 imass2 5641 . . . . . . . . . . . 12 (((𝐵𝑟)(,)𝐵) ⊆ 𝐷 → ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷))
13091, 129syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷))
131128, 130eqsstrd 3788 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) ⊆ ((ℝ D 𝐺) “ 𝐷))
132 lhop.gd0 . . . . . . . . . . 11 (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
133132adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
134131, 133ssneldd 3755 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))))
135 limcresi 23868 . . . . . . . . . . 11 ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
13691resmptd 5592 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
13789fveq1d 6335 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))
138 fvres 6350 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
139137, 138sylan9eq 2825 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
140103fveq1d 6335 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))
141 fvres 6350 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
142140, 141sylan9eq 2825 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
143139, 142oveq12d 6813 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
144143mpteq2dva 4879 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
145136, 144eqtr4d 2808 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))))
146145oveq1d 6810 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) = ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
147135, 146syl5sseq 3802 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
148 lhop.c . . . . . . . . . . 11 (𝜑𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
149148adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
150147, 149sseldd 3753 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
15123, 19, 24, 71, 74, 96, 110, 114, 118, 125, 134, 150lhop2 23997 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) lim 𝐵))
15255resmptd 5592 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
153 fvres 6350 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → ((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = (𝐹𝑧))
154 fvres 6350 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = (𝐺𝑧))
155153, 154oveq12d 6813 . . . . . . . . . . 11 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
156155mpteq2ia 4875 . . . . . . . . . 10 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))
157152, 156syl6eqr 2823 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))))
158157oveq1d 6810 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) = ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) lim 𝐵))
159151, 158eleqtrrd 2853 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
160 ssun2 3928 . . . . . . . . . . . 12 (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
161160, 54syl5sseqr 3803 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}))
162161, 69sstrd 3762 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐴)
16326, 162fssresd 6212 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ)
16473, 162fssresd 6212 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ)
165 ioossre 12439 . . . . . . . . . . . . . 14 (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ
166165a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)
16780, 81dvres 23894 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
16875, 76, 77, 166, 167syl22anc 1477 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
169 iooretop 22788 . . . . . . . . . . . . . 14 (𝐵(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))
170 isopn3i 21106 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (𝐵(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
17184, 169, 170mp2an 672 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))
172171reseq2i 5530 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))
173168, 172syl6eq 2821 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))))
174173dmeqd 5463 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))))
175161, 59sstrd 3762 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷)
176175, 92sstrd 3762 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹))
177 ssdmres 5560 . . . . . . . . . . 11 ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
178176, 177sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
179174, 178eqtrd 2805 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟)))
18080, 81dvres 23894 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
18175, 99, 77, 166, 180syl22anc 1477 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
182171reseq2i 5530 . . . . . . . . . . . 12 ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))
183181, 182syl6eq 2821 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
184183dmeqd 5463 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
185175, 106sstrd 3762 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺))
186 ssdmres 5560 . . . . . . . . . . 11 ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
187185, 186sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
188184, 187eqtrd 2805 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟)))
189 limcresi 23868 . . . . . . . . . 10 (𝐹 lim 𝐵) ⊆ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
190189, 113sseldi 3750 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
191 limcresi 23868 . . . . . . . . . 10 (𝐺 lim 𝐵) ⊆ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
192191, 117sseldi 3750 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
193 df-ima 5263 . . . . . . . . . . 11 (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) = ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))
194 imass2 5641 . . . . . . . . . . . 12 ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
195175, 194syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
196193, 195syl5eqssr 3799 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
197196, 124ssneldd 3755 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))
198183rneqd 5490 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
199 df-ima 5263 . . . . . . . . . . . 12 ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))
200198, 199syl6eqr 2823 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))))
201 imass2 5641 . . . . . . . . . . . 12 ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷))
202175, 201syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷))
203200, 202eqsstrd 3788 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) ⊆ ((ℝ D 𝐺) “ 𝐷))
204203, 133ssneldd 3755 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))))
205 limcresi 23868 . . . . . . . . . . 11 ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
206175resmptd 5592 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
207173fveq1d 6335 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))
208 fvres 6350 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
209207, 208sylan9eq 2825 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
210183fveq1d 6335 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))
211 fvres 6350 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
212210, 211sylan9eq 2825 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
213209, 212oveq12d 6813 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
214213mpteq2dva 4879 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
215206, 214eqtr4d 2808 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))))
216215oveq1d 6810 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
217205, 216syl5sseq 3802 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
218217, 149sseldd 3753 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
21919, 34, 35, 163, 164, 179, 188, 190, 192, 197, 204, 218lhop1 23996 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) lim 𝐵))
220161resmptd 5592 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹𝑧) / (𝐺𝑧))))
221 fvres 6350 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐹𝑧))
222 fvres 6350 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐺𝑧))
223221, 222oveq12d 6813 . . . . . . . . . . 11 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
224223mpteq2ia 4875 . . . . . . . . . 10 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹𝑧) / (𝐺𝑧)))
225220, 224syl6eqr 2823 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))))
226225oveq1d 6810 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) lim 𝐵))
227219, 226eleqtrrd 2853 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
228159, 227elind 3949 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)))
22959resmptd 5592 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) = (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))))
230229oveq1d 6810 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) lim 𝐵) = ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
23167sselda 3752 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷) → 𝑧𝐴)
23225ffvelrnda 6504 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℝ)
233231, 232syldan 579 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (𝐹𝑧) ∈ ℝ)
234233recnd 10273 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐹𝑧) ∈ ℂ)
23572ffvelrnda 6504 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (𝐺𝑧) ∈ ℝ)
236231, 235syldan 579 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ ℝ)
237236recnd 10273 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ ℂ)
238123adantr 466 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → ¬ 0 ∈ (𝐺𝐷))
23972ffnd 6185 . . . . . . . . . . . . . . . 16 (𝜑𝐺 Fn 𝐴)
240239adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝐺 Fn 𝐴)
24167adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝐷𝐴)
242 simpr 471 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝑧𝐷)
243 fnfvima 6641 . . . . . . . . . . . . . . 15 ((𝐺 Fn 𝐴𝐷𝐴𝑧𝐷) → (𝐺𝑧) ∈ (𝐺𝐷))
244240, 241, 242, 243syl3anc 1476 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ (𝐺𝐷))
245 eleq1 2838 . . . . . . . . . . . . . 14 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ (𝐺𝐷) ↔ 0 ∈ (𝐺𝐷)))
246244, 245syl5ibcom 235 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷) → ((𝐺𝑧) = 0 → 0 ∈ (𝐺𝐷)))
247246necon3bd 2957 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (¬ 0 ∈ (𝐺𝐷) → (𝐺𝑧) ≠ 0))
248238, 247mpd 15 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐺𝑧) ≠ 0)
249234, 237, 248divcld 11006 . . . . . . . . . 10 ((𝜑𝑧𝐷) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
250249adantlr 694 . . . . . . . . 9 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧𝐷) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
251 eqid 2771 . . . . . . . . 9 (𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) = (𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧)))
252250, 251fmptd 6529 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))):𝐷⟶ℂ)
253 difss 3888 . . . . . . . . . . 11 (𝐼 ∖ {𝐵}) ⊆ 𝐼
25458, 253eqsstri 3784 . . . . . . . . . 10 𝐷𝐼
25513, 61syl6ss 3764 . . . . . . . . . 10 (𝜑𝐼 ⊆ ℂ)
256254, 255syl5ss 3763 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
257256adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ ℂ)
258 eqid 2771 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))
25958uneq1i 3914 . . . . . . . . . . . . . . . . 17 (𝐷 ∪ {𝐵}) = ((𝐼 ∖ {𝐵}) ∪ {𝐵})
260 undif1 4186 . . . . . . . . . . . . . . . . 17 ((𝐼 ∖ {𝐵}) ∪ {𝐵}) = (𝐼 ∪ {𝐵})
261259, 260eqtri 2793 . . . . . . . . . . . . . . . 16 (𝐷 ∪ {𝐵}) = (𝐼 ∪ {𝐵})
262 simprr 756 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)
26342, 262sstrd 3762 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ 𝐼)
264 ssequn2 3937 . . . . . . . . . . . . . . . . 17 ({𝐵} ⊆ 𝐼 ↔ (𝐼 ∪ {𝐵}) = 𝐼)
265263, 264sylib 208 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐼 ∪ {𝐵}) = 𝐼)
266261, 265syl5eq 2817 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐷 ∪ {𝐵}) = 𝐼)
267266oveq2d 6811 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t 𝐼))
26813adantr 466 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℝ)
269 eqid 2771 . . . . . . . . . . . . . . . 16 (topGen‘ran (,)) = (topGen‘ran (,))
27080, 269rerest 22826 . . . . . . . . . . . . . . 15 (𝐼 ⊆ ℝ → ((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,)) ↾t 𝐼))
271268, 270syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,)) ↾t 𝐼))
272267, 271eqtrd 2805 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((topGen‘ran (,)) ↾t 𝐼))
273272fveq2d 6337 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))) = (int‘((topGen‘ran (,)) ↾t 𝐼)))
274273fveq1d 6335 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
27580cnfldtopon 22805 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
276255adantr 466 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℂ)
277 resttopon 21185 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝐼 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼))
278275, 276, 277sylancr 575 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼))
279 topontop 20937 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top)
280278, 279syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top)
281271, 280eqeltrrd 2851 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((topGen‘ran (,)) ↾t 𝐼) ∈ Top)
282 iooretop 22788 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))
283282a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)))
2844adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ∈ (topGen‘ran (,)))
285 restopn2 21201 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ 𝐼 ∈ (topGen‘ran (,))) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)))
28684, 284, 285sylancr 575 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)))
287283, 262, 286mpbir2and 692 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼))
288 isopn3i 21106 . . . . . . . . . . . 12 ((((topGen‘ran (,)) ↾t 𝐼) ∈ Top ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼)) → ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
289281, 287, 288syl2anc 573 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
290274, 289eqtrd 2805 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
29141, 290eleqtrrd 2853 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
292 undif1 4186 . . . . . . . . . . 11 ((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵})
293 ssequn2 3937 . . . . . . . . . . . 12 ({𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
29442, 293sylib 208 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
295292, 294syl5eq 2817 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
296295fveq2d 6337 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})) = ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
297291, 296eleqtrrd 2853 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})))
298252, 59, 257, 80, 258, 297limcres 23869 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) lim 𝐵) = ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
29978, 61sstri 3761 . . . . . . . . 9 ((𝐵𝑟)(,)𝐵) ⊆ ℂ
300299a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ ℂ)
301165, 61sstri 3761 . . . . . . . . 9 (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ
302301a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ)
30359sselda 3752 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → 𝑧𝐷)
304303, 250syldan 579 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
305 eqid 2771 . . . . . . . . . 10 (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) = (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧)))
306304, 305fmptd 6529 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ)
30754feq2d 6170 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ ↔ (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ))
308306, 307mpbid 222 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ)
309300, 302, 308limcun 23878 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵) = ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)))
310230, 298, 3093eqtr3rd 2814 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)) = ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
311228, 310eleqtrd 2852 . . . . 5 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
312311expr 444 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
31318, 312sylbid 230 . . 3 ((𝜑𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
314313rexlimdva 3179 . 2 (𝜑 → (∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
3159, 314mpd 15 1 (𝜑𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wrex 3062  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  {csn 4317   cuni 4575   class class class wbr 4787  cmpt 4864   × cxp 5248  dom cdm 5250  ran crn 5251  cres 5252  cima 5253  ccom 5254   Fn wfn 6025  wf 6026  cfv 6030  (class class class)co 6795  cc 10139  cr 10140  0cc0 10141   + caddc 10144  *cxr 10278   < clt 10279  cmin 10471   / cdiv 10889  +crp 12034  (,)cioo 12379  abscabs 14181  t crest 16288  TopOpenctopn 16289  topGenctg 16305  ∞Metcxmt 19945  ballcbl 19947  MetOpencmopn 19950  fldccnfld 19960  Topctop 20917  TopOnctopon 20934  intcnt 21041   lim climc 23845   D cdv 23846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-inf2 8705  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218  ax-pre-sup 10219  ax-addf 10220  ax-mulf 10221
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-of 7047  df-om 7216  df-1st 7318  df-2nd 7319  df-supp 7450  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-2o 7717  df-oadd 7720  df-er 7899  df-map 8014  df-pm 8015  df-ixp 8066  df-en 8113  df-dom 8114  df-sdom 8115  df-fin 8116  df-fsupp 8435  df-fi 8476  df-sup 8507  df-inf 8508  df-oi 8574  df-card 8968  df-cda 9195  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-div 10890  df-nn 11226  df-2 11284  df-3 11285  df-4 11286  df-5 11287  df-6 11288  df-7 11289  df-8 11290  df-9 11291  df-n0 11499  df-z 11584  df-dec 11700  df-uz 11893  df-q 11996  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-ioo 12383  df-ioc 12384  df-ico 12385  df-icc 12386  df-fz 12533  df-fzo 12673  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-mulr 16162  df-starv 16163  df-sca 16164  df-vsca 16165  df-ip 16166  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16290  df-topn 16291  df-0g 16309  df-gsum 16310  df-topgen 16311  df-pt 16312  df-prds 16315  df-xrs 16369  df-qtop 16374  df-imas 16375  df-xps 16377  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-submnd 17543  df-mulg 17748  df-cntz 17956  df-cmn 18401  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-fbas 19957  df-fg 19958  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cld 21043  df-ntr 21044  df-cls 21045  df-nei 21122  df-lp 21160  df-perf 21161  df-cn 21251  df-cnp 21252  df-haus 21339  df-cmp 21410  df-tx 21585  df-hmeo 21778  df-fil 21869  df-fm 21961  df-flim 21962  df-flf 21963  df-xms 22344  df-ms 22345  df-tms 22346  df-cncf 22900  df-limc 23849  df-dv 23850
This theorem is referenced by:  taylthlem2  24347  dirkercncflem2  40835  fourierdlem62  40899
  Copyright terms: Public domain W3C validator