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

Theorem lhop1lem 23821
Description: Lemma for lhop1 23822. (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 12249 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐷𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
52, 3, 4syl2anc 694 . . . . . . . 8 (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
6 lhop1lem.x . . . . . . . 8 (𝜑𝑋 ∈ (𝐴(,)𝐷))
75, 6sseldd 3637 . . . . . . 7 (𝜑𝑋 ∈ (𝐴(,)𝐵))
81, 7ffvelrnd 6400 . . . . . 6 (𝜑 → (𝐹𝑋) ∈ ℝ)
98recnd 10106 . . . . 5 (𝜑 → (𝐹𝑋) ∈ ℂ)
10 lhop1.g . . . . . . 7 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
1110, 7ffvelrnd 6400 . . . . . 6 (𝜑 → (𝐺𝑋) ∈ ℝ)
1211recnd 10106 . . . . 5 (𝜑 → (𝐺𝑋) ∈ ℂ)
13 lhop1.gn0 . . . . . 6 (𝜑 → ¬ 0 ∈ ran 𝐺)
14 ffn 6083 . . . . . . . . . 10 (𝐺:(𝐴(,)𝐵)⟶ℝ → 𝐺 Fn (𝐴(,)𝐵))
1510, 14syl 17 . . . . . . . . 9 (𝜑𝐺 Fn (𝐴(,)𝐵))
16 fnfvelrn 6396 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺𝑋) ∈ ran 𝐺)
1715, 7, 16syl2anc 694 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ran 𝐺)
18 eleq1 2718 . . . . . . . 8 ((𝐺𝑋) = 0 → ((𝐺𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
1917, 18syl5ibcom 235 . . . . . . 7 (𝜑 → ((𝐺𝑋) = 0 → 0 ∈ ran 𝐺))
2019necon3bd 2837 . . . . . 6 (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺𝑋) ≠ 0))
2113, 20mpd 15 . . . . 5 (𝜑 → (𝐺𝑋) ≠ 0)
229, 12, 21divcld 10839 . . . 4 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ)
23 limccl 23684 . . . . 5 ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) ⊆ ℂ
24 lhop1.c . . . . 5 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
2523, 24sseldi 3634 . . . 4 (𝜑𝐶 ∈ ℂ)
2622, 25subcld 10430 . . 3 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) − 𝐶) ∈ ℂ)
2726abscld 14219 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ∈ ℝ)
28 lhop1lem.e . . 3 (𝜑𝐸 ∈ ℝ+)
2928rpred 11910 . 2 (𝜑𝐸 ∈ ℝ)
30 2re 11128 . . . 4 2 ∈ ℝ
3130a1i 11 . . 3 (𝜑 → 2 ∈ ℝ)
3231, 29remulcld 10108 . 2 (𝜑 → (2 · 𝐸) ∈ ℝ)
33 cnxmet 22623 . . . . . . . . . . . . 13 (abs ∘ − ) ∈ (∞Met‘ℂ)
3433a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
35 simprl 809 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝑣 ∈ (TopOpen‘ℂfld))
36 simprr 811 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝐴𝑣)
37 eliooord 12271 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋𝑋 < 𝐷))
386, 37syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < 𝑋𝑋 < 𝐷))
3938simpld 474 . . . . . . . . . . . . . 14 (𝜑𝐴 < 𝑋)
40 lhop1.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
41 ioossre 12273 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐷) ⊆ ℝ
4241, 6sseldi 3634 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
43 difrp 11906 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4440, 42, 43syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4539, 44mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐴) ∈ ℝ+)
4645adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (𝑋𝐴) ∈ ℝ+)
47 eqid 2651 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4847cnfldtopn 22632 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
4948mopni3 22346 . . . . . . . . . . . 12 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣) ∧ (𝑋𝐴) ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
5034, 35, 36, 46, 49syl31anc 1369 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
51 lhop1lem.r . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 = (𝐴 + (𝑟 / 2))
5240adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ)
53 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ+)
5453rpred 11910 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ)
5554rehalfcld 11317 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
5652, 55readdcld 10107 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ)
5751, 56syl5eqel 2734 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ)
5857recnd 10106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℂ)
5940recnd 10106 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℂ)
6059adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℂ)
61 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
6261cnmetdval 22621 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
6358, 60, 62syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
6451oveq1i 6700 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴)
6554recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℂ)
6665halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℂ)
6760, 66pncan2d 10432 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2))
6864, 67syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅𝐴) = (𝑟 / 2))
6968fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑅𝐴)) = (abs‘(𝑟 / 2)))
7053rphalfcld 11922 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ+)
7170rpred 11910 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
7270rpge0d 11914 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 0 ≤ (𝑟 / 2))
7371, 72absidd 14205 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
7463, 69, 733eqtrd 2689 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2))
75 rphalflt 11898 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+ → (𝑟 / 2) < 𝑟)
7653, 75syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < 𝑟)
7774, 76eqbrtrd 4707 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟)
7833a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
7954rexrd 10127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ*)
80 elbl3 22244 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8178, 79, 60, 58, 80syl22anc 1367 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8277, 81mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟))
8352, 70ltaddrpd 11943 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2)))
8483, 51syl6breqr 4727 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < 𝑅)
8542adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ)
8685, 52resubcld 10496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑋𝐴) ∈ ℝ)
87 simprr 811 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 < (𝑋𝐴))
8871, 54, 86, 76, 87lttrd 10236 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < (𝑋𝐴))
8952, 71, 85ltaddsub2d 10666 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋𝐴)))
9088, 89mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋)
9151, 90syl5eqbr 4720 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 < 𝑋)
9252rexrd 10127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ*)
9342rexrd 10127 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
9493adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ*)
95 elioo2 12254 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝑋 ∈ ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
9692, 94, 95syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
9757, 84, 91, 96mpbir3and 1264 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝑋))
9882, 97elind 3831 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)))
999adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑋) ∈ ℂ)
1001adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
101 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ∈ ℝ)
102101rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℝ*)
10338simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋 < 𝐷)
10442, 101, 103ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑋𝐷)
10593, 102, 2, 104, 3xrletrd 12031 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
106 iooss2 12249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ ℝ*𝑋𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
1072, 105, 106syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
109108, 97sseldd 3637 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝐵))
110100, 109ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℝ)
111110recnd 10106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℂ)
11299, 111subcld 10430 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
11312adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑋) ∈ ℂ)
11410adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
115114, 109ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℝ)
116115recnd 10106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℂ)
117113, 116subcld 10430 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
118 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
119118adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
12012adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑋) ∈ ℂ)
121107sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵))
12210ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℝ)
123121, 122syldan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℝ)
124123recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℂ)
125120, 124subeq0ad 10440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 ↔ (𝐺𝑋) = (𝐺𝑧)))
126 ioossre 12273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴(,)𝐵) ⊆ ℝ
127126, 121sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ)
128127adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 ∈ ℝ)
12942ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑋 ∈ ℝ)
130 eliooord 12271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧𝑧 < 𝑋))
131130adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧𝑧 < 𝑋))
132131simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋)
133132adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 < 𝑋)
13440rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐴 ∈ ℝ*)
135134adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈ ℝ*)
1362adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈ ℝ*)
137131simpld 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧)
13893, 102, 2, 103, 3xrltletrd 12030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑋 < 𝐵)
139138adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵)
140 iccssioo 12280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝑧𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
141135, 136, 137, 139, 140syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
142141adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
143 ax-resscn 10031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℝ ⊆ ℂ
144143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ℝ ⊆ ℂ)
145 fss 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
14610, 143, 145sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
147126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
148 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
149 dvcn 23729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
150144, 146, 147, 148, 149syl31anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
151 cncffvrn 22748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ℝ ⊆ ℂ ∧ 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
152143, 150, 151sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
15310, 152mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
154153ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
155 rescncf 22747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)))
156142, 154, 155sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))
157143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ℝ ⊆ ℂ)
158146ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
159126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐴(,)𝐵) ⊆ ℝ)
160142, 126syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ ℝ)
16147tgioo2 22653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
16247, 161dvres 23720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
163157, 158, 159, 160, 162syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
164 iccntr 22671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
165128, 129, 164syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
166165reseq2d 5428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
167163, 166eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
168167dmeqd 5358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
169 ioossicc 12297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋)
170169, 142syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵))
171148ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
172170, 171sseqtr4d 3675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺))
173 ssdmres 5455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
174172, 173sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
175168, 174eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋))
176127rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*)
17793adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ*)
17842adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ)
179127, 178, 132ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧𝑋)
180 ubicc2 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑋 ∈ (𝑧[,]𝑋))
181176, 177, 179, 180syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋))
182 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑋 ∈ (𝑧[,]𝑋) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
183181, 182syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
184 lbicc2 12326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑧 ∈ (𝑧[,]𝑋))
185176, 177, 179, 184syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋))
186 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (𝑧[,]𝑋) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
187185, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
188183, 187eqeq12d 2666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺𝑋) = (𝐺𝑧)))
189188biimpar 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧))
190189eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋))
191128, 129, 133, 156, 175, 190rolle 23798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0)
192167fveq1d 6231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤))
193 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
194192, 193sylan9eq 2705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
195 dvf 23716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
196148feq2d 6069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
197195, 196mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
198197ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
199 ffn 6083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
200198, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
201200adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
202170sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
203 fnfvelrn 6396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
204201, 202, 203syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
205194, 204eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺))
206 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
207205, 206syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
208207rexlimdva 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
209191, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 0 ∈ ran (ℝ D 𝐺))
210209ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) = (𝐺𝑧) → 0 ∈ ran (ℝ D 𝐺)))
211125, 210sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺)))
212211necon3bd 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
213119, 212mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
214213ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
215214adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
216 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑅 → (𝐺𝑧) = (𝐺𝑅))
217216oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑅 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑅)))
218217neeq1d 2882 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑅 → (((𝐺𝑋) − (𝐺𝑧)) ≠ 0 ↔ ((𝐺𝑋) − (𝐺𝑅)) ≠ 0))
219218rspcv 3336 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ (𝐴(,)𝑋) → (∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0 → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0))
22097, 215, 219sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
221112, 117, 220divcld 10839 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) ∈ ℂ)
22225adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐶 ∈ ℂ)
223221, 222subcld 10430 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶) ∈ ℂ)
224223abscld 14219 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ∈ ℝ)
22529adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐸 ∈ ℝ)
226102adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐷 ∈ ℝ*)
227103adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 < 𝐷)
228 iccssioo 12280 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ*𝐷 ∈ ℝ*) ∧ (𝐴 < 𝑅𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
22992, 226, 84, 227, 228syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
2305adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
231229, 230sstrd 3646 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵))
232 fss 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
2331, 143, 232sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
234 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
235 dvcn 23729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
236144, 233, 147, 234, 235syl31anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
237 cncffvrn 22748 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
238143, 236, 237sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
2391, 238mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
240239adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
241 rescncf 22747 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
242231, 240, 241sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
243153adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
244 rescncf 22747 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
245231, 243, 244sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
246143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ℝ ⊆ ℂ)
247233adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
248126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐵) ⊆ ℝ)
249 iccssre 12293 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ)
25057, 85, 249syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ ℝ)
25147, 161dvres 23720 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
252246, 247, 248, 250, 251syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
253 iccntr 22671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
25457, 85, 253syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
255254reseq2d 5428 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
256252, 255eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
257256dmeqd 5358 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
25852, 57, 84ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴𝑅)
259 iooss1 12248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝐴𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
26092, 258, 259syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
261104adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋𝐷)
262 iooss2 12249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐷 ∈ ℝ*𝑋𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
263226, 261, 262syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
264260, 263sstrd 3646 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷))
265264, 230sstrd 3646 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵))
266234adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
267265, 266sseqtr4d 3675 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹))
268 ssdmres 5455 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
269267, 268sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
270257, 269eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
271146adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
27247, 161dvres 23720 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
273246, 271, 248, 250, 272syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
274254reseq2d 5428 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
275273, 274eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
276275dmeqd 5358 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
277148adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
278265, 277sseqtr4d 3675 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺))
279 ssdmres 5455 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
280278, 279sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
281276, 280eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
28257, 85, 91, 242, 245, 270, 281cmvth 23799 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)))
28357rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ*)
284283adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ ℝ*)
28593ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ ℝ*)
28657, 85, 91ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅𝑋)
287286adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅𝑋)
288 ubicc2 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑋 ∈ (𝑅[,]𝑋))
289284, 285, 287, 288syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋))
290 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ (𝑅[,]𝑋) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
291289, 290syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
292 lbicc2 12326 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑅 ∈ (𝑅[,]𝑋))
293284, 285, 287, 292syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋))
294 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑅 ∈ (𝑅[,]𝑋) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
295293, 294syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
296291, 295oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹𝑋) − (𝐹𝑅)))
297275fveq1d 6231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤))
298 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
299297, 298sylan9eq 2705 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
300296, 299oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)))
301 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑋 ∈ (𝑅[,]𝑋) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
302289, 301syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
303 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑅 ∈ (𝑅[,]𝑋) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
304293, 303syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
305302, 304oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺𝑋) − (𝐺𝑅)))
306256fveq1d 6231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤))
307 fvres 6245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
308306, 307sylan9eq 2705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
309305, 308oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)))
310117adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
311 dvf 23716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
312234feq2d 6069 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
313311, 312mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
314313ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
315265sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
316314, 315ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ)
317310, 316mulcomd 10099 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
318309, 317eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
319300, 318eqeq12d 2666 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
320112adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
321197ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
322321, 315ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ)
323220adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
324118ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
325321, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
326325, 315, 203syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
327 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
328326, 327syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
329328necon3bd 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0))
330324, 329mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0)
331320, 310, 316, 322, 323, 330divmuleqd 10885 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
332319, 331bitr4d 271 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
333332rexbidva 3078 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
334282, 333mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
335264sselda 3636 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷))
336 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
337336ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
338 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤))
339 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤))
340338, 339oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
341340oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶) = ((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶))
342341fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
343342breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
344343rspcv 3336 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ (𝐴(,)𝐷) → (∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
345335, 337, 344sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)
346 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶) = ((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶))
347346fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
348347breq1d 4695 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
349345, 348syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
350349rexlimdva 3060 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
351334, 350mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸)
352224, 225, 351ltled 10223 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸)
353 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑅 → (𝐹𝑢) = (𝐹𝑅))
354353oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → ((𝐹𝑋) − (𝐹𝑢)) = ((𝐹𝑋) − (𝐹𝑅)))
355 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑅 → (𝐺𝑢) = (𝐺𝑅))
356355oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → ((𝐺𝑋) − (𝐺𝑢)) = ((𝐺𝑋) − (𝐺𝑅)))
357354, 356oveq12d 6708 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) = (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))))
358357oveq1d 6705 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑅 → ((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶) = ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶))
359358fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑅 → (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)))
360359breq1d 4695 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑅 → ((abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸))
361360rspcev 3340 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
36298, 352, 361syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
363362adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
364 ssrin 3871 . . . . . . . . . . . . . . . . 17 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋)))
365 lbioo 12244 . . . . . . . . . . . . . . . . . . . 20 ¬ 𝐴 ∈ (𝐴(,)𝑋)
366 disjsn 4278 . . . . . . . . . . . . . . . . . . . 20 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋))
367365, 366mpbir 221 . . . . . . . . . . . . . . . . . . 19 ((𝐴(,)𝑋) ∩ {𝐴}) = ∅
368 disj3 4054 . . . . . . . . . . . . . . . . . . 19 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}))
369367, 368mpbi 220 . . . . . . . . . . . . . . . . . 18 (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})
370369ineq2i 3844 . . . . . . . . . . . . . . . . 17 (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))
371364, 370syl6sseq 3684 . . . . . . . . . . . . . . . 16 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))
372 ssrexv 3700 . . . . . . . . . . . . . . . 16 (((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
373371, 372syl 17 . . . . . . . . . . . . . . 15 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
374363, 373syl5com 31 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
375374anassrs 681 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
376375expimpd 628 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
377376rexlimdva 3060 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
37850, 377mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
379 inss2 3867 . . . . . . . . . . . . . 14 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴})
380 difss 3770 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋)
381379, 380sstri 3645 . . . . . . . . . . . . 13 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)
382381sseli 3632 . . . . . . . . . . . 12 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋))
383 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → (𝐹𝑧) = (𝐹𝑢))
384383oveq2d 6706 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → ((𝐹𝑋) − (𝐹𝑧)) = ((𝐹𝑋) − (𝐹𝑢)))
385 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → (𝐺𝑧) = (𝐺𝑢))
386385oveq2d 6706 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑢)))
387384, 386oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
388 eqid 2651 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))
389 ovex 6718 . . . . . . . . . . . . . . . 16 (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) ∈ V
390387, 388, 389fvmpt 6321 . . . . . . . . . . . . . . 15 (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
391390oveq1d 6705 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝑋) → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶) = ((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶))
392391fveq2d 6233 . . . . . . . . . . . . 13 (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)))
393392breq1d 4695 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
394382, 393syl 17 . . . . . . . . . . 11 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
395394rexbiia 3069 . . . . . . . . . 10 (∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
396378, 395sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
397 ovex 6718 . . . . . . . . . . 11 (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ V
398397, 388fnmpti 6060 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋)
399 oveq1 6697 . . . . . . . . . . . . 13 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → (𝑥𝐶) = (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶))
400399fveq2d 6233 . . . . . . . . . . . 12 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → (abs‘(𝑥𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)))
401400breq1d 4695 . . . . . . . . . . 11 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
402401rexima 6537 . . . . . . . . . 10 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
403398, 381, 402mp2an 708 . . . . . . . . 9 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
404396, 403sylibr 224 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸)
405 dfrex2 3025 . . . . . . . 8 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
406404, 405sylib 208 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
407 ssrab 3713 . . . . . . . 8 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸))
408407simprbi 479 . . . . . . 7 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
409406, 408nsyl 135 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})
410409expr 642 . . . . 5 ((𝜑𝑣 ∈ (TopOpen‘ℂfld)) → (𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
411410ralrimiva 2995 . . . 4 (𝜑 → ∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
412 ralinexa 3026 . . . 4 (∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
413411, 412sylib 208 . . 3 (𝜑 → ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
414 oveq1 6697 . . . . . . . . 9 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (𝑥𝐶) = (((𝐹𝑋) / (𝐺𝑋)) − 𝐶))
415414fveq2d 6233 . . . . . . . 8 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (abs‘(𝑥𝐶)) = (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)))
416415breq1d 4695 . . . . . . 7 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
417416notbid 307 . . . . . 6 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (¬ (abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
418417elrab3 3397 . . . . 5 (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
41922, 418syl 17 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
420 notrab 3937 . . . . . 6 (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}
42161cnmetdval 22621 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶𝑥)))
422 abssub 14110 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (abs‘(𝐶𝑥)) = (abs‘(𝑥𝐶)))
423421, 422eqtrd 2685 . . . . . . . . . . 11 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
42425, 423sylan 487 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
425424breq1d 4695 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥𝐶)) ≤ 𝐸))
426425rabbidva 3219 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸})
42733a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
42829rexrd 10127 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ*)
429 eqid 2651 . . . . . . . . . 10 {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸}
43048, 429blcld 22357 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
431427, 25, 428, 430syl3anc 1366 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
432426, 431eqeltrrd 2731 . . . . . . 7 (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
43347cnfldtopon 22633 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
434433toponunii 20769 . . . . . . . 8 ℂ = (TopOpen‘ℂfld)
435434cldopn 20883 . . . . . . 7 ({𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
436432, 435syl 17 . . . . . 6 (𝜑 → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
437420, 436syl5eqelr 2735 . . . . 5 (𝜑 → {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (TopOpen‘ℂfld))
4389adantr 480 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑋) ∈ ℂ)
4391ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℝ)
440121, 439syldan 486 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℝ)
441440recnd 10106 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℂ)
442438, 441subcld 10430 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑧)) ∈ ℂ)
443120, 124subcld 10430 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ)
444 eldifsn 4350 . . . . . . . . 9 (((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}) ↔ (((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ ∧ ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
445443, 213, 444sylanbrc 699 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}))
446 ssid 3657 . . . . . . . . 9 ℂ ⊆ ℂ
447446a1i 11 . . . . . . . 8 (𝜑 → ℂ ⊆ ℂ)
448 difss 3770 . . . . . . . . 9 (ℂ ∖ {0}) ⊆ ℂ
449448a1i 11 . . . . . . . 8 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
450 cnex 10055 . . . . . . . . . 10 ℂ ∈ V
451450, 448ssexi 4836 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
452 txrest 21482 . . . . . . . . . 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}))))
453433, 433, 450, 451, 452mp4an 709 . . . . . . . . 9 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
454434restid 16141 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
455433, 454ax-mp 5 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
456455oveq1i 6700 . . . . . . . . 9 (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
457453, 456eqtr2i 2674 . . . . . . . 8 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0})))
4589subid1d 10419 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) = (𝐹𝑋))
459 txtopon 21442 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
460433, 433, 459mp2an 708 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
461460toponunii 20769 . . . . . . . . . . . . 13 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
462461restid 16141 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)) → (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ)) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)))
463460, 462ax-mp 5 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ)) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
464463eqcomi 2660 . . . . . . . . . 10 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
465 limcresi 23694 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
466 ioossre 12273 . . . . . . . . . . . . . 14 (𝐴(,)𝑋) ⊆ ℝ
467 resmpt 5484 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)))
468466, 467ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋))
469468oveq1i 6700 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
470465, 469sseqtri 3670 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
471 cncfmptc 22761 . . . . . . . . . . . . 13 (((𝐹𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
4728, 144, 144, 471syl3anc 1366 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
473 eqidd 2652 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐹𝑋) = (𝐹𝑋))
474472, 40, 473cnmptlimc 23699 . . . . . . . . . . 11 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴))
475470, 474sseldi 3634 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴))
476 limcresi 23694 . . . . . . . . . . . 12 (𝐹 lim 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴)
4771, 107feqresmpt 6289 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)))
478477oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
479476, 478syl5sseq 3686 . . . . . . . . . . 11 (𝜑 → (𝐹 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
480 lhop1.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
481479, 480sseldd 3637 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
48247subcn 22716 . . . . . . . . . . 11 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
483 0cn 10070 . . . . . . . . . . . 12 0 ∈ ℂ
484 opelxpi 5182 . . . . . . . . . . . 12 (((𝐹𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
4859, 483, 484sylancl 695 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
486461cncnpi 21130 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
487482, 485, 486sylancr 696 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
488438, 441, 447, 447, 47, 464, 475, 481, 487limccnp2 23701 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
489458, 488eqeltrrd 2731 . . . . . . . 8 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
49012subid1d 10419 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) = (𝐺𝑋))
491 limcresi 23694 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
492 resmpt 5484 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)))
493466, 492ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋))
494493oveq1i 6700 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
495491, 494sseqtri 3670 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
496 cncfmptc 22761 . . . . . . . . . . . . 13 (((𝐺𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
49711, 144, 144, 496syl3anc 1366 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
498 eqidd 2652 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐺𝑋) = (𝐺𝑋))
499497, 40, 498cnmptlimc 23699 . . . . . . . . . . 11 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴))
500495, 499sseldi 3634 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴))
501 limcresi 23694 . . . . . . . . . . . 12 (𝐺 lim 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴)
50210, 107feqresmpt 6289 . . . . . . . . . . . . 13 (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)))
503502oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
504501, 503syl5sseq 3686 . . . . . . . . . . 11 (𝜑 → (𝐺 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
505 lhop1.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
506504, 505sseldd 3637 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
507 opelxpi 5182 . . . . . . . . . . . 12 (((𝐺𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
50812, 483, 507sylancl 695 . . . . . . . . . . 11 (𝜑 → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
509461cncnpi 21130 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
510482, 508, 509sylancr 696 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
511120, 124, 447, 447, 47, 464, 500, 506, 510limccnp2 23701 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
512490, 511eqeltrrd 2731 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
513 eqid 2651 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
51447, 513divcn 22718 . . . . . . . . 9 / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld))
515 eldifsn 4350 . . . . . . . . . . 11 ((𝐺𝑋) ∈ (ℂ ∖ {0}) ↔ ((𝐺𝑋) ∈ ℂ ∧ (𝐺𝑋) ≠ 0))
51612, 21, 515sylanbrc 699 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ (ℂ ∖ {0}))
517 opelxpi 5182 . . . . . . . . . 10 (((𝐹𝑋) ∈ ℂ ∧ (𝐺𝑋) ∈ (ℂ ∖ {0})) → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
5189, 516, 517syl2anc 694 . . . . . . . . 9 (𝜑 → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
519 resttopon 21013 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
520433, 448, 519mp2an 708 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))
521 txtopon 21442 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))) → ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0}))))
522433, 520, 521mp2an 708 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0})))
523522toponunii 20769 . . . . . . . . . 10 (ℂ × (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
524523cncnpi 21130 . . . . . . . . 9 (( / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0}))) → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
525514, 518, 524sylancr 696 . . . . . . . 8 (𝜑 → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
526442, 445, 447, 449, 47, 457, 489, 512, 525limccnp2 23701 . . . . . . 7 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴))
527442, 443, 213divcld 10839 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ ℂ)
528527, 388fmptd 6425 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))):(𝐴(,)𝑋)⟶ℂ)
529466, 143sstri 3645 . . . . . . . . 9 (𝐴(,)𝑋) ⊆ ℂ
530529a1i 11 . . . . . . . 8 (𝜑 → (𝐴(,)𝑋) ⊆ ℂ)
531528, 530, 59, 47ellimc2 23686 . . . . . . 7 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))))
532526, 531mpbid 222 . . . . . 6 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))
533532simprd 478 . . . . 5 (𝜑 → ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))
534 eleq2 2719 . . . . . . 7 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 ↔ ((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
535 sseq2 3660 . . . . . . . . 9 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
536535anbi2d 740 . . . . . . . 8 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
537536rexbidv 3081 . . . . . . 7 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
538534, 537imbi12d 333 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))))
539538rspcv 3336 . . . . 5 ({𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (TopOpen‘ℂfld) → (∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))))
540437, 533, 539sylc 65 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
541419, 540sylbird 250 . . 3 (𝜑 → (¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
542413, 541mt3d 140 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸)
54329recnd 10106 . . . 4 (𝜑𝐸 ∈ ℂ)
544543mulid2d 10096 . . 3 (𝜑 → (1 · 𝐸) = 𝐸)
545 1red 10093 . . . 4 (𝜑 → 1 ∈ ℝ)
546 1lt2 11232 . . . . 5 1 < 2
547546a1i 11 . . . 4 (𝜑 → 1 < 2)
548545, 31, 28, 547ltmul1dd 11965 . . 3 (𝜑 → (1 · 𝐸) < (2 · 𝐸))
549544, 548eqbrtrrd 4709 . 2 (𝜑𝐸 < (2 · 𝐸))
55027, 29, 32, 542, 549lelttrd 10233 1 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) < (2 · 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cin 3606  wss 3607  c0 3948  {csn 4210  cop 4216   class class class wbr 4685  cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  *cxr 10111   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  2c2 11108  +crp 11870  (,)cioo 12213  [,]cicc 12216  abscabs 14018  t crest 16128  TopOpenctopn 16129  topGenctg 16145  ∞Metcxmt 19779  ballcbl 19781  fldccnfld 19794  TopOnctopon 20763  Clsdccld 20868  intcnt 20869   Cn ccn 21076   CnP ccnp 21077   ×t ctx 21411  cnccncf 22726   lim climc 23671   D cdv 23672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676
This theorem is referenced by:  lhop1  23822
  Copyright terms: Public domain W3C validator