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

Theorem lhop1lem 23990
Description: Lemma for lhop1 23991. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
lhop1.a (𝜑𝐴 ∈ ℝ)
lhop1.b (𝜑𝐵 ∈ ℝ*)
lhop1.l (𝜑𝐴 < 𝐵)
lhop1.f (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
lhop1.g (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
lhop1.if (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
lhop1.ig (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
lhop1.f0 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
lhop1.g0 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
lhop1.gn0 (𝜑 → ¬ 0 ∈ ran 𝐺)
lhop1.gd0 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
lhop1.c (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
lhop1lem.e (𝜑𝐸 ∈ ℝ+)
lhop1lem.d (𝜑𝐷 ∈ ℝ)
lhop1lem.db (𝜑𝐷𝐵)
lhop1lem.x (𝜑𝑋 ∈ (𝐴(,)𝐷))
lhop1lem.t (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
lhop1lem.r 𝑅 = (𝐴 + (𝑟 / 2))
Assertion
Ref Expression
lhop1lem (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) < (2 · 𝐸))
Distinct variable groups:   𝑧,𝑟,𝐵   𝑡,𝐷   𝜑,𝑟,𝑧   𝑧,𝑅   𝑡,𝑟,𝐴,𝑧   𝐸,𝑟,𝑡   𝑋,𝑟,𝑧   𝐶,𝑟,𝑡,𝑧   𝐹,𝑟,𝑡,𝑧   𝐺,𝑟,𝑡,𝑧
Allowed substitution hints:   𝜑(𝑡)   𝐵(𝑡)   𝐷(𝑧,𝑟)   𝑅(𝑡,𝑟)   𝐸(𝑧)   𝑋(𝑡)

Proof of Theorem lhop1lem
Dummy variables 𝑣 𝑥 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lhop1.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2 lhop1.b . . . . . . . . 9 (𝜑𝐵 ∈ ℝ*)
3 lhop1lem.db . . . . . . . . 9 (𝜑𝐷𝐵)
4 iooss2 12429 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐷𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
52, 3, 4syl2anc 575 . . . . . . . 8 (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
6 lhop1lem.x . . . . . . . 8 (𝜑𝑋 ∈ (𝐴(,)𝐷))
75, 6sseldd 3799 . . . . . . 7 (𝜑𝑋 ∈ (𝐴(,)𝐵))
81, 7ffvelrnd 6582 . . . . . 6 (𝜑 → (𝐹𝑋) ∈ ℝ)
98recnd 10353 . . . . 5 (𝜑 → (𝐹𝑋) ∈ ℂ)
10 lhop1.g . . . . . . 7 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
1110, 7ffvelrnd 6582 . . . . . 6 (𝜑 → (𝐺𝑋) ∈ ℝ)
1211recnd 10353 . . . . 5 (𝜑 → (𝐺𝑋) ∈ ℂ)
13 lhop1.gn0 . . . . . 6 (𝜑 → ¬ 0 ∈ ran 𝐺)
1410ffnd 6257 . . . . . . . . 9 (𝜑𝐺 Fn (𝐴(,)𝐵))
15 fnfvelrn 6578 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺𝑋) ∈ ran 𝐺)
1614, 7, 15syl2anc 575 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ran 𝐺)
17 eleq1 2873 . . . . . . . 8 ((𝐺𝑋) = 0 → ((𝐺𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
1816, 17syl5ibcom 236 . . . . . . 7 (𝜑 → ((𝐺𝑋) = 0 → 0 ∈ ran 𝐺))
1918necon3bd 2992 . . . . . 6 (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺𝑋) ≠ 0))
2013, 19mpd 15 . . . . 5 (𝜑 → (𝐺𝑋) ≠ 0)
219, 12, 20divcld 11086 . . . 4 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ)
22 limccl 23853 . . . . 5 ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) ⊆ ℂ
23 lhop1.c . . . . 5 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
2422, 23sseldi 3796 . . . 4 (𝜑𝐶 ∈ ℂ)
2521, 24subcld 10677 . . 3 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) − 𝐶) ∈ ℂ)
2625abscld 14398 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ∈ ℝ)
27 lhop1lem.e . . 3 (𝜑𝐸 ∈ ℝ+)
2827rpred 12086 . 2 (𝜑𝐸 ∈ ℝ)
29 2re 11374 . . . 4 2 ∈ ℝ
3029a1i 11 . . 3 (𝜑 → 2 ∈ ℝ)
3130, 28remulcld 10355 . 2 (𝜑 → (2 · 𝐸) ∈ ℝ)
32 cnxmet 22789 . . . . . . . . . . . . 13 (abs ∘ − ) ∈ (∞Met‘ℂ)
3332a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
34 simprl 778 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝑣 ∈ (TopOpen‘ℂfld))
35 simprr 780 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝐴𝑣)
36 eliooord 12451 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋𝑋 < 𝐷))
376, 36syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < 𝑋𝑋 < 𝐷))
3837simpld 484 . . . . . . . . . . . . . 14 (𝜑𝐴 < 𝑋)
39 lhop1.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
40 ioossre 12453 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐷) ⊆ ℝ
4140, 6sseldi 3796 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
42 difrp 12082 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4339, 41, 42syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4438, 43mpbid 223 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐴) ∈ ℝ+)
4544adantr 468 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (𝑋𝐴) ∈ ℝ+)
46 eqid 2806 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4746cnfldtopn 22798 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
4847mopni3 22512 . . . . . . . . . . . 12 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣) ∧ (𝑋𝐴) ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
4933, 34, 35, 45, 48syl31anc 1485 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
50 lhop1lem.r . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 = (𝐴 + (𝑟 / 2))
5139adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ)
52 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ+)
5352rpred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ)
5453rehalfcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
5551, 54readdcld 10354 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ)
5650, 55syl5eqel 2889 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ)
5756recnd 10353 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℂ)
5839recnd 10353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℂ)
5958adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℂ)
60 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
6160cnmetdval 22787 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
6257, 59, 61syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
6350oveq1i 6884 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴)
6453recnd 10353 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℂ)
6564halfcld 11544 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℂ)
6659, 65pncan2d 10679 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2))
6763, 66syl5eq 2852 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅𝐴) = (𝑟 / 2))
6867fveq2d 6412 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑅𝐴)) = (abs‘(𝑟 / 2)))
6952rphalfcld 12098 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ+)
7069rpred 12086 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
7169rpge0d 12090 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 0 ≤ (𝑟 / 2))
7270, 71absidd 14384 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
7362, 68, 723eqtrd 2844 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2))
74 rphalflt 12074 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+ → (𝑟 / 2) < 𝑟)
7552, 74syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < 𝑟)
7673, 75eqbrtrd 4866 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟)
7732a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
7853rexrd 10374 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ*)
79 elbl3 22410 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8077, 78, 59, 57, 79syl22anc 858 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8176, 80mpbird 248 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟))
8251, 69ltaddrpd 12119 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2)))
8382, 50syl6breqr 4886 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < 𝑅)
8441adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ)
8584, 51resubcld 10743 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑋𝐴) ∈ ℝ)
86 simprr 780 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 < (𝑋𝐴))
8770, 53, 85, 75, 86lttrd 10483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < (𝑋𝐴))
8851, 70, 84ltaddsub2d 10913 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋𝐴)))
8987, 88mpbird 248 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋)
9050, 89syl5eqbr 4879 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 < 𝑋)
9151rexrd 10374 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ*)
9241rexrd 10374 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
9392adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ*)
94 elioo2 12434 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝑋 ∈ ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
9591, 93, 94syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
9656, 83, 90, 95mpbir3and 1435 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝑋))
9781, 96elind 3997 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)))
989adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑋) ∈ ℂ)
991adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
100 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ∈ ℝ)
101100rexrd 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℝ*)
10237simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋 < 𝐷)
10341, 100, 102ltled 10470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑋𝐷)
10492, 101, 2, 103, 3xrletrd 12211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
105 iooss2 12429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ ℝ*𝑋𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
1062, 104, 105syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
107106adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
108107, 96sseldd 3799 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝐵))
10999, 108ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℝ)
110109recnd 10353 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℂ)
11198, 110subcld 10677 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
11212adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑋) ∈ ℂ)
11310adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
114113, 108ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℝ)
115114recnd 10353 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℂ)
116112, 115subcld 10677 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
117 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑅 → (𝐺𝑧) = (𝐺𝑅))
118117oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑅 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑅)))
119118neeq1d 3037 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑅 → (((𝐺𝑋) − (𝐺𝑧)) ≠ 0 ↔ ((𝐺𝑋) − (𝐺𝑅)) ≠ 0))
120 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
121120adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
12212adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑋) ∈ ℂ)
123106sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵))
12410ffvelrnda 6581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℝ)
125123, 124syldan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℝ)
126125recnd 10353 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℂ)
127122, 126subeq0ad 10687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 ↔ (𝐺𝑋) = (𝐺𝑧)))
128 ioossre 12453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴(,)𝐵) ⊆ ℝ
129128, 123sseldi 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ)
130129adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 ∈ ℝ)
13141ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑋 ∈ ℝ)
132 eliooord 12451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧𝑧 < 𝑋))
133132adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧𝑧 < 𝑋))
134133simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋)
135134adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 < 𝑋)
13639rexrd 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐴 ∈ ℝ*)
137136adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈ ℝ*)
1382adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈ ℝ*)
139133simpld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧)
14092, 101, 2, 102, 3xrltletrd 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑋 < 𝐵)
141140adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵)
142 iccssioo 12460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝑧𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
143137, 138, 139, 141, 142syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
144143adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
145 ax-resscn 10278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℝ ⊆ ℂ
146145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ℝ ⊆ ℂ)
147 fss 6269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
14810, 145, 147sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
149128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
150 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
151 dvcn 23898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
152146, 148, 149, 150, 151syl31anc 1485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
153 cncffvrn 22914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ℝ ⊆ ℂ ∧ 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
154145, 152, 153sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
15510, 154mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
156155ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
157 rescncf 22913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)))
158144, 156, 157sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))
159145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ℝ ⊆ ℂ)
160148ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
161128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐴(,)𝐵) ⊆ ℝ)
162144, 128syl6ss 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ ℝ)
16346tgioo2 22819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
16446, 163dvres 23889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
165159, 160, 161, 162, 164syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
166 iccntr 22837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
167130, 131, 166syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
168167reseq2d 5597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
169165, 168eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
170169dmeqd 5527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
171 ioossicc 12477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋)
172171, 144syl5ss 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵))
173150ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
174172, 173sseqtr4d 3839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺))
175 ssdmres 5623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
176174, 175sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
177170, 176eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋))
178129rexrd 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*)
17992adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ*)
18041adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ)
181129, 180, 134ltled 10470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧𝑋)
182 ubicc2 12509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑋 ∈ (𝑧[,]𝑋))
183178, 179, 181, 182syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋))
184 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑋 ∈ (𝑧[,]𝑋) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
185183, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
186 lbicc2 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑧 ∈ (𝑧[,]𝑋))
187178, 179, 181, 186syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋))
188 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (𝑧[,]𝑋) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
189187, 188syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
190185, 189eqeq12d 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺𝑋) = (𝐺𝑧)))
191190biimpar 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧))
192191eqcomd 2812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋))
193130, 131, 135, 158, 177, 192rolle 23967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0)
194169fveq1d 6410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤))
195 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
196194, 195sylan9eq 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
197 dvf 23885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
198150feq2d 6242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
199197, 198mpbii 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
200199ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
201200ffnd 6257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
202201adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
203172sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
204 fnfvelrn 6578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
205202, 203, 204syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
206196, 205eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺))
207 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
208206, 207syl5ibcom 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
209208rexlimdva 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
210193, 209mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 0 ∈ ran (ℝ D 𝐺))
211210ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) = (𝐺𝑧) → 0 ∈ ran (ℝ D 𝐺)))
212127, 211sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺)))
213212necon3bd 2992 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
214121, 213mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
215214ralrimiva 3154 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
216215adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
217119, 216, 96rspcdva 3508 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
218111, 116, 217divcld 11086 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) ∈ ℂ)
21924adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐶 ∈ ℂ)
220218, 219subcld 10677 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶) ∈ ℂ)
221220abscld 14398 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ∈ ℝ)
22228adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐸 ∈ ℝ)
223101adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐷 ∈ ℝ*)
224102adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 < 𝐷)
225 iccssioo 12460 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ*𝐷 ∈ ℝ*) ∧ (𝐴 < 𝑅𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
22691, 223, 83, 224, 225syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
2275adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
228226, 227sstrd 3808 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵))
229 fss 6269 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
2301, 145, 229sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
231 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
232 dvcn 23898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
233146, 230, 149, 231, 232syl31anc 1485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
234 cncffvrn 22914 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
235145, 233, 234sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
2361, 235mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
237236adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
238 rescncf 22913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
239228, 237, 238sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
240155adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
241 rescncf 22913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
242228, 240, 241sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
243145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ℝ ⊆ ℂ)
244230adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
245128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐵) ⊆ ℝ)
246 iccssre 12473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ)
24756, 84, 246syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ ℝ)
24846, 163dvres 23889 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
249243, 244, 245, 247, 248syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
250 iccntr 22837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
25156, 84, 250syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
252251reseq2d 5597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
253249, 252eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
254253dmeqd 5527 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
25551, 56, 83ltled 10470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴𝑅)
256 iooss1 12428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝐴𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
25791, 255, 256syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
258103adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋𝐷)
259 iooss2 12429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐷 ∈ ℝ*𝑋𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
260223, 258, 259syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
261257, 260sstrd 3808 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷))
262261, 227sstrd 3808 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵))
263231adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
264262, 263sseqtr4d 3839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹))
265 ssdmres 5623 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
266264, 265sylib 209 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
267254, 266eqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
268148adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
26946, 163dvres 23889 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
270243, 268, 245, 247, 269syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
271251reseq2d 5597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
272270, 271eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
273272dmeqd 5527 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
274150adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
275262, 274sseqtr4d 3839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺))
276 ssdmres 5623 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
277275, 276sylib 209 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
278273, 277eqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
27956, 84, 90, 239, 242, 267, 278cmvth 23968 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)))
28056rexrd 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ*)
281280adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ ℝ*)
28292ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ ℝ*)
28356, 84, 90ltled 10470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅𝑋)
284283adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅𝑋)
285 ubicc2 12509 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑋 ∈ (𝑅[,]𝑋))
286281, 282, 284, 285syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋))
287 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ (𝑅[,]𝑋) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
288286, 287syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
289 lbicc2 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑅 ∈ (𝑅[,]𝑋))
290281, 282, 284, 289syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋))
291 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 ∈ (𝑅[,]𝑋) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
293288, 292oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹𝑋) − (𝐹𝑅)))
294272fveq1d 6410 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤))
295 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
296294, 295sylan9eq 2860 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
297293, 296oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)))
298 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑋 ∈ (𝑅[,]𝑋) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
299286, 298syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
300 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑅 ∈ (𝑅[,]𝑋) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
301290, 300syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
302299, 301oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺𝑋) − (𝐺𝑅)))
303253fveq1d 6410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤))
304 fvres 6427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
305303, 304sylan9eq 2860 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
306302, 305oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)))
307116adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
308 dvf 23885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
309231feq2d 6242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
310308, 309mpbii 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
311310ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
312262sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
313311, 312ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ)
314307, 313mulcomd 10346 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
315306, 314eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
316297, 315eqeq12d 2821 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
317111adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
318199ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
319318, 312ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ)
320217adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
321120ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
322318ffnd 6257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
323322, 312, 204syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
324 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
325323, 324syl5ibcom 236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
326325necon3bd 2992 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0))
327321, 326mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0)
328317, 307, 313, 319, 320, 327divmuleqd 11132 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
329316, 328bitr4d 273 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
330329rexbidva 3237 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
331279, 330mpbid 223 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
332 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤))
333 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤))
334332, 333oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
335334fvoveq1d 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
336335breq1d 4854 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
337 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
338337ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
339261sselda 3798 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷))
340336, 338, 339rspcdva 3508 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)
341 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
342341breq1d 4854 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
343340, 342syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
344343rexlimdva 3219 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
345331, 344mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸)
346221, 222, 345ltled 10470 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸)
347 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐹𝑢) = (𝐹𝑅))
348347oveq2d 6890 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐹𝑋) − (𝐹𝑢)) = ((𝐹𝑋) − (𝐹𝑅)))
349 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐺𝑢) = (𝐺𝑅))
350349oveq2d 6890 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐺𝑋) − (𝐺𝑢)) = ((𝐺𝑋) − (𝐺𝑅)))
351348, 350oveq12d 6892 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑅 → (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) = (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))))
352351fvoveq1d 6896 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑅 → (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)))
353352breq1d 4854 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑅 → ((abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸))
354353rspcev 3502 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
35597, 346, 354syl2anc 575 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
356355adantlr 697 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
357 ssrin 4034 . . . . . . . . . . . . . . . . 17 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋)))
358 lbioo 12424 . . . . . . . . . . . . . . . . . . . 20 ¬ 𝐴 ∈ (𝐴(,)𝑋)
359 disjsn 4438 . . . . . . . . . . . . . . . . . . . 20 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋))
360358, 359mpbir 222 . . . . . . . . . . . . . . . . . . 19 ((𝐴(,)𝑋) ∩ {𝐴}) = ∅
361 disj3 4218 . . . . . . . . . . . . . . . . . . 19 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}))
362360, 361mpbi 221 . . . . . . . . . . . . . . . . . 18 (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})
363362ineq2i 4010 . . . . . . . . . . . . . . . . 17 (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))
364357, 363syl6sseq 3848 . . . . . . . . . . . . . . . 16 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))
365 ssrexv 3864 . . . . . . . . . . . . . . . 16 (((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
366364, 365syl 17 . . . . . . . . . . . . . . 15 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
367356, 366syl5com 31 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
368367anassrs 455 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
369368expimpd 443 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
370369rexlimdva 3219 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
37149, 370mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
372 inss2 4030 . . . . . . . . . . . . . 14 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴})
373 difss 3936 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋)
374372, 373sstri 3807 . . . . . . . . . . . . 13 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)
375374sseli 3794 . . . . . . . . . . . 12 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋))
376 fveq2 6408 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐹𝑧) = (𝐹𝑢))
377376oveq2d 6890 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐹𝑋) − (𝐹𝑧)) = ((𝐹𝑋) − (𝐹𝑢)))
378 fveq2 6408 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐺𝑧) = (𝐺𝑢))
379378oveq2d 6890 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑢)))
380377, 379oveq12d 6892 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
381 eqid 2806 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))
382 ovex 6906 . . . . . . . . . . . . . . 15 (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) ∈ V
383380, 381, 382fvmpt 6503 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
384383fvoveq1d 6896 . . . . . . . . . . . . 13 (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)))
385384breq1d 4854 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
386375, 385syl 17 . . . . . . . . . . 11 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
387386rexbiia 3228 . . . . . . . . . 10 (∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
388371, 387sylibr 225 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
389 ovex 6906 . . . . . . . . . . 11 (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ V
390389, 381fnmpti 6233 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋)
391 fvoveq1 6897 . . . . . . . . . . . 12 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → (abs‘(𝑥𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)))
392391breq1d 4854 . . . . . . . . . . 11 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
393392rexima 6722 . . . . . . . . . 10 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
394390, 374, 393mp2an 675 . . . . . . . . 9 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
395388, 394sylibr 225 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸)
396 dfrex2 3183 . . . . . . . 8 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
397395, 396sylib 209 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
398 ssrab 3877 . . . . . . . 8 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸))
399398simprbi 486 . . . . . . 7 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
400397, 399nsyl 137 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})
401400expr 446 . . . . 5 ((𝜑𝑣 ∈ (TopOpen‘ℂfld)) → (𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
402401ralrimiva 3154 . . . 4 (𝜑 → ∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
403 ralinexa 3184 . . . 4 (∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
404402, 403sylib 209 . . 3 (𝜑 → ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
405 fvoveq1 6897 . . . . . . . 8 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (abs‘(𝑥𝐶)) = (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)))
406405breq1d 4854 . . . . . . 7 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
407406notbid 309 . . . . . 6 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (¬ (abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
408407elrab3 3560 . . . . 5 (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
40921, 408syl 17 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
410 eleq2 2874 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 ↔ ((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
411 sseq2 3824 . . . . . . . 8 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
412411anbi2d 616 . . . . . . 7 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
413412rexbidv 3240 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
414410, 413imbi12d 335 . . . . 5 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))))
4159adantr 468 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑋) ∈ ℂ)
4161ffvelrnda 6581 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℝ)
417123, 416syldan 581 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℝ)
418417recnd 10353 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℂ)
419415, 418subcld 10677 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑧)) ∈ ℂ)
420122, 126subcld 10677 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ)
421 eldifsn 4508 . . . . . . . . 9 (((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}) ↔ (((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ ∧ ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
422420, 214, 421sylanbrc 574 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}))
423 ssidd 3821 . . . . . . . 8 (𝜑 → ℂ ⊆ ℂ)
424 difss 3936 . . . . . . . . 9 (ℂ ∖ {0}) ⊆ ℂ
425424a1i 11 . . . . . . . 8 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
42646cnfldtopon 22799 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
427 cnex 10302 . . . . . . . . . 10 ℂ ∈ V
428427, 424ssexi 4998 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
429 txrest 21648 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) ∧ (ℂ ∈ V ∧ (ℂ ∖ {0}) ∈ V)) → (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))))
430426, 426, 427, 428, 429mp4an 676 . . . . . . . . 9 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
431426toponunii 20934 . . . . . . . . . . . 12 ℂ = (TopOpen‘ℂfld)
432431restid 16299 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
433426, 432ax-mp 5 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
434433oveq1i 6884 . . . . . . . . 9 (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
435430, 434eqtr2i 2829 . . . . . . . 8 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0})))
4369subid1d 10666 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) = (𝐹𝑋))
437 txtopon 21608 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
438426, 426, 437mp2an 675 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
439438toponrestid 20939 . . . . . . . . . 10 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
440 limcresi 23863 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
441 ioossre 12453 . . . . . . . . . . . . . 14 (𝐴(,)𝑋) ⊆ ℝ
442 resmpt 5654 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)))
443441, 442ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋))
444443oveq1i 6884 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
445440, 444sseqtri 3834 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
446 cncfmptc 22927 . . . . . . . . . . . . 13 (((𝐹𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
4478, 146, 146, 446syl3anc 1483 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
448 eqidd 2807 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐹𝑋) = (𝐹𝑋))
449447, 39, 448cnmptlimc 23868 . . . . . . . . . . 11 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴))
450445, 449sseldi 3796 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴))
451 limcresi 23863 . . . . . . . . . . . 12 (𝐹 lim 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴)
4521, 106feqresmpt 6471 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)))
453452oveq1d 6889 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
454451, 453syl5sseq 3850 . . . . . . . . . . 11 (𝜑 → (𝐹 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
455 lhop1.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
456454, 455sseldd 3799 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
45746subcn 22882 . . . . . . . . . . 11 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
458 0cn 10317 . . . . . . . . . . . 12 0 ∈ ℂ
459 opelxpi 5348 . . . . . . . . . . . 12 (((𝐹𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
4609, 458, 459sylancl 576 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
461438toponunii 20934 . . . . . . . . . . . 12 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
462461cncnpi 21296 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
463457, 460, 462sylancr 577 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
464415, 418, 423, 423, 46, 439, 450, 456, 463limccnp2 23870 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
465436, 464eqeltrrd 2886 . . . . . . . 8 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
46612subid1d 10666 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) = (𝐺𝑋))
467 limcresi 23863 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
468 resmpt 5654 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)))
469441, 468ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋))
470469oveq1i 6884 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
471467, 470sseqtri 3834 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
472 cncfmptc 22927 . . . . . . . . . . . . 13 (((𝐺𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
47311, 146, 146, 472syl3anc 1483 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
474 eqidd 2807 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐺𝑋) = (𝐺𝑋))
475473, 39, 474cnmptlimc 23868 . . . . . . . . . . 11 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴))
476471, 475sseldi 3796 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴))
477 limcresi 23863 . . . . . . . . . . . 12 (𝐺 lim 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴)
47810, 106feqresmpt 6471 . . . . . . . . . . . . 13 (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)))
479478oveq1d 6889 . . . . . . . . . . . 12 (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
480477, 479syl5sseq 3850 . . . . . . . . . . 11 (𝜑 → (𝐺 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
481 lhop1.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
482480, 481sseldd 3799 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
483 opelxpi 5348 . . . . . . . . . . . 12 (((𝐺𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
48412, 458, 483sylancl 576 . . . . . . . . . . 11 (𝜑 → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
485461cncnpi 21296 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
486457, 484, 485sylancr 577 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
487122, 126, 423, 423, 46, 439, 476, 482, 486limccnp2 23870 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
488466, 487eqeltrrd 2886 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
489 eqid 2806 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
49046, 489divcn 22884 . . . . . . . . 9 / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld))
491 eldifsn 4508 . . . . . . . . . . 11 ((𝐺𝑋) ∈ (ℂ ∖ {0}) ↔ ((𝐺𝑋) ∈ ℂ ∧ (𝐺𝑋) ≠ 0))
49212, 20, 491sylanbrc 574 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ (ℂ ∖ {0}))
493 opelxpi 5348 . . . . . . . . . 10 (((𝐹𝑋) ∈ ℂ ∧ (𝐺𝑋) ∈ (ℂ ∖ {0})) → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
4949, 492, 493syl2anc 575 . . . . . . . . 9 (𝜑 → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
495 resttopon 21179 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
496426, 424, 495mp2an 675 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))
497 txtopon 21608 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))) → ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0}))))
498426, 496, 497mp2an 675 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0})))
499498toponunii 20934 . . . . . . . . . 10 (ℂ × (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
500499cncnpi 21296 . . . . . . . . 9 (( / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0}))) → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
501490, 494, 500sylancr 577 . . . . . . . 8 (𝜑 → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
502419, 422, 423, 425, 46, 435, 465, 488, 501limccnp2 23870 . . . . . . 7 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴))
503419, 420, 214divcld 11086 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ ℂ)
504503fmpttd 6607 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))):(𝐴(,)𝑋)⟶ℂ)
505441, 145sstri 3807 . . . . . . . . 9 (𝐴(,)𝑋) ⊆ ℂ
506505a1i 11 . . . . . . . 8 (𝜑 → (𝐴(,)𝑋) ⊆ ℂ)
507504, 506, 58, 46ellimc2 23855 . . . . . . 7 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))))
508502, 507mpbid 223 . . . . . 6 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))
509508simprd 485 . . . . 5 (𝜑 → ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))
510 notrab 4105 . . . . . 6 (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}
51160cnmetdval 22787 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶𝑥)))
512 abssub 14289 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (abs‘(𝐶𝑥)) = (abs‘(𝑥𝐶)))
513511, 512eqtrd 2840 . . . . . . . . . . 11 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
51424, 513sylan 571 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
515514breq1d 4854 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥𝐶)) ≤ 𝐸))
516515rabbidva 3378 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸})
51732a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51828rexrd 10374 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ*)
519 eqid 2806 . . . . . . . . . 10 {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸}
52047, 519blcld 22523 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
521517, 24, 518, 520syl3anc 1483 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
522516, 521eqeltrrd 2886 . . . . . . 7 (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
523431cldopn 21049 . . . . . . 7 ({𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
524522, 523syl 17 . . . . . 6 (𝜑 → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
525510, 524syl5eqelr 2890 . . . . 5 (𝜑 → {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (TopOpen‘ℂfld))
526414, 509, 525rspcdva 3508 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
527409, 526sylbird 251 . . 3 (𝜑 → (¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
528404, 527mt3d 142 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸)
52928recnd 10353 . . . 4 (𝜑𝐸 ∈ ℂ)
530529mulid2d 10343 . . 3 (𝜑 → (1 · 𝐸) = 𝐸)
531 1red 10326 . . . 4 (𝜑 → 1 ∈ ℝ)
532 1lt2 11470 . . . . 5 1 < 2
533532a1i 11 . . . 4 (𝜑 → 1 < 2)
534531, 30, 27, 533ltmul1dd 12141 . . 3 (𝜑 → (1 · 𝐸) < (2 · 𝐸))
535530, 534eqbrtrrd 4868 . 2 (𝜑𝐸 < (2 · 𝐸))
53626, 28, 31, 528, 535lelttrd 10480 1 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) < (2 · 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  {crab 3100  Vcvv 3391  cdif 3766  cin 3768  wss 3769  c0 4116  {csn 4370  cop 4376   class class class wbr 4844  cmpt 4923   × cxp 5309  dom cdm 5311  ran crn 5312  cres 5313  cima 5314  ccom 5315   Fn wfn 6096  wf 6097  cfv 6101  (class class class)co 6874  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226  *cxr 10358   < clt 10359  cle 10360  cmin 10551   / cdiv 10969  2c2 11356  +crp 12046  (,)cioo 12393  [,]cicc 12396  abscabs 14197  t crest 16286  TopOpenctopn 16287  topGenctg 16303  ∞Metcxmt 19939  ballcbl 19941  fldccnfld 19954  TopOnctopon 20928  Clsdccld 21034  intcnt 21035   Cn ccn 21242   CnP ccnp 21243   ×t ctx 21577  cnccncf 22892   lim climc 23840   D cdv 23841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-fi 8556  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-z 11644  df-dec 11760  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-ioo 12397  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-seq 13025  df-exp 13084  df-hash 13338  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-hom 16177  df-cco 16178  df-rest 16288  df-topn 16289  df-0g 16307  df-gsum 16308  df-topgen 16309  df-pt 16310  df-prds 16313  df-xrs 16367  df-qtop 16372  df-imas 16373  df-xps 16375  df-mre 16451  df-mrc 16452  df-acs 16454  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-submnd 17541  df-mulg 17746  df-cntz 17951  df-cmn 18396  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-fbas 19951  df-fg 19952  df-cnfld 19955  df-top 20912  df-topon 20929  df-topsp 20951  df-bases 20964  df-cld 21037  df-ntr 21038  df-cls 21039  df-nei 21116  df-lp 21154  df-perf 21155  df-cn 21245  df-cnp 21246  df-haus 21333  df-cmp 21404  df-tx 21579  df-hmeo 21772  df-fil 21863  df-fm 21955  df-flim 21956  df-flf 21957  df-xms 22338  df-ms 22339  df-tms 22340  df-cncf 22894  df-limc 23844  df-dv 23845
This theorem is referenced by:  lhop1  23991
  Copyright terms: Public domain W3C validator