| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 2 | 1 | rexmet 24812 |
. . . 4
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ((abs ∘ − )
↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
| 4 | | lhop.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (topGen‘ran
(,))) |
| 5 | | lhop.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝐼) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
| 7 | 1, 6 | tgioo 24817 |
. . . 4
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
| 8 | 7 | mopni2 24506 |
. . 3
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝐼 ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ 𝐼) → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼) |
| 9 | 3, 4, 5, 8 | syl3anc 1373 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼) |
| 10 | | elssuni 4937 |
. . . . . . . . 9
⊢ (𝐼 ∈ (topGen‘ran (,))
→ 𝐼 ⊆ ∪ (topGen‘ran (,))) |
| 11 | | uniretop 24783 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 12 | 10, 11 | sseqtrrdi 4025 |
. . . . . . . 8
⊢ (𝐼 ∈ (topGen‘ran (,))
→ 𝐼 ⊆
ℝ) |
| 13 | 4, 12 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ⊆ ℝ) |
| 14 | 13, 5 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 15 | | rpre 13043 |
. . . . . 6
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
| 16 | 1 | bl2ioo 24813 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 17 | 14, 15, 16 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 18 | 17 | sseq1d 4015 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼 ↔ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) |
| 19 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ℝ) |
| 20 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ+) |
| 21 | 20 | rpred 13077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝑟 ∈ ℝ) |
| 22 | 19, 21 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 − 𝑟) ∈ ℝ) |
| 23 | 22 | rexrd 11311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 − 𝑟) ∈
ℝ*) |
| 24 | 19, 20 | ltsubrpd 13109 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 − 𝑟) < 𝐵) |
| 25 | | lhop.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
| 26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℝ) |
| 27 | | ssun1 4178 |
. . . . . . . . . . . 12
⊢ ((𝐵 − 𝑟)(,)𝐵) ⊆ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) |
| 28 | | unass 4172 |
. . . . . . . . . . . . . . 15
⊢ (({𝐵} ∪ ((𝐵 − 𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ({𝐵} ∪ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) |
| 29 | | uncom 4158 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐵} ∪ ((𝐵 − 𝑟)(,)𝐵)) = (((𝐵 − 𝑟)(,)𝐵) ∪ {𝐵}) |
| 30 | 29 | uneq1i 4164 |
. . . . . . . . . . . . . . 15
⊢ (({𝐵} ∪ ((𝐵 − 𝑟)(,)𝐵)) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((((𝐵 − 𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) |
| 31 | 28, 30 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
⊢ ({𝐵} ∪ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵 − 𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) |
| 32 | 19 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈
ℝ*) |
| 33 | 19, 21 | readdcld 11290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈ ℝ) |
| 34 | 33 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 + 𝑟) ∈
ℝ*) |
| 35 | 19, 20 | ltaddrpd 13110 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 < (𝐵 + 𝑟)) |
| 36 | | ioojoin 13523 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 − 𝑟) ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ (𝐵 + 𝑟) ∈ ℝ*)
∧ ((𝐵 − 𝑟) < 𝐵 ∧ 𝐵 < (𝐵 + 𝑟))) → ((((𝐵 − 𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 37 | 23, 32, 34, 24, 35, 36 | syl32anc 1380 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵 − 𝑟)(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)(𝐵 + 𝑟))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 38 | 31, 37 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ({𝐵} ∪ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 39 | | elioo2 13428 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 − 𝑟) ∈ ℝ* ∧ (𝐵 + 𝑟) ∈ ℝ*) → (𝐵 ∈ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵 − 𝑟) < 𝐵 ∧ 𝐵 < (𝐵 + 𝑟)))) |
| 40 | 23, 34, 39 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵 ∈ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ↔ (𝐵 ∈ ℝ ∧ (𝐵 − 𝑟) < 𝐵 ∧ 𝐵 < (𝐵 + 𝑟)))) |
| 41 | 19, 24, 35, 40 | mpbir3and 1343 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 42 | 41 | snssd 4809 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 43 | | incom 4209 |
. . . . . . . . . . . . . . 15
⊢ ({𝐵} ∩ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) |
| 44 | | ubioo 13419 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
𝐵 ∈ ((𝐵 − 𝑟)(,)𝐵) |
| 45 | | lbioo 13418 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
𝐵 ∈ (𝐵(,)(𝐵 + 𝑟)) |
| 46 | 44, 45 | pm3.2ni 881 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
(𝐵 ∈ ((𝐵 − 𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟))) |
| 47 | | elun 4153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ↔ (𝐵 ∈ ((𝐵 − 𝑟)(,)𝐵) ∨ 𝐵 ∈ (𝐵(,)(𝐵 + 𝑟)))) |
| 48 | 46, 47 | mtbir 323 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝐵 ∈ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) |
| 49 | | disjsn 4711 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) |
| 50 | 48, 49 | mpbir 231 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) ∩ {𝐵}) = ∅ |
| 51 | 43, 50 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ ({𝐵} ∩ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅ |
| 52 | | uneqdifeq 4493 |
. . . . . . . . . . . . . 14
⊢ (({𝐵} ⊆ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∧ ({𝐵} ∩ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ∅) → (({𝐵} ∪ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))) |
| 53 | 42, 51, 52 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (({𝐵} ∪ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))))) |
| 54 | 38, 53 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) = (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))) |
| 55 | 27, 54 | sseqtrrid 4027 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) |
| 56 | | ssdif 4144 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼 → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵})) |
| 57 | 56 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ (𝐼 ∖ {𝐵})) |
| 58 | | lhop.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝐼 ∖ {𝐵}) |
| 59 | 57, 58 | sseqtrrdi 4025 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐷) |
| 60 | | lhop.if |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ⊆ dom (ℝ D 𝐹)) |
| 61 | | ax-resscn 11212 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℂ |
| 62 | 61 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 63 | | fss 6752 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
| 64 | 25, 61, 63 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
| 65 | | lhop.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 66 | 62, 64, 65 | dvbss 25936 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ 𝐴) |
| 67 | 60, 66 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ 𝐴) |
| 69 | 59, 68 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ⊆ 𝐴) |
| 70 | 55, 69 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ 𝐴) |
| 71 | 26, 70 | fssresd 6775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)):((𝐵 − 𝑟)(,)𝐵)⟶ℝ) |
| 72 | | lhop.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
| 73 | 72 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℝ) |
| 74 | 73, 70 | fssresd 6775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)):((𝐵 − 𝑟)(,)𝐵)⟶ℝ) |
| 75 | 61 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ℝ ⊆
ℂ) |
| 76 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐹:𝐴⟶ℂ) |
| 77 | 65 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐴 ⊆ ℝ) |
| 78 | | ioossre 13448 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 − 𝑟)(,)𝐵) ⊆ ℝ |
| 79 | 78 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ ℝ) |
| 80 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 81 | | tgioo4 24826 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 82 | 80, 81 | dvres 25946 |
. . . . . . . . . . . . 13
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵 − 𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘((𝐵 −
𝑟)(,)𝐵)))) |
| 83 | 75, 76, 77, 79, 82 | syl22anc 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 (,)))‘((𝐵 − 𝑟)(,)𝐵)) = ((𝐵 − 𝑟)(,)𝐵)) |
| 87 | 84, 85, 86 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
((int‘(topGen‘ran (,)))‘((𝐵 − 𝑟)(,)𝐵)) = ((𝐵 − 𝑟)(,)𝐵) |
| 88 | 87 | reseq2i 5994 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐹) ↾
((int‘(topGen‘ran (,)))‘((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵)) |
| 89 | 83, 88 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵))) |
| 90 | 89 | dmeqd 5916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))) = dom ((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵))) |
| 91 | 55, 59 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ 𝐷) |
| 92 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐹)) |
| 93 | 91, 92 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹)) |
| 94 | | ssdmres 6031 |
. . . . . . . . . . 11
⊢ (((𝐵 − 𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵)) = ((𝐵 − 𝑟)(,)𝐵)) |
| 95 | 93, 94 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵)) = ((𝐵 − 𝑟)(,)𝐵)) |
| 96 | 90, 95 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((𝐵 − 𝑟)(,)𝐵)) |
| 97 | | fss 6752 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:𝐴⟶ℂ) |
| 98 | 72, 61, 97 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝐴⟶ℂ) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐺:𝐴⟶ℂ) |
| 100 | 80, 81 | dvres 25946 |
. . . . . . . . . . . . 13
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ ((𝐵 − 𝑟)(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘((𝐵 −
𝑟)(,)𝐵)))) |
| 101 | 75, 99, 77, 79, 100 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘((𝐵 −
𝑟)(,)𝐵)))) |
| 102 | 87 | reseq2i 5994 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐺) ↾
((int‘(topGen‘ran (,)))‘((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵)) |
| 103 | 101, 102 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵))) |
| 104 | 103 | dmeqd 5916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = dom ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵))) |
| 105 | | lhop.ig |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ⊆ dom (ℝ D 𝐺)) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ dom (ℝ D 𝐺)) |
| 107 | 91, 106 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺)) |
| 108 | | ssdmres 6031 |
. . . . . . . . . . 11
⊢ (((𝐵 − 𝑟)(,)𝐵) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵)) = ((𝐵 − 𝑟)(,)𝐵)) |
| 109 | 107, 108 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵)) = ((𝐵 − 𝑟)(,)𝐵)) |
| 110 | 104, 109 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((𝐵 − 𝑟)(,)𝐵)) |
| 111 | | limcresi 25920 |
. . . . . . . . . 10
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) |
| 112 | | lhop.f0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐵)) |
| 113 | 112 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐹 limℂ 𝐵)) |
| 114 | 111, 113 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵)) |
| 115 | | limcresi 25920 |
. . . . . . . . . 10
⊢ (𝐺 limℂ 𝐵) ⊆ ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) |
| 116 | | lhop.g0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐵)) |
| 117 | 116 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ (𝐺 limℂ 𝐵)) |
| 118 | 115, 117 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵)) |
| 119 | | df-ima 5698 |
. . . . . . . . . . 11
⊢ (𝐺 “ ((𝐵 − 𝑟)(,)𝐵)) = ran (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)) |
| 120 | | imass2 6120 |
. . . . . . . . . . . 12
⊢ (((𝐵 − 𝑟)(,)𝐵) ⊆ 𝐷 → (𝐺 “ ((𝐵 − 𝑟)(,)𝐵)) ⊆ (𝐺 “ 𝐷)) |
| 121 | 91, 120 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ ((𝐵 − 𝑟)(,)𝐵)) ⊆ (𝐺 “ 𝐷)) |
| 122 | 119, 121 | eqsstrrid 4023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)) ⊆ (𝐺 “ 𝐷)) |
| 123 | | lhop.gn0 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ 𝐷)) |
| 124 | 123 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ (𝐺 “ 𝐷)) |
| 125 | 122, 124 | ssneldd 3986 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) |
| 126 | 103 | rneqd 5949 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ran ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵))) |
| 127 | | df-ima 5698 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐺) “ ((𝐵 − 𝑟)(,)𝐵)) = ran ((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵)) |
| 128 | 126, 127 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) = ((ℝ D 𝐺) “ ((𝐵 − 𝑟)(,)𝐵))) |
| 129 | | imass2 6120 |
. . . . . . . . . . . 12
⊢ (((𝐵 − 𝑟)(,)𝐵) ⊆ 𝐷 → ((ℝ D 𝐺) “ ((𝐵 − 𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷)) |
| 130 | 91, 129 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ ((𝐵 − 𝑟)(,)𝐵)) ⊆ ((ℝ D 𝐺) “ 𝐷)) |
| 131 | 128, 130 | eqsstrd 4018 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))) ⊆ ((ℝ D 𝐺) “ 𝐷)) |
| 132 | | lhop.gd0 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 0 ∈ ((ℝ D
𝐺) “ 𝐷)) |
| 133 | 132 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ((ℝ D 𝐺) “ 𝐷)) |
| 134 | 131, 133 | ssneldd 3986 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D
(𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))) |
| 135 | | limcresi 25920 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵) ⊆ (((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) |
| 136 | 91 | resmptd 6058 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))) |
| 137 | 89 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧)) |
| 138 | | fvres 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) → (((ℝ D 𝐹) ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐹)‘𝑧)) |
| 139 | 137, 138 | sylan9eq 2797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐹)‘𝑧)) |
| 140 | 103 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) = (((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧)) |
| 141 | | fvres 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) → (((ℝ D 𝐺) ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) = ((ℝ D 𝐺)‘𝑧)) |
| 142 | 140, 141 | sylan9eq 2797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵)) → ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) = ((ℝ D 𝐺)‘𝑧)) |
| 143 | 139, 142 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) |
| 144 | 143 | mpteq2dva 5242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧))) = (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))) |
| 145 | 136, 144 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧)))) |
| 146 | 145 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧))) limℂ 𝐵)) |
| 147 | 135, 146 | sseqtrid 4026 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵) ⊆ ((𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧))) limℂ 𝐵)) |
| 148 | | lhop.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵)) |
| 149 | 148 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵)) |
| 150 | 147, 149 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧) / ((ℝ D (𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵)))‘𝑧))) limℂ 𝐵)) |
| 151 | 23, 19, 24, 71, 74, 96, 110, 114, 118, 125, 134, 150 | lhop2 26054 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧))) limℂ 𝐵)) |
| 152 | 55 | resmptd 6058 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
| 153 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) → ((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) = (𝐹‘𝑧)) |
| 154 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) → ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) = (𝐺‘𝑧)) |
| 155 | 153, 154 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) → (((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧)) = ((𝐹‘𝑧) / (𝐺‘𝑧))) |
| 156 | 155 | mpteq2ia 5245 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧))) = (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) |
| 157 | 152, 156 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) = (𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧)))) |
| 158 | 157 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ ((𝐵 − 𝑟)(,)𝐵) ↦ (((𝐹 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧) / ((𝐺 ↾ ((𝐵 − 𝑟)(,)𝐵))‘𝑧))) limℂ 𝐵)) |
| 159 | 151, 158 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵)) |
| 160 | | ssun2 4179 |
. . . . . . . . . . . 12
⊢ (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟))) |
| 161 | 160, 54 | sseqtrrid 4027 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) |
| 162 | 161, 69 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐴) |
| 163 | 26, 162 | fssresd 6775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ) |
| 164 | 73, 162 | fssresd 6775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))):(𝐵(,)(𝐵 + 𝑟))⟶ℝ) |
| 165 | | ioossre 13448 |
. . . . . . . . . . . . . 14
⊢ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ |
| 166 | 165 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ) |
| 167 | 80, 81 | dvres 25946 |
. . . . . . . . . . . . 13
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵(,)(𝐵 + 𝑟))))) |
| 168 | 75, 76, 77, 166, 167 | syl22anc 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 (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))) |
| 171 | 84, 169, 170 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟)) |
| 172 | 171 | reseq2i 5994 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐹) ↾
((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) |
| 173 | 168, 172 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))) |
| 174 | 173 | dmeqd 5916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))) |
| 175 | 161, 59 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷) |
| 176 | 175, 92 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹)) |
| 177 | | ssdmres 6031 |
. . . . . . . . . . 11
⊢ ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))) |
| 178 | 176, 177 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))) |
| 179 | 174, 178 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟))) |
| 180 | 80, 81 | dvres 25946 |
. . . . . . . . . . . . 13
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:𝐴⟶ℂ) ∧ (𝐴 ⊆ ℝ ∧ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵(,)(𝐵 + 𝑟))))) |
| 181 | 75, 99, 77, 166, 180 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵(,)(𝐵 + 𝑟))))) |
| 182 | 171 | reseq2i 5994 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐺) ↾
((int‘(topGen‘ran (,)))‘(𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) |
| 183 | 181, 182 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))) |
| 184 | 183 | dmeqd 5916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))) |
| 185 | 175, 106 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺)) |
| 186 | | ssdmres 6031 |
. . . . . . . . . . 11
⊢ ((𝐵(,)(𝐵 + 𝑟)) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))) |
| 187 | 185, 186 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝐵(,)(𝐵 + 𝑟))) |
| 188 | 184, 187 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → dom (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = (𝐵(,)(𝐵 + 𝑟))) |
| 189 | | limcresi 25920 |
. . . . . . . . . 10
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵) |
| 190 | 189, 113 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵)) |
| 191 | | limcresi 25920 |
. . . . . . . . . 10
⊢ (𝐺 limℂ 𝐵) ⊆ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵) |
| 192 | 191, 117 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 0 ∈ ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵)) |
| 193 | | df-ima 5698 |
. . . . . . . . . . 11
⊢ (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) = ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) |
| 194 | | imass2 6120 |
. . . . . . . . . . . 12
⊢ ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺 “ 𝐷)) |
| 195 | 175, 194 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐺 “ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺 “ 𝐷)) |
| 196 | 193, 195 | eqsstrrid 4023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))) ⊆ (𝐺 “ 𝐷)) |
| 197 | 196, 124 | ssneldd 3986 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) |
| 198 | 183 | rneqd 5949 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))) |
| 199 | | df-ima 5698 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) = ran ((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟))) |
| 200 | 198, 199 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) = ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟)))) |
| 201 | | imass2 6120 |
. . . . . . . . . . . 12
⊢ ((𝐵(,)(𝐵 + 𝑟)) ⊆ 𝐷 → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷)) |
| 202 | 175, 201 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D 𝐺) “ (𝐵(,)(𝐵 + 𝑟))) ⊆ ((ℝ D 𝐺) “ 𝐷)) |
| 203 | 200, 202 | eqsstrd 4018 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ran (ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))) ⊆ ((ℝ D 𝐺) “ 𝐷)) |
| 204 | 203, 133 | ssneldd 3986 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ¬ 0 ∈ ran (ℝ D
(𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))) |
| 205 | | limcresi 25920 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵) ⊆ (((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵) |
| 206 | 175 | resmptd 6058 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))) |
| 207 | 173 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)) |
| 208 | | fvres 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐹) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐹)‘𝑧)) |
| 209 | 207, 208 | sylan9eq 2797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐹)‘𝑧)) |
| 210 | 183 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)) |
| 211 | | fvres 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((ℝ D 𝐺) ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = ((ℝ D 𝐺)‘𝑧)) |
| 212 | 210, 211 | sylan9eq 2797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) = ((ℝ D 𝐺)‘𝑧)) |
| 213 | 209, 212 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (𝐵(,)(𝐵 + 𝑟))) → (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧)) = (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) |
| 214 | 213 | mpteq2dva 5242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))) |
| 215 | 206, 214 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧)))) |
| 216 | 215 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) limℂ 𝐵)) |
| 217 | 205, 216 | sseqtrid 4026 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵) ⊆ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) limℂ 𝐵)) |
| 218 | 217, 149 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((ℝ D (𝐹 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧) / ((ℝ D (𝐺 ↾ (𝐵(,)(𝐵 + 𝑟))))‘𝑧))) limℂ 𝐵)) |
| 219 | 19, 34, 35, 163, 164, 179, 188, 190, 192, 197, 204, 218 | lhop1 26053 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) limℂ 𝐵)) |
| 220 | 161 | resmptd 6058 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
| 221 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐹‘𝑧)) |
| 222 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) = (𝐺‘𝑧)) |
| 223 | 221, 222 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) → (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)) = ((𝐹‘𝑧) / (𝐺‘𝑧))) |
| 224 | 223 | mpteq2ia 5245 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) |
| 225 | 220, 224 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) = (𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧)))) |
| 226 | 225 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵) = ((𝑧 ∈ (𝐵(,)(𝐵 + 𝑟)) ↦ (((𝐹 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧) / ((𝐺 ↾ (𝐵(,)(𝐵 + 𝑟)))‘𝑧))) limℂ 𝐵)) |
| 227 | 219, 226 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵)) |
| 228 | 159, 227 | elind 4200 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) ∩ (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵))) |
| 229 | 59 | resmptd 6058 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) = (𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
| 230 | 229 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) limℂ 𝐵) = ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 231 | 67 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ 𝐴) |
| 232 | 25 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ) |
| 233 | 231, 232 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐹‘𝑧) ∈ ℝ) |
| 234 | 233 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐹‘𝑧) ∈ ℂ) |
| 235 | 72 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ) |
| 236 | 231, 235 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐺‘𝑧) ∈ ℝ) |
| 237 | 236 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐺‘𝑧) ∈ ℂ) |
| 238 | 123 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ¬ 0 ∈ (𝐺 “ 𝐷)) |
| 239 | 72 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 Fn 𝐴) |
| 240 | 239 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐺 Fn 𝐴) |
| 241 | 67 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐷 ⊆ 𝐴) |
| 242 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ 𝐷) |
| 243 | | fnfvima 7253 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 Fn 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐷) → (𝐺‘𝑧) ∈ (𝐺 “ 𝐷)) |
| 244 | 240, 241,
242, 243 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐺‘𝑧) ∈ (𝐺 “ 𝐷)) |
| 245 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝑧) = 0 → ((𝐺‘𝑧) ∈ (𝐺 “ 𝐷) ↔ 0 ∈ (𝐺 “ 𝐷))) |
| 246 | 244, 245 | syl5ibcom 245 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ((𝐺‘𝑧) = 0 → 0 ∈ (𝐺 “ 𝐷))) |
| 247 | 246 | necon3bd 2954 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (¬ 0 ∈ (𝐺 “ 𝐷) → (𝐺‘𝑧) ≠ 0)) |
| 248 | 238, 247 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐺‘𝑧) ≠ 0) |
| 249 | 234, 237,
248 | divcld 12043 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ) |
| 250 | 249 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ 𝐷) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ) |
| 251 | 250 | fmpttd 7135 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):𝐷⟶ℂ) |
| 252 | | difss 4136 |
. . . . . . . . . . 11
⊢ (𝐼 ∖ {𝐵}) ⊆ 𝐼 |
| 253 | 58, 252 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝐷 ⊆ 𝐼 |
| 254 | 13, 61 | sstrdi 3996 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ⊆ ℂ) |
| 255 | 253, 254 | sstrid 3995 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
| 256 | 255 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐷 ⊆ ℂ) |
| 257 | | eqid 2737 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t (𝐷
∪ {𝐵})) |
| 258 | 58 | uneq1i 4164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∪ {𝐵}) = ((𝐼 ∖ {𝐵}) ∪ {𝐵}) |
| 259 | | undif1 4476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∖ {𝐵}) ∪ {𝐵}) = (𝐼 ∪ {𝐵}) |
| 260 | 258, 259 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∪ {𝐵}) = (𝐼 ∪ {𝐵}) |
| 261 | | simprr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼) |
| 262 | 42, 261 | sstrd 3994 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → {𝐵} ⊆ 𝐼) |
| 263 | | ssequn2 4189 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐵} ⊆ 𝐼 ↔ (𝐼 ∪ {𝐵}) = 𝐼) |
| 264 | 262, 263 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐼 ∪ {𝐵}) = 𝐼) |
| 265 | 260, 264 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐷 ∪ {𝐵}) = 𝐼) |
| 266 | 265 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t 𝐼)) |
| 267 | 13 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℝ) |
| 268 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 269 | 80, 268 | rerest 24825 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ⊆ ℝ →
((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,))
↾t 𝐼)) |
| 270 | 267, 269 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((TopOpen‘ℂfld) ↾t 𝐼) = ((topGen‘ran (,))
↾t 𝐼)) |
| 271 | 266, 270 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})) = ((topGen‘ran (,))
↾t 𝐼)) |
| 272 | 271 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
(int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵}))) = (int‘((topGen‘ran (,))
↾t 𝐼))) |
| 273 | 272 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) = ((int‘((topGen‘ran (,))
↾t 𝐼))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟)))) |
| 274 | 80 | cnfldtopon 24803 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 275 | 254 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ⊆ ℂ) |
| 276 | | resttopon 23169 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝐼 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼)) |
| 277 | 274, 275,
276 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼)) |
| 278 | | topontop 22919 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ↾t 𝐼) ∈ (TopOn‘𝐼) →
((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top) |
| 279 | 277, 278 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((TopOpen‘ℂfld) ↾t 𝐼) ∈ Top) |
| 280 | 270, 279 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((topGen‘ran (,))
↾t 𝐼)
∈ Top) |
| 281 | | iooretop 24786 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran
(,)) |
| 282 | 281 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran
(,))) |
| 283 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐼 ∈ (topGen‘ran
(,))) |
| 284 | | restopn2 23185 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐼 ∈ (topGen‘ran (,))) →
(((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,))
↾t 𝐼)
↔ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧
((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼))) |
| 285 | 84, 283, 284 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,))
↾t 𝐼)
↔ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ (topGen‘ran (,)) ∧
((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼))) |
| 286 | 282, 261,
285 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,))
↾t 𝐼)) |
| 287 | | isopn3i 23090 |
. . . . . . . . . . . 12
⊢
((((topGen‘ran (,)) ↾t 𝐼) ∈ Top ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∈ ((topGen‘ran (,))
↾t 𝐼))
→ ((int‘((topGen‘ran (,)) ↾t 𝐼))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 288 | 280, 286,
287 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((int‘((topGen‘ran
(,)) ↾t 𝐼))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 289 | 273, 288 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 290 | 41, 289 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟)))) |
| 291 | | undif1 4476 |
. . . . . . . . . . 11
⊢ ((((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) |
| 292 | | ssequn2 4189 |
. . . . . . . . . . . 12
⊢ ({𝐵} ⊆ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ↔ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 293 | 42, 292 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∪ {𝐵}) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 294 | 291, 293 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}) = ((𝐵 − 𝑟)(,)(𝐵 + 𝑟))) |
| 295 | 294 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) →
((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵})) =
((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((𝐵 − 𝑟)(,)(𝐵 + 𝑟)))) |
| 296 | 290, 295 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐷 ∪ {𝐵})))‘((((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ∪ {𝐵}))) |
| 297 | 251, 59, 256, 80, 257, 296 | limcres 25921 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) limℂ 𝐵) = ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 298 | 78, 61 | sstri 3993 |
. . . . . . . . 9
⊢ ((𝐵 − 𝑟)(,)𝐵) ⊆ ℂ |
| 299 | 298 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝐵 − 𝑟)(,)𝐵) ⊆ ℂ) |
| 300 | 165, 61 | sstri 3993 |
. . . . . . . . 9
⊢ (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ |
| 301 | 300 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝐵(,)(𝐵 + 𝑟)) ⊆ ℂ) |
| 302 | 59 | sselda 3983 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → 𝑧 ∈ 𝐷) |
| 303 | 302, 250 | syldan 591 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) ∧ 𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ) |
| 304 | 303 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ) |
| 305 | 54 | feq2d 6722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵})⟶ℂ ↔ (𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ)) |
| 306 | 304, 305 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → (𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(((𝐵 − 𝑟)(,)𝐵) ∪ (𝐵(,)(𝐵 + 𝑟)))⟶ℂ) |
| 307 | 299, 301,
306 | limcun 25930 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵) = ((((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) ∩ (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵))) |
| 308 | 230, 297,
307 | 3eqtr3rd 2786 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → ((((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ ((𝐵 − 𝑟)(,)𝐵)) limℂ 𝐵) ∩ (((𝑧 ∈ (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ∖ {𝐵}) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝐵(,)(𝐵 + 𝑟))) limℂ 𝐵)) = ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 309 | 228, 308 | eleqtrd 2843 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ ((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼)) → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 310 | 309 | expr 456 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝐵 − 𝑟)(,)(𝐵 + 𝑟)) ⊆ 𝐼 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵))) |
| 311 | 18, 310 | sylbid 240 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵))) |
| 312 | 311 | rexlimdva 3155 |
. 2
⊢ (𝜑 → (∃𝑟 ∈ ℝ+ (𝐵(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐼 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵))) |
| 313 | 9, 312 | mpd 15 |
1
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ 𝐷 ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |