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

Theorem lhop 26055
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 2737 . . . . 5 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
21rexmet 24812 . . . 4 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32a1i 11 . . 3 (𝜑 → ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ))
4 lhop.i . . 3 (𝜑𝐼 ∈ (topGen‘ran (,)))
5 lhop.b . . 3 (𝜑𝐵𝐼)
6 eqid 2737 . . . . 5 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
71, 6tgioo 24817 . . . 4 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
87mopni2 24506 . . 3 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐼 ∈ (topGen‘ran (,)) ∧ 𝐵𝐼) → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼)
93, 4, 5, 8syl3anc 1373 . 2 (𝜑 → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼)
10 elssuni 4937 . . . . . . . . 9 (𝐼 ∈ (topGen‘ran (,)) → 𝐼 (topGen‘ran (,)))
11 uniretop 24783 . . . . . . . . 9 ℝ = (topGen‘ran (,))
1210, 11sseqtrrdi 4025 . . . . . . . 8 (𝐼 ∈ (topGen‘ran (,)) → 𝐼 ⊆ ℝ)
134, 12syl 17 . . . . . . 7 (𝜑𝐼 ⊆ ℝ)
1413, 5sseldd 3984 . . . . . 6 (𝜑𝐵 ∈ ℝ)
15 rpre 13043 . . . . . 6 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
161bl2ioo 24813 . . . . . 6 ((𝐵 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
1714, 15, 16syl2an 596 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
1817sseq1d 4015 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼 ↔ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼))
1914adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ)
20 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ+)
2120rpred 13077 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ)
2219, 21resubcld 11691 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) ∈ ℝ)
2322rexrd 11311 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) ∈ ℝ*)
2419, 20ltsubrpd 13109 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵𝑟) < 𝐵)
25 lhop.f . . . . . . . . . . 11 (𝜑𝐹:𝐴⟶ℝ)
2625adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℝ)
27 ssun1 4178 . . . . . . . . . . . 12 ((𝐵𝑟)(,)𝐵) ⊆ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
28 unass 4172 . . . . . . . . . . . . . . 15 (({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
29 uncom 4158 . . . . . . . . . . . . . . . 16 ({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) = (((𝐵𝑟)(,)𝐵) ∪ {𝐵})
3029uneq1i 4164 . . . . . . . . . . . . . . 15 (({𝐵} ∪ ((𝐵𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟)))
3128, 30eqtr3i 2767 . . . . . . . . . . . . . 14 ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟)))
3219rexrd 11311 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ*)
3319, 21readdcld 11290 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ)
3433rexrd 11311 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ*)
3519, 20ltaddrpd 13110 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 < (𝐵 + 𝑟))
36 ioojoin 13523 . . . . . . . . . . . . . . 15 ((((𝐵𝑟) ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) ∧ ((𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))) → ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
3723, 32, 34, 24, 35, 36syl32anc 1380 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
3831, 37eqtrid 2789 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
39 elioo2 13428 . . . . . . . . . . . . . . . . 17 (((𝐵𝑟) ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) → (𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))))
4023, 34, 39syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵𝑟) < 𝐵𝐵 < (𝐵 + 𝑟))))
4119, 24, 35, 40mpbir3and 1343 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((𝐵𝑟)(,)(𝐵 + 𝑟)))
4241snssd 4809 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)))
43 incom 4209 . . . . . . . . . . . . . . 15 ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵})
44 ubioo 13419 . . . . . . . . . . . . . . . . . 18 ¬ 𝐵 ∈ ((𝐵𝑟)(,)𝐵)
45 lbioo 13418 . . . . . . . . . . . . . . . . . 18 ¬ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))
4644, 45pm3.2ni 881 . . . . . . . . . . . . . . . . 17 ¬ (𝐵 ∈ ((𝐵𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟)))
47 elun 4153 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ↔ (𝐵 ∈ ((𝐵𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))))
4846, 47mtbir 323 . . . . . . . . . . . . . . . 16 ¬ 𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
49 disjsn 4711 . . . . . . . . . . . . . . . 16 (((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
5048, 49mpbir 231 . . . . . . . . . . . . . . 15 ((((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅
5143, 50eqtri 2765 . . . . . . . . . . . . . 14 ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅
52 uneqdifeq 4493 . . . . . . . . . . . . . 14 (({𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∧ ({𝐵} ∩ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅) → (({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))))
5342, 51, 52sylancl 586 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (({𝐵} ∪ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))))
5438, 53mpbid 232 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))
5527, 54sseqtrrid 4027 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}))
56 ssdif 4144 . . . . . . . . . . . . . 14 (((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼 → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵}))
5756ad2antll 729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵}))
58 lhop.d . . . . . . . . . . . . 13 𝐷 = (𝐼 ∖ {𝐵})
5957, 58sseqtrrdi 4025 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐷)
60 lhop.if . . . . . . . . . . . . . 14 (𝜑𝐷 ⊆ dom (ℝ D 𝐹))
61 ax-resscn 11212 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ⊆ ℂ)
63 fss 6752 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
6425, 61, 63sylancl 586 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐴⟶ℂ)
65 lhop.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ ℝ)
6662, 64, 65dvbss 25936 . . . . . . . . . . . . . 14 (𝜑 → dom (ℝ D 𝐹) ⊆ 𝐴)
6760, 66sstrd 3994 . . . . . . . . . . . . 13 (𝜑𝐷𝐴)
6867adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷𝐴)
6959, 68sstrd 3994 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐴)
7055, 69sstrd 3994 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ 𝐴)
7126, 70fssresd 6775 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ ((𝐵𝑟)(,)𝐵)):((𝐵𝑟)(,)𝐵)⟶ℝ)
72 lhop.g . . . . . . . . . . 11 (𝜑𝐺:𝐴⟶ℝ)
7372adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℝ)
7473, 70fssresd 6775 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ ((𝐵𝑟)(,)𝐵)):((𝐵𝑟)(,)𝐵)⟶ℝ)
7561a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ℝ ⊆ ℂ)
7664adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℂ)
7765adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐴 ⊆ ℝ)
78 ioossre 13448 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)𝐵) ⊆ ℝ
7978a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ ℝ)
80 eqid 2737 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
81 tgioo4 24826 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
8280, 81dvres 25946 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
8375, 76, 77, 79, 82syl22anc 839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
84 retop 24782 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
85 iooretop 24786 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)𝐵) ∈ (topGen‘ran (,))
86 isopn3i 23090 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ ((𝐵𝑟)(,)𝐵) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
8784, 85, 86mp2an 692 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵)
8887reseq2i 5994 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))
8983, 88eqtrdi 2793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)))
9089dmeqd 5916 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)))
9155, 59sstrd 3994 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ 𝐷)
9260adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐹))
9391, 92sstrd 3994 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹))
94 ssdmres 6031 . . . . . . . . . . 11 (((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
9593, 94sylib 218 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
9690, 95eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵))) = ((𝐵𝑟)(,)𝐵))
97 fss 6752 . . . . . . . . . . . . . . 15 ((𝐺:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:𝐴⟶ℂ)
9872, 61, 97sylancl 586 . . . . . . . . . . . . . 14 (𝜑𝐺:𝐴⟶ℂ)
9998adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℂ)
10080, 81dvres 25946 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
10175, 99, 77, 79, 100syl22anc 839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))))
10287reseq2i 5994 . . . . . . . . . . . 12 ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))
103101, 102eqtrdi 2793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
104103dmeqd 5916 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
105 lhop.ig . . . . . . . . . . . . 13 (𝜑𝐷 ⊆ dom (ℝ D 𝐺))
106105adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐺))
10791, 106sstrd 3994 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺))
108 ssdmres 6031 . . . . . . . . . . 11 (((𝐵𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
109107, 108sylib 218 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)) = ((𝐵𝑟)(,)𝐵))
110104, 109eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((𝐵𝑟)(,)𝐵))
111 limcresi 25920 . . . . . . . . . 10 (𝐹 lim 𝐵) ⊆ ((𝐹 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
112 lhop.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
113112adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐹 lim 𝐵))
114111, 113sselid 3981 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
115 limcresi 25920 . . . . . . . . . 10 (𝐺 lim 𝐵) ⊆ ((𝐺 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
116 lhop.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
117116adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐺 lim 𝐵))
118115, 117sselid 3981 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
119 df-ima 5698 . . . . . . . . . . 11 (𝐺 “ ((𝐵𝑟)(,)𝐵)) = ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵))
120 imass2 6120 . . . . . . . . . . . 12 (((𝐵𝑟)(,)𝐵) ⊆ 𝐷 → (𝐺 “ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
12191, 120syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
122119, 121eqsstrrid 4023 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵)) ⊆ (𝐺𝐷))
123 lhop.gn0 . . . . . . . . . . 11 (𝜑 → ¬ 0 ∈ (𝐺𝐷))
124123adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ (𝐺𝐷))
125122, 124ssneldd 3986 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))
126103rneqd 5949 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ran ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵)))
127 df-ima 5698 . . . . . . . . . . . 12 ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) = ran ((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))
128126, 127eqtr4di 2795 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) = ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)))
129 imass2 6120 . . . . . . . . . . . 12 (((𝐵𝑟)(,)𝐵) ⊆ 𝐷 → ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷))
13091, 129syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ ((𝐵𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷))
131128, 130eqsstrd 4018 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))) ⊆ ((ℝ D 𝐺) “ 𝐷))
132 lhop.gd0 . . . . . . . . . . 11 (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
133132adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷))
134131, 133ssneldd 3986 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵))))
135 limcresi 25920 . . . . . . . . . . 11 ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵)
13691resmptd 6058 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
13789fveq1d 6908 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))
138 fvres 6925 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((ℝ D 𝐹) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
139137, 138sylan9eq 2797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
140103fveq1d 6908 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))
141 fvres 6925 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((ℝ D 𝐺) ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
142140, 141sylan9eq 2797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
143139, 142oveq12d 7449 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵𝑟)(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
144143mpteq2dva 5242 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
145136, 144eqtr4d 2780 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))))
146145oveq1d 7446 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) = ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
147135, 146sseqtrid 4026 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
148 lhop.c . . . . . . . . . . 11 (𝜑𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
149148adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
150147, 149sseldd 3984 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵𝑟)(,)𝐵)))‘𝑧))) lim 𝐵))
15123, 19, 24, 71, 74, 96, 110, 114, 118, 125, 134, 150lhop2 26054 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) lim 𝐵))
15255resmptd 6058 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
153 fvres 6925 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → ((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = (𝐹𝑧))
154 fvres 6925 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) = (𝐺𝑧))
155153, 154oveq12d 7449 . . . . . . . . . . 11 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) → (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
156155mpteq2ia 5245 . . . . . . . . . 10 (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))
157152, 156eqtr4di 2795 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))))
158157oveq1d 7446 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) = ((𝑧 ∈ ((𝐵𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵𝑟)(,)𝐵))‘𝑧))) lim 𝐵))
159151, 158eleqtrrd 2844 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵))
160 ssun2 4179 . . . . . . . . . . . 12 (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))
161160, 54sseqtrrid 4027 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}))
162161, 69sstrd 3994 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐴)
16326, 162fssresd 6775 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ)
16473, 162fssresd 6775 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ)
165 ioossre 13448 . . . . . . . . . . . . . 14 (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ
166165a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)
16780, 81dvres 25946 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
16875, 76, 77, 166, 167syl22anc 839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
169 iooretop 24786 . . . . . . . . . . . . . 14 (𝐵(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))
170 isopn3i 23090 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (𝐵(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
17184, 169, 170mp2an 692 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))
172171reseq2i 5994 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))
173168, 172eqtrdi 2793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))))
174173dmeqd 5916 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))))
175161, 59sstrd 3994 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷)
176175, 92sstrd 3994 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹))
177 ssdmres 6031 . . . . . . . . . . 11 ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
178176, 177sylib 218 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
179174, 178eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟)))
18080, 81dvres 25946 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
18175, 99, 77, 166, 180syl22anc 839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))))
182171reseq2i 5994 . . . . . . . . . . . 12 ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))
183181, 182eqtrdi 2793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
184183dmeqd 5916 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
185175, 106sstrd 3994 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺))
186 ssdmres 6031 . . . . . . . . . . 11 ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
187185, 186sylib 218 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)))
188184, 187eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟)))
189 limcresi 25920 . . . . . . . . . 10 (𝐹 lim 𝐵) ⊆ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
190189, 113sselid 3981 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
191 limcresi 25920 . . . . . . . . . 10 (𝐺 lim 𝐵) ⊆ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
192191, 117sselid 3981 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
193 df-ima 5698 . . . . . . . . . . 11 (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) = ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))
194 imass2 6120 . . . . . . . . . . . 12 ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
195175, 194syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
196193, 195eqsstrrid 4023 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺𝐷))
197196, 124ssneldd 3986 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))
198183rneqd 5949 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))))
199 df-ima 5698 . . . . . . . . . . . 12 ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))
200198, 199eqtr4di 2795 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))))
201 imass2 6120 . . . . . . . . . . . 12 ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷))
202175, 201syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷))
203200, 202eqsstrd 4018 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) ⊆ ((ℝ D 𝐺) “ 𝐷))
204203, 133ssneldd 3986 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))))
205 limcresi 25920 . . . . . . . . . . 11 ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)
206175resmptd 6058 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
207173fveq1d 6908 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))
208 fvres 6925 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
209207, 208sylan9eq 2797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐹)‘𝑧))
210183fveq1d 6908 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))
211 fvres 6925 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
212210, 211sylan9eq 2797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐺)‘𝑧))
213209, 212oveq12d 7449 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
214213mpteq2dva 5242 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))))
215206, 214eqtr4d 2780 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))))
216215oveq1d 7446 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
217205, 216sseqtrid 4026 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵) ⊆ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
218217, 149sseldd 3984 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) lim 𝐵))
21919, 34, 35, 163, 164, 179, 188, 190, 192, 197, 204, 218lhop1 26053 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) lim 𝐵))
220161resmptd 6058 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹𝑧) / (𝐺𝑧))))
221 fvres 6925 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐹𝑧))
222 fvres 6925 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐺𝑧))
223221, 222oveq12d 7449 . . . . . . . . . . 11 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
224223mpteq2ia 5245 . . . . . . . . . 10 (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹𝑧) / (𝐺𝑧)))
225220, 224eqtr4di 2795 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))))
226225oveq1d 7446 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) lim 𝐵))
227219, 226eleqtrrd 2844 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵))
228159, 227elind 4200 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)))
22959resmptd 6058 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) = (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))))
230229oveq1d 7446 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) lim 𝐵) = ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
23167sselda 3983 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷) → 𝑧𝐴)
23225ffvelcdmda 7104 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℝ)
233231, 232syldan 591 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (𝐹𝑧) ∈ ℝ)
234233recnd 11289 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐹𝑧) ∈ ℂ)
23572ffvelcdmda 7104 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (𝐺𝑧) ∈ ℝ)
236231, 235syldan 591 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ ℝ)
237236recnd 11289 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ ℂ)
238123adantr 480 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → ¬ 0 ∈ (𝐺𝐷))
23972ffnd 6737 . . . . . . . . . . . . . . . 16 (𝜑𝐺 Fn 𝐴)
240239adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝐺 Fn 𝐴)
24167adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝐷𝐴)
242 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐷) → 𝑧𝐷)
243 fnfvima 7253 . . . . . . . . . . . . . . 15 ((𝐺 Fn 𝐴𝐷𝐴𝑧𝐷) → (𝐺𝑧) ∈ (𝐺𝐷))
244240, 241, 242, 243syl3anc 1373 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐷) → (𝐺𝑧) ∈ (𝐺𝐷))
245 eleq1 2829 . . . . . . . . . . . . . 14 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ (𝐺𝐷) ↔ 0 ∈ (𝐺𝐷)))
246244, 245syl5ibcom 245 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷) → ((𝐺𝑧) = 0 → 0 ∈ (𝐺𝐷)))
247246necon3bd 2954 . . . . . . . . . . . 12 ((𝜑𝑧𝐷) → (¬ 0 ∈ (𝐺𝐷) → (𝐺𝑧) ≠ 0))
248238, 247mpd 15 . . . . . . . . . . 11 ((𝜑𝑧𝐷) → (𝐺𝑧) ≠ 0)
249234, 237, 248divcld 12043 . . . . . . . . . 10 ((𝜑𝑧𝐷) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
250249adantlr 715 . . . . . . . . 9 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧𝐷) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
251250fmpttd 7135 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))):𝐷⟶ℂ)
252 difss 4136 . . . . . . . . . . 11 (𝐼 ∖ {𝐵}) ⊆ 𝐼
25358, 252eqsstri 4030 . . . . . . . . . 10 𝐷𝐼
25413, 61sstrdi 3996 . . . . . . . . . 10 (𝜑𝐼 ⊆ ℂ)
255253, 254sstrid 3995 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
256255adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ ℂ)
257 eqid 2737 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))
25858uneq1i 4164 . . . . . . . . . . . . . . . . 17 (𝐷 ∪ {𝐵}) = ((𝐼 ∖ {𝐵}) ∪ {𝐵})
259 undif1 4476 . . . . . . . . . . . . . . . . 17 ((𝐼 ∖ {𝐵}) ∪ {𝐵}) = (𝐼 ∪ {𝐵})
260258, 259eqtri 2765 . . . . . . . . . . . . . . . 16 (𝐷 ∪ {𝐵}) = (𝐼 ∪ {𝐵})
261 simprr 773 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)
26242, 261sstrd 3994 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ 𝐼)
263 ssequn2 4189 . . . . . . . . . . . . . . . . 17 ({𝐵} ⊆ 𝐼 ↔ (𝐼 ∪ {𝐵}) = 𝐼)
264262, 263sylib 218 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐼 ∪ {𝐵}) = 𝐼)
265260, 264eqtrid 2789 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐷 ∪ {𝐵}) = 𝐼)
266265oveq2d 7447 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t 𝐼))
26713adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℝ)
268 eqid 2737 . . . . . . . . . . . . . . . 16 (topGen‘ran (,)) = (topGen‘ran (,))
26980, 268rerest 24825 . . . . . . . . . . . . . . 15 (𝐼 ⊆ ℝ → ((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,)) ↾t 𝐼))
270267, 269syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,)) ↾t 𝐼))
271266, 270eqtrd 2777 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((topGen‘ran (,)) ↾t 𝐼))
272271fveq2d 6910 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))) = (int‘((topGen‘ran (,)) ↾t 𝐼)))
273272fveq1d 6908 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
27480cnfldtopon 24803 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
275254adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℂ)
276 resttopon 23169 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝐼 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼))
277274, 275, 276sylancr 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼))
278 topontop 22919 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top)
279277, 278syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top)
280270, 279eqeltrrd 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((topGen‘ran (,)) ↾t 𝐼) ∈ Top)
281 iooretop 24786 . . . . . . . . . . . . . 14 ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,))
282281a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)))
2834adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ∈ (topGen‘ran (,)))
284 restopn2 23185 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ 𝐼 ∈ (topGen‘ran (,))) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)))
28584, 283, 284sylancr 587 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)))
286282, 261, 285mpbir2and 713 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼))
287 isopn3i 23090 . . . . . . . . . . . 12 ((((topGen‘ran (,)) ↾t 𝐼) ∈ Top ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,)) ↾t 𝐼)) → ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
288280, 286, 287syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
289273, 288eqtrd 2777 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
29041, 289eleqtrrd 2844 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
291 undif1 4476 . . . . . . . . . . 11 ((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵})
292 ssequn2 4189 . . . . . . . . . . . 12 ({𝐵} ⊆ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
29342, 292sylib 218 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
294291, 293eqtrid 2789 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = ((𝐵𝑟)(,)(𝐵 + 𝑟)))
295294fveq2d 6910 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})) = ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵𝑟)(,)(𝐵 + 𝑟))))
296290, 295eleqtrrd 2844 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})))
297251, 59, 256, 80, 257, 296limcres 25921 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) lim 𝐵) = ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
29878, 61sstri 3993 . . . . . . . . 9 ((𝐵𝑟)(,)𝐵) ⊆ ℂ
299298a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵𝑟)(,)𝐵) ⊆ ℂ)
300165, 61sstri 3993 . . . . . . . . 9 (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ
301300a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ)
30259sselda 3983 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → 𝑧𝐷)
303302, 250syldan 591 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
304303fmpttd 7135 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ)
30554feq2d 6722 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ ↔ (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ))
306304, 305mpbid 232 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))):(((𝐵𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ)
307299, 301, 306limcun 25930 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵) = ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)))
308230, 297, 3073eqtr3rd 2786 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ ((𝐵𝑟)(,)𝐵)) lim 𝐵) ∩ (((𝑧 ∈ (((𝐵𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) lim 𝐵)) = ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
309228, 308eleqtrd 2843 . . . . 5 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
310309expr 456 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (((𝐵𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
31118, 310sylbid 240 . . 3 ((𝜑𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
312311rexlimdva 3155 . 2 (𝜑 → (∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵)))
3139, 312mpd 15 1 (𝜑𝐶 ∈ ((𝑧𝐷 ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wrex 3070  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626   cuni 4907   class class class wbr 5143  cmpt 5225   × cxp 5683  dom cdm 5685  ran crn 5686  cres 5687  cima 5688  ccom 5689   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155   + caddc 11158  *cxr 11294   < clt 11295  cmin 11492   / cdiv 11920  +crp 13034  (,)cioo 13387  abscabs 15273  t crest 17465  TopOpenctopn 17466  topGenctg 17482  ∞Metcxmet 21349  ballcbl 21351  MetOpencmopn 21354  fldccnfld 21364  Topctop 22899  TopOnctopon 22916  intcnt 23025   lim climc 25897   D cdv 25898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902
This theorem is referenced by:  taylthlem2  26416  taylthlem2OLD  26417  dirkercncflem2  46119  fourierdlem62  46183
  Copyright terms: Public domain W3C validator