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

Theorem lhop 24628
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 2824 . . . . 5 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
21rexmet 23405 . . . 4 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32a1i 11 . . 3 (𝜑 → ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ))
4 lhop.i . . 3 (𝜑𝐼 ∈ (topGen‘ran (,)))
5 lhop.b . . 3 (𝜑𝐵𝐼)
6 eqid 2824 . . . . 5 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
71, 6tgioo 23410 . . . 4 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
87mopni2 23109 . . 3 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐼 ∈ (topGen‘ran (,)) ∧ 𝐵𝐼) → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼)
93, 4, 5, 8syl3anc 1368 . 2 (𝜑 → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼)
10 elssuni 4854 . . . . . . . . 9 (𝐼 ∈ (topGen‘ran (,)) → 𝐼 (topGen‘ran (,)))
11 uniretop 23377 . . . . . . . . 9 ℝ = (topGen‘ran (,))
1210, 11sseqtrrdi 4004 . . . . . . . 8 (𝐼 ∈ (topGen‘ran (,)) → 𝐼 ⊆ ℝ)
134, 12syl 17 . . . . . . 7 (𝜑𝐼 ⊆ ℝ)
1413, 5sseldd 3954 . . . . . 6 (𝜑𝐵 ∈ ℝ)
15 rpre 12396 . . . . . 6 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
161bl2ioo 23406 . . . . . 6 ((𝐵 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
1714, 15, 16syl2an 598 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
1817sseq1d 3984 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼 ↔ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼))
1914adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ)
20 simprl 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ+)
2120rpred 12430 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ)
2219, 21resubcld 11068 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) ∈ ℝ)
2322rexrd 10691 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) ∈ ℝ*)
2419, 20ltsubrpd 12462 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) < 𝐵)
25 lhop.f . . . . . . . . . . 11 (𝜑𝐹:𝐴⟶ℝ)
2625adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℝ)
27 ssun1 4134 . . . . . . . . . . . 12 ((𝐵𝑟)(,)𝐵) ⊆ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
28 unass 4128 . . . . . . . . . . . . . . 15 (({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
29 uncom 4115 . . . . . . . . . . . . . . . 16 ({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) = (((𝐵𝑟)(,)𝐵) ∪ {𝐵})
3029uneq1i 4121 . . . . . . . . . . . . . . 15 (({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟)))
3128, 30eqtr3i 2849 . . . . . . . . . . . . . 14 ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟)))
3219rexrd 10691 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ*)
3319, 21readdcld 10670 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ)
3433rexrd 10691 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ*)
3519, 20ltaddrpd 12463 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 < (𝐵 + 𝑟))
36 ioojoin 12872 . . . . . . . . . . . . . . 15 ((((𝐵𝑟) ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) ∧ ((𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))) → ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
3723, 32, 34, 24, 35, 36syl32anc 1375 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
3831, 37syl5eq 2871 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
39 elioo2 12778 . . . . . . . . . . . . . . . . 17 (((𝐵𝑟) ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) → (𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))))
4023, 34, 39syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))))
4119, 24, 35, 40mpbir3and 1339 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)))
4241snssd 4726 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)))
43 incom 4163 . . . . . . . . . . . . . . 15 ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵})
44 ubioo 12769 . . . . . . . . . . . . . . . . . 18 ¬ 𝐵 ∈ ((𝐵𝑟)(,)𝐵)
45 lbioo 12768 . . . . . . . . . . . . . . . . . 18 ¬ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))
4644, 45pm3.2ni 878 . . . . . . . . . . . . . . . . 17 ¬ (𝐵 ∈ ((𝐵𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟)))
47 elun 4111 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ↔ (𝐵 ∈ ((𝐵𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))))
4846, 47mtbir 326 . . . . . . . . . . . . . . . 16 ¬ 𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
49 disjsn 4632 . . . . . . . . . . . . . . . 16 (((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
5048, 49mpbir 234 . . . . . . . . . . . . . . 15 ((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅
5143, 50eqtri 2847 . . . . . . . . . . . . . 14 ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅
52 uneqdifeq 4421 . . . . . . . . . . . . . 14 (({𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∧ ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅) → (({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))))
5342, 51, 52sylancl 589 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))))
5438, 53mpbid 235 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
5527, 54sseqtrrid 4006 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}))
56 ssdif 4102 . . . . . . . . . . . . . 14 (((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼 → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵}))
5756ad2antll 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵}))
58 lhop.d . . . . . . . . . . . . 13 𝐷 = (𝐼 ∖ {𝐵})
5957, 58sseqtrrdi 4004 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐷)
60 lhop.if . . . . . . . . . . . . . 14 (𝜑𝐷 ⊆ dom (ℝ D 𝐹))
61 ax-resscn 10594 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ⊆ ℂ)
63 fss 6519 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
6425, 61, 63sylancl 589 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐴⟶ℂ)
65 lhop.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ ℝ)
6662, 64, 65dvbss 24513 . . . . . . . . . . . . . 14 (𝜑 → dom (ℝ D 𝐹) ⊆ 𝐴)
6760, 66sstrd 3963 . . . . . . . . . . . . 13 (𝜑𝐷𝐴)
6867adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷𝐴)
6959, 68sstrd 3963 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐴)
7055, 69sstrd 3963 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ 𝐴)
7126, 70fssresd 6537 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ ((𝐵𝑟)(,)𝐵)):((𝐵𝑟)(,)𝐵)⟶ℝ)
72 lhop.g . . . . . . . . . . 11 (𝜑𝐺:𝐴⟶ℝ)
7372adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℝ)
7473, 70fssresd 6537 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ ((𝐵𝑟)(,)𝐵)):((𝐵𝑟)(,)𝐵)⟶ℝ)
7561a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ℝ ⊆ ℂ)
7664adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℂ)
7765adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐴 ⊆ ℝ)
78 ioossre 12797 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)𝐵) ⊆ ℝ
7978a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ ℝ)
80 eqid 2824 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8180tgioo2 23417 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
8280, 81dvres 24523 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
8375, 76, 77, 79, 82syl22anc 837 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
84 retop 23376 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
85 iooretop 23380 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)𝐵) ∈ (topGen‘ran (,))
86 isopn3i 21696 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ ((𝐵𝑟)(,)𝐵) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
8784, 85, 86mp2an 691 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵)
8887reseq2i 5839 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))
8983, 88syl6eq 2875 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)))
9089dmeqd 5762 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)))
9155, 59sstrd 3963 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ 𝐷)
9260adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐹))
9391, 92sstrd 3963 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹))
94 ssdmres 5865 . . . . . . . . . . 11 (((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
9593, 94sylib 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
9690, 95eqtrd 2859 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((𝐵𝑟)(,)𝐵))
97 fss 6519 . . . . . . . . . . . . . . 15 ((𝐺:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:𝐴⟶ℂ)
9872, 61, 97sylancl 589 . . . . . . . . . . . . . 14 (𝜑𝐺:𝐴⟶ℂ)
9998adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℂ)
10080, 81dvres 24523 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
10175, 99, 77, 79, 100syl22anc 837 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
10287reseq2i 5839 . . . . . . . . . . . 12 ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))
103101, 102syl6eq 2875 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
104103dmeqd 5762 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
105 lhop.ig . . . . . . . . . . . . 13 (𝜑𝐷 ⊆ dom (ℝ D 𝐺))
106105adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐺))
10791, 106sstrd 3963 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺))
108 ssdmres 5865 . . . . . . . . . . 11 (((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
109107, 108sylib 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
110104, 109eqtrd 2859 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((𝐵𝑟)(,)𝐵))
111 limcresi 24497 . . . . . . . . . 10 (𝐹 lim 𝐵) ⊆ ((𝐹 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
112 lhop.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
113112adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐹 lim 𝐵))
114111, 113sseldi 3951 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
115 limcresi 24497 . . . . . . . . . 10 (𝐺 lim 𝐵) ⊆ ((𝐺 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
116 lhop.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
117116adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐺 lim 𝐵))
118115, 117sseldi 3951 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
119 df-ima 5556 . . . . . . . . . . 11 (𝐺 “ ((𝐵𝑟)(,)𝐵)) = ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵))
120 imass2 5954 . . . . . . . . . . . 12 (((𝐵𝑟)(,)𝐵) ⊆ 𝐷 → (𝐺 “ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
12191, 120syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
122119, 121eqsstrrid 4002 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
123 lhop.gn0 . . . . . . . . . . 11 (𝜑 → ¬ 0 ∈ (𝐺𝐷))
124123adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ (𝐺𝐷))
125122, 124ssneldd 3956 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))
126103rneqd 5796 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ran ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
127 df-ima 5556 . . . . . . . . . . . 12 ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) = ran ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))
128126, 127eqtr4di 2877 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)))
129 imass2 5954 . . . . . . . . . . . 12 (((𝐵𝑟)(,)𝐵) ⊆ 𝐷 → ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷))
13091, 129syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷))
131128, 130eqsstrd 3991 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) ⊆ ((ℝ D 𝐺) “ 𝐷))
132 lhop.gd0 . . . . . . . . . . 11 (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
133132adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
134131, 133ssneldd 3956 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))))
135 limcresi 24497 . . . . . . . . . . 11 ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
13691resmptd 5897 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
13789fveq1d 6665 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))
138 fvres 6682 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
139137, 138sylan9eq 2879 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
140103fveq1d 6665 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))
141 fvres 6682 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
142140, 141sylan9eq 2879 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
143139, 142oveq12d 7169 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
144143mpteq2dva 5148 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
145136, 144eqtr4d 2862 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))))
146145oveq1d 7166 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) = ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
147135, 146sseqtrid 4005 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
148 lhop.c . . . . . . . . . . 11 (𝜑𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
149148adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
150147, 149sseldd 3954 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
15123, 19, 24, 71, 74, 96, 110, 114, 118, 125, 134, 150lhop2 24627 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) lim 𝐵))
15255resmptd 5897 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
153 fvres 6682 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → ((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = (𝐹𝑧))
154 fvres 6682 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = (𝐺𝑧))
155153, 154oveq12d 7169 . . . . . . . . . . 11 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
156155mpteq2ia 5144 . . . . . . . . . 10 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))
157152, 156eqtr4di 2877 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))))
158157oveq1d 7166 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) = ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) lim 𝐵))
159151, 158eleqtrrd 2919 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
160 ssun2 4135 . . . . . . . . . . . 12 (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
161160, 54sseqtrrid 4006 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}))
162161, 69sstrd 3963 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐴)
16326, 162fssresd 6537 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ)
16473, 162fssresd 6537 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ)
165 ioossre 12797 . . . . . . . . . . . . . 14 (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ
166165a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)
16780, 81dvres 24523 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
16875, 76, 77, 166, 167syl22anc 837 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
169 iooretop 23380 . . . . . . . . . . . . . 14 (𝐵(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))
170 isopn3i 21696 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (𝐵(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
17184, 169, 170mp2an 691 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))
172171reseq2i 5839 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))
173168, 172syl6eq 2875 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))))
174173dmeqd 5762 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))))
175161, 59sstrd 3963 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷)
176175, 92sstrd 3963 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹))
177 ssdmres 5865 . . . . . . . . . . 11 ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
178176, 177sylib 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
179174, 178eqtrd 2859 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟)))
18080, 81dvres 24523 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
18175, 99, 77, 166, 180syl22anc 837 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
182171reseq2i 5839 . . . . . . . . . . . 12 ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))
183181, 182syl6eq 2875 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
184183dmeqd 5762 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
185175, 106sstrd 3963 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺))
186 ssdmres 5865 . . . . . . . . . . 11 ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
187185, 186sylib 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
188184, 187eqtrd 2859 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟)))
189 limcresi 24497 . . . . . . . . . 10 (𝐹 lim 𝐵) ⊆ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
190189, 113sseldi 3951 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
191 limcresi 24497 . . . . . . . . . 10 (𝐺 lim 𝐵) ⊆ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
192191, 117sseldi 3951 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
193 df-ima 5556 . . . . . . . . . . 11 (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) = ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))
194 imass2 5954 . . . . . . . . . . . 12 ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
195175, 194syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
196193, 195eqsstrrid 4002 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
197196, 124ssneldd 3956 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))
198183rneqd 5796 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
199 df-ima 5556 . . . . . . . . . . . 12 ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))
200198, 199eqtr4di 2877 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))))
201 imass2 5954 . . . . . . . . . . . 12 ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷))
202175, 201syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷))
203200, 202eqsstrd 3991 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) ⊆ ((ℝ D 𝐺) “ 𝐷))
204203, 133ssneldd 3956 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))))
205 limcresi 24497 . . . . . . . . . . 11 ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
206175resmptd 5897 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
207173fveq1d 6665 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))
208 fvres 6682 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
209207, 208sylan9eq 2879 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
210183fveq1d 6665 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))
211 fvres 6682 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
212210, 211sylan9eq 2879 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
213209, 212oveq12d 7169 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
214213mpteq2dva 5148 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
215206, 214eqtr4d 2862 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))))
216215oveq1d 7166 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
217205, 216sseqtrid 4005 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
218217, 149sseldd 3954 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
21919, 34, 35, 163, 164, 179, 188, 190, 192, 197, 204, 218lhop1 24626 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) lim 𝐵))
220161resmptd 5897 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹𝑧) / (𝐺𝑧))))
221 fvres 6682 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐹𝑧))
222 fvres 6682 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐺𝑧))
223221, 222oveq12d 7169 . . . . . . . . . . 11 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
224223mpteq2ia 5144 . . . . . . . . . 10 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹𝑧) / (𝐺𝑧)))
225220, 224eqtr4di 2877 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))))
226225oveq1d 7166 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) lim 𝐵))
227219, 226eleqtrrd 2919 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
228159, 227elind 4156 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)))
22959resmptd 5897 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) = (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))))
230229oveq1d 7166 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) lim 𝐵) = ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
23167sselda 3953 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷) → 𝑧𝐴)
23225ffvelrnda 6844 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℝ)
233231, 232syldan 594 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (𝐹𝑧) ∈ ℝ)
234233recnd 10669 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐹𝑧) ∈ ℂ)
23572ffvelrnda 6844 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (𝐺𝑧) ∈ ℝ)
236231, 235syldan 594 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ ℝ)
237236recnd 10669 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ ℂ)
238123adantr 484 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → ¬ 0 ∈ (𝐺𝐷))
23972ffnd 6506 . . . . . . . . . . . . . . . 16 (𝜑𝐺 Fn 𝐴)
240239adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝐺 Fn 𝐴)
24167adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝐷𝐴)
242 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝑧𝐷)
243 fnfvima 6989 . . . . . . . . . . . . . . 15 ((𝐺 Fn 𝐴𝐷𝐴𝑧𝐷) → (𝐺𝑧) ∈ (𝐺𝐷))
244240, 241, 242, 243syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ (𝐺𝐷))
245 eleq1 2903 . . . . . . . . . . . . . 14 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ (𝐺𝐷) ↔ 0 ∈ (𝐺𝐷)))
246244, 245syl5ibcom 248 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷) → ((𝐺𝑧) = 0 → 0 ∈ (𝐺𝐷)))
247246necon3bd 3028 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (¬ 0 ∈ (𝐺𝐷) → (𝐺𝑧) ≠ 0))
248238, 247mpd 15 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐺𝑧) ≠ 0)
249234, 237, 248divcld 11416 . . . . . . . . . 10 ((𝜑𝑧𝐷) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
250249adantlr 714 . . . . . . . . 9 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧𝐷) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
251250fmpttd 6872 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))):𝐷⟶ℂ)
252 difss 4094 . . . . . . . . . . 11 (𝐼 ∖ {𝐵}) ⊆ 𝐼
25358, 252eqsstri 3987 . . . . . . . . . 10 𝐷𝐼
25413, 61sstrdi 3965 . . . . . . . . . 10 (𝜑𝐼 ⊆ ℂ)
255253, 254sstrid 3964 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
256255adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ ℂ)
257 eqid 2824 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))
25858uneq1i 4121 . . . . . . . . . . . . . . . . 17 (𝐷 ∪ {𝐵}) = ((𝐼 ∖ {𝐵}) ∪ {𝐵})
259 undif1 4407 . . . . . . . . . . . . . . . . 17 ((𝐼 ∖ {𝐵}) ∪ {𝐵}) = (𝐼 ∪ {𝐵})
260258, 259eqtri 2847 . . . . . . . . . . . . . . . 16 (𝐷 ∪ {𝐵}) = (𝐼 ∪ {𝐵})
261 simprr 772 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)
26242, 261sstrd 3963 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ 𝐼)
263 ssequn2 4145 . . . . . . . . . . . . . . . . 17 ({𝐵} ⊆ 𝐼 ↔ (𝐼 ∪ {𝐵}) = 𝐼)
264262, 263sylib 221 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐼 ∪ {𝐵}) = 𝐼)
265260, 264syl5eq 2871 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐷 ∪ {𝐵}) = 𝐼)
266265oveq2d 7167 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t 𝐼))
26713adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℝ)
268 eqid 2824 . . . . . . . . . . . . . . . 16 (topGen‘ran (,)) = (topGen‘ran (,))
26980, 268rerest 23418 . . . . . . . . . . . . . . 15 (𝐼 ⊆ ℝ → ((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,)) ↾t 𝐼))
270267, 269syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,)) ↾t 𝐼))
271266, 270eqtrd 2859 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((topGen‘ran (,)) ↾t 𝐼))
272271fveq2d 6667 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))) = (int‘((topGen‘ran (,)) ↾t 𝐼)))
273272fveq1d 6665 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
27480cnfldtopon 23397 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
275254adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℂ)
276 resttopon 21775 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝐼 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼))
277274, 275, 276sylancr 590 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼))
278 topontop 21527 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top)
279277, 278syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top)
280270, 279eqeltrrd 2917 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((topGen‘ran (,)) ↾t 𝐼) ∈ Top)
281 iooretop 23380 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))
282281a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)))
2834adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ∈ (topGen‘ran (,)))
284 restopn2 21791 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ 𝐼 ∈ (topGen‘ran (,))) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)))
28584, 283, 284sylancr 590 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)))
286282, 261, 285mpbir2and 712 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼))
287 isopn3i 21696 . . . . . . . . . . . 12 ((((topGen‘ran (,)) ↾t 𝐼) ∈ Top ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼)) → ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
288280, 286, 287syl2anc 587 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
289273, 288eqtrd 2859 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
29041, 289eleqtrrd 2919 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
291 undif1 4407 . . . . . . . . . . 11 ((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵})
292 ssequn2 4145 . . . . . . . . . . . 12 ({𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
29342, 292sylib 221 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
294291, 293syl5eq 2871 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
295294fveq2d 6667 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})) = ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
296290, 295eleqtrrd 2919 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})))
297251, 59, 256, 80, 257, 296limcres 24498 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) lim 𝐵) = ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
29878, 61sstri 3962 . . . . . . . . 9 ((𝐵𝑟)(,)𝐵) ⊆ ℂ
299298a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ ℂ)
300165, 61sstri 3962 . . . . . . . . 9 (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ
301300a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ)
30259sselda 3953 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → 𝑧𝐷)
303302, 250syldan 594 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
304303fmpttd 6872 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ)
30554feq2d 6491 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ ↔ (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ))
306304, 305mpbid 235 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ)
307299, 301, 306limcun 24507 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵) = ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)))
308230, 297, 3073eqtr3rd 2868 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)) = ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
309228, 308eleqtrd 2918 . . . . 5 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
310309expr 460 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
31118, 310sylbid 243 . . 3 ((𝜑𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
312311rexlimdva 3276 . 2 (𝜑 → (∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
3139, 312mpd 15 1 (𝜑𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2115  wne 3014  wrex 3134  cdif 3916  cun 3917  cin 3918  wss 3919  c0 4276  {csn 4550   cuni 4824   class class class wbr 5053  cmpt 5133   × cxp 5541  dom cdm 5543  ran crn 5544  cres 5545  cima 5546  ccom 5547   Fn wfn 6340  wf 6341  cfv 6345  (class class class)co 7151  cc 10535  cr 10536  0cc0 10537   + caddc 10540  *cxr 10674   < clt 10675  cmin 10870   / cdiv 11297  +crp 12388  (,)cioo 12737  abscabs 14595  t crest 16696  TopOpenctopn 16697  topGenctg 16713  ∞Metcxmet 20085  ballcbl 20087  MetOpencmopn 20090  fldccnfld 20100  Topctop 21507  TopOnctopon 21524  intcnt 21631   lim climc 24474   D cdv 24475
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615  ax-addf 10616  ax-mulf 10617
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7405  df-om 7577  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-fi 8874  df-sup 8905  df-inf 8906  df-oi 8973  df-card 9367  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11637  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-q 12348  df-rp 12389  df-xneg 12506  df-xadd 12507  df-xmul 12508  df-ioo 12741  df-ioc 12742  df-ico 12743  df-icc 12744  df-fz 12897  df-fzo 13040  df-seq 13376  df-exp 13437  df-hash 13698  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910  df-psmet 20092  df-xmet 20093  df-met 20094  df-bl 20095  df-mopn 20096  df-fbas 20097  df-fg 20098  df-cnfld 20101  df-top 21508  df-topon 21525  df-topsp 21547  df-bases 21560  df-cld 21633  df-ntr 21634  df-cls 21635  df-nei 21712  df-lp 21750  df-perf 21751  df-cn 21841  df-cnp 21842  df-haus 21929  df-cmp 22001  df-tx 22176  df-hmeo 22369  df-fil 22460  df-fm 22552  df-flim 22553  df-flf 22554  df-xms 22936  df-ms 22937  df-tms 22938  df-cncf 23492  df-limc 24478  df-dv 24479
This theorem is referenced by:  taylthlem2  24978  dirkercncflem2  42699  fourierdlem62  42763
  Copyright terms: Public domain W3C validator