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

Theorem lhop1lem 25282
Description: Lemma for lhop1 25283. (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 13220 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐷𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
52, 3, 4syl2anc 585 . . . . . . . 8 (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
6 lhop1lem.x . . . . . . . 8 (𝜑𝑋 ∈ (𝐴(,)𝐷))
75, 6sseldd 3936 . . . . . . 7 (𝜑𝑋 ∈ (𝐴(,)𝐵))
81, 7ffvelcdmd 7022 . . . . . 6 (𝜑 → (𝐹𝑋) ∈ ℝ)
98recnd 11108 . . . . 5 (𝜑 → (𝐹𝑋) ∈ ℂ)
10 lhop1.g . . . . . . 7 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
1110, 7ffvelcdmd 7022 . . . . . 6 (𝜑 → (𝐺𝑋) ∈ ℝ)
1211recnd 11108 . . . . 5 (𝜑 → (𝐺𝑋) ∈ ℂ)
13 lhop1.gn0 . . . . . 6 (𝜑 → ¬ 0 ∈ ran 𝐺)
1410ffnd 6656 . . . . . . . . 9 (𝜑𝐺 Fn (𝐴(,)𝐵))
15 fnfvelrn 7018 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺𝑋) ∈ ran 𝐺)
1614, 7, 15syl2anc 585 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ran 𝐺)
17 eleq1 2825 . . . . . . . 8 ((𝐺𝑋) = 0 → ((𝐺𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
1816, 17syl5ibcom 245 . . . . . . 7 (𝜑 → ((𝐺𝑋) = 0 → 0 ∈ ran 𝐺))
1918necon3bd 2955 . . . . . 6 (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺𝑋) ≠ 0))
2013, 19mpd 15 . . . . 5 (𝜑 → (𝐺𝑋) ≠ 0)
219, 12, 20divcld 11856 . . . 4 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ)
22 limccl 25144 . . . . 5 ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) ⊆ ℂ
23 lhop1.c . . . . 5 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
2422, 23sselid 3933 . . . 4 (𝜑𝐶 ∈ ℂ)
2521, 24subcld 11437 . . 3 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) − 𝐶) ∈ ℂ)
2625abscld 15247 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ∈ ℝ)
27 lhop1lem.e . . 3 (𝜑𝐸 ∈ ℝ+)
2827rpred 12877 . 2 (𝜑𝐸 ∈ ℝ)
29 2re 12152 . . . 4 2 ∈ ℝ
3029a1i 11 . . 3 (𝜑 → 2 ∈ ℝ)
3130, 28remulcld 11110 . 2 (𝜑 → (2 · 𝐸) ∈ ℝ)
32 cnxmet 24041 . . . . . . . . . . . . 13 (abs ∘ − ) ∈ (∞Met‘ℂ)
3332a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
34 simprl 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝑣 ∈ (TopOpen‘ℂfld))
35 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝐴𝑣)
36 eliooord 13243 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋𝑋 < 𝐷))
376, 36syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < 𝑋𝑋 < 𝐷))
3837simpld 496 . . . . . . . . . . . . . 14 (𝜑𝐴 < 𝑋)
39 lhop1.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
40 ioossre 13245 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐷) ⊆ ℝ
4140, 6sselid 3933 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
42 difrp 12873 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4339, 41, 42syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4438, 43mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐴) ∈ ℝ+)
4544adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (𝑋𝐴) ∈ ℝ+)
46 eqid 2737 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4746cnfldtopn 24050 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
4847mopni3 23755 . . . . . . . . . . . 12 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣) ∧ (𝑋𝐴) ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
4933, 34, 35, 45, 48syl31anc 1373 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
50 ssrin 4184 . . . . . . . . . . . . . . . 16 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋)))
51 lbioo 13215 . . . . . . . . . . . . . . . . . . 19 ¬ 𝐴 ∈ (𝐴(,)𝑋)
52 disjsn 4663 . . . . . . . . . . . . . . . . . . 19 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋))
5351, 52mpbir 230 . . . . . . . . . . . . . . . . . 18 ((𝐴(,)𝑋) ∩ {𝐴}) = ∅
54 disj3 4404 . . . . . . . . . . . . . . . . . 18 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}))
5553, 54mpbi 229 . . . . . . . . . . . . . . . . 17 (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})
5655ineq2i 4160 . . . . . . . . . . . . . . . 16 (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))
5750, 56sseqtrdi 3985 . . . . . . . . . . . . . . 15 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))
58 lhop1lem.r . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 = (𝐴 + (𝑟 / 2))
5939adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ)
60 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ+)
6160rpred 12877 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ)
6261rehalfcld 12325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
6359, 62readdcld 11109 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ)
6458, 63eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ)
6564recnd 11108 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℂ)
6639recnd 11108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℂ)
6766adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℂ)
68 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
6968cnmetdval 24039 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
7065, 67, 69syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
7158oveq1i 7351 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴)
7261recnd 11108 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℂ)
7372halfcld 12323 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℂ)
7467, 73pncan2d 11439 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2))
7571, 74eqtrid 2789 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅𝐴) = (𝑟 / 2))
7675fveq2d 6833 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑅𝐴)) = (abs‘(𝑟 / 2)))
7760rphalfcld 12889 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ+)
7877rpred 12877 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
7977rpge0d 12881 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 0 ≤ (𝑟 / 2))
8078, 79absidd 15233 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
8170, 76, 803eqtrd 2781 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2))
82 rphalflt 12864 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+ → (𝑟 / 2) < 𝑟)
8360, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < 𝑟)
8481, 83eqbrtrd 5118 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟)
8532a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
8661rexrd 11130 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ*)
87 elbl3 23650 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8885, 86, 67, 65, 87syl22anc 837 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8984, 88mpbird 257 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟))
9059, 77ltaddrpd 12910 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2)))
9190, 58breqtrrdi 5138 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < 𝑅)
9241adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ)
9392, 59resubcld 11508 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑋𝐴) ∈ ℝ)
94 simprr 771 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 < (𝑋𝐴))
9578, 61, 93, 83, 94lttrd 11241 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < (𝑋𝐴))
9659, 78, 92ltaddsub2d 11681 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋𝐴)))
9795, 96mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋)
9858, 97eqbrtrid 5131 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 < 𝑋)
9959rexrd 11130 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ*)
10041rexrd 11130 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
101100adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ*)
102 elioo2 13225 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝑋 ∈ ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
10399, 101, 102syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
10464, 91, 98, 103mpbir3and 1342 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝑋))
10589, 104elind 4145 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)))
1069adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑋) ∈ ℂ)
1071adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
108 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ∈ ℝ)
109108rexrd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℝ*)
11037simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋 < 𝐷)
11141, 108, 110ltled 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑋𝐷)
112100, 109, 2, 111, 3xrletrd 13001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
113 iooss2 13220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ ℝ*𝑋𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
1142, 112, 113syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
115114adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
116115, 104sseldd 3936 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝐵))
117107, 116ffvelcdmd 7022 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℝ)
118117recnd 11108 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℂ)
119106, 118subcld 11437 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
12012adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑋) ∈ ℂ)
12110adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
122121, 116ffvelcdmd 7022 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℝ)
123122recnd 11108 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℂ)
124120, 123subcld 11437 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
125 fveq2 6829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑅 → (𝐺𝑧) = (𝐺𝑅))
126125oveq2d 7357 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑅 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑅)))
127126neeq1d 3001 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑅 → (((𝐺𝑋) − (𝐺𝑧)) ≠ 0 ↔ ((𝐺𝑋) − (𝐺𝑅)) ≠ 0))
128 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
129128adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
13012adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑋) ∈ ℂ)
131114sselda 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵))
13210ffvelcdmda 7021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℝ)
133131, 132syldan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℝ)
134133recnd 11108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℂ)
135130, 134subeq0ad 11447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 ↔ (𝐺𝑋) = (𝐺𝑧)))
136 ioossre 13245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴(,)𝐵) ⊆ ℝ
137136, 131sselid 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ)
138137adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 ∈ ℝ)
13941ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑋 ∈ ℝ)
140 eliooord 13243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧𝑧 < 𝑋))
141140adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧𝑧 < 𝑋))
142141simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋)
143142adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 < 𝑋)
14439rexrd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐴 ∈ ℝ*)
145144adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈ ℝ*)
1462adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈ ℝ*)
147141simpld 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧)
148100, 109, 2, 110, 3xrltletrd 13000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑋 < 𝐵)
149148adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵)
150 iccssioo 13253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝑧𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
151145, 146, 147, 149, 150syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
152151adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
153 ax-resscn 11033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℝ ⊆ ℂ
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ℝ ⊆ ℂ)
155 fss 6672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
15610, 153, 155sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
157136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
158 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
159 dvcn 25190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
160154, 156, 157, 158, 159syl31anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
161 cncfcdm 24166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ℝ ⊆ ℂ ∧ 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
162153, 160, 161sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
16310, 162mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
164163ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
165 rescncf 24165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)))
166152, 164, 165sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))
167153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ℝ ⊆ ℂ)
168156ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
169136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐴(,)𝐵) ⊆ ℝ)
170152, 136sstrdi 3947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ ℝ)
17146tgioo2 24071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
17246, 171dvres 25180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
173167, 168, 169, 170, 172syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
174 iccntr 24089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
175138, 139, 174syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
176175reseq2d 5927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
177173, 176eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
178177dmeqd 5851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
179 ioossicc 13270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋)
180179, 152sstrid 3946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵))
181158ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
182180, 181sseqtrrd 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺))
183 ssdmres 5950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
184182, 183sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
185178, 184eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋))
186137rexrd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*)
187100adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ*)
18841adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ)
189137, 188, 142ltled 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧𝑋)
190 ubicc2 13302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑋 ∈ (𝑧[,]𝑋))
191186, 187, 189, 190syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋))
192191fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
193 lbicc2 13301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑧 ∈ (𝑧[,]𝑋))
194186, 187, 189, 193syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋))
195194fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
196192, 195eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺𝑋) = (𝐺𝑧)))
197196biimpar 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧))
198197eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋))
199138, 139, 143, 166, 185, 198rolle 25259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0)
200177fveq1d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤))
201 fvres 6848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
202200, 201sylan9eq 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
203 dvf 25176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
204158feq2d 6641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
205203, 204mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
206205ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
207206ffnd 6656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
208207adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
209180sselda 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
210 fnfvelrn 7018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
211208, 209, 210syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
212202, 211eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺))
213 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
214212, 213syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
215214rexlimdva 3149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
216199, 215mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 0 ∈ ran (ℝ D 𝐺))
217216ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) = (𝐺𝑧) → 0 ∈ ran (ℝ D 𝐺)))
218135, 217sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺)))
219218necon3bd 2955 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
220129, 219mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
221220ralrimiva 3140 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
222221adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
223127, 222, 104rspcdva 3574 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
224119, 124, 223divcld 11856 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) ∈ ℂ)
22524adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐶 ∈ ℂ)
226224, 225subcld 11437 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶) ∈ ℂ)
227226abscld 15247 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ∈ ℝ)
22828adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐸 ∈ ℝ)
229109adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐷 ∈ ℝ*)
230110adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 < 𝐷)
231 iccssioo 13253 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ*𝐷 ∈ ℝ*) ∧ (𝐴 < 𝑅𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
23299, 229, 91, 230, 231syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
2335adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
234232, 233sstrd 3945 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵))
235 fss 6672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
2361, 153, 235sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
237 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
238 dvcn 25190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
239154, 236, 157, 237, 238syl31anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
240 cncfcdm 24166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
241153, 239, 240sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
2421, 241mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
243242adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
244 rescncf 24165 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
245234, 243, 244sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
246163adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
247 rescncf 24165 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
248234, 246, 247sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
249153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ℝ ⊆ ℂ)
250236adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
251136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐵) ⊆ ℝ)
252 iccssre 13266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ)
25364, 92, 252syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ ℝ)
25446, 171dvres 25180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
255249, 250, 251, 253, 254syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
256 iccntr 24089 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
25764, 92, 256syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
258257reseq2d 5927 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
259255, 258eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
260259dmeqd 5851 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
26159, 64, 91ltled 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴𝑅)
262 iooss1 13219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝐴𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
26399, 261, 262syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
264111adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋𝐷)
265 iooss2 13220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐷 ∈ ℝ*𝑋𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
266229, 264, 265syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
267263, 266sstrd 3945 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷))
268267, 233sstrd 3945 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵))
269237adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
270268, 269sseqtrrd 3976 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹))
271 ssdmres 5950 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
272270, 271sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
273260, 272eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
274156adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
27546, 171dvres 25180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
276249, 274, 251, 253, 275syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
277257reseq2d 5927 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
278276, 277eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
279278dmeqd 5851 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
280158adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
281268, 280sseqtrrd 3976 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺))
282 ssdmres 5950 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
283281, 282sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
284279, 283eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
28564, 92, 98, 245, 248, 273, 284cmvth 25260 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)))
28664rexrd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ*)
287286adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ ℝ*)
288100ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ ℝ*)
28964, 92, 98ltled 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅𝑋)
290289adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅𝑋)
291 ubicc2 13302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑋 ∈ (𝑅[,]𝑋))
292287, 288, 290, 291syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋))
293292fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
294 lbicc2 13301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑅 ∈ (𝑅[,]𝑋))
295287, 288, 290, 294syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋))
296295fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
297293, 296oveq12d 7359 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹𝑋) − (𝐹𝑅)))
298278fveq1d 6831 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤))
299 fvres 6848 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
300298, 299sylan9eq 2797 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
301297, 300oveq12d 7359 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)))
302292fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
303295fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
304302, 303oveq12d 7359 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺𝑋) − (𝐺𝑅)))
305259fveq1d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤))
306 fvres 6848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
307305, 306sylan9eq 2797 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
308304, 307oveq12d 7359 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)))
309124adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
310 dvf 25176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
311237feq2d 6641 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
312310, 311mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
313312ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
314268sselda 3935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
315313, 314ffvelcdmd 7022 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ)
316309, 315mulcomd 11101 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
317308, 316eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
318301, 317eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
319119adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
320205ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
321320, 314ffvelcdmd 7022 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ)
322223adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
323128ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
324320ffnd 6656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
325324, 314, 210syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
326 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
327325, 326syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
328327necon3bd 2955 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0))
329323, 328mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0)
330319, 309, 315, 321, 322, 329divmuleqd 11902 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
331318, 330bitr4d 282 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
332331rexbidva 3170 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
333285, 332mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
334 fveq2 6829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤))
335 fveq2 6829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤))
336334, 335oveq12d 7359 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
337336fvoveq1d 7363 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
338337breq1d 5106 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
339 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
340339ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
341267sselda 3935 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷))
342338, 340, 341rspcdva 3574 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)
343 fvoveq1 7364 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
344343breq1d 5106 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
345342, 344syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
346345rexlimdva 3149 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
347333, 346mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸)
348227, 228, 347ltled 11228 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸)
349 fveq2 6829 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐹𝑢) = (𝐹𝑅))
350349oveq2d 7357 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐹𝑋) − (𝐹𝑢)) = ((𝐹𝑋) − (𝐹𝑅)))
351 fveq2 6829 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐺𝑢) = (𝐺𝑅))
352351oveq2d 7357 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐺𝑋) − (𝐺𝑢)) = ((𝐺𝑋) − (𝐺𝑅)))
353350, 352oveq12d 7359 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑅 → (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) = (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))))
354353fvoveq1d 7363 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑅 → (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)))
355354breq1d 5106 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑅 → ((abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸))
356355rspcev 3573 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
357105, 348, 356syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
358357adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
359 ssrexv 4002 . . . . . . . . . . . . . . 15 (((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
36057, 358, 359syl2imc 41 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
361360anassrs 469 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
362361expimpd 455 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
363362rexlimdva 3149 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
36449, 363mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
365 inss2 4180 . . . . . . . . . . . . . 14 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴})
366 difss 4082 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋)
367365, 366sstri 3944 . . . . . . . . . . . . 13 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)
368367sseli 3931 . . . . . . . . . . . 12 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋))
369 fveq2 6829 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐹𝑧) = (𝐹𝑢))
370369oveq2d 7357 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐹𝑋) − (𝐹𝑧)) = ((𝐹𝑋) − (𝐹𝑢)))
371 fveq2 6829 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐺𝑧) = (𝐺𝑢))
372371oveq2d 7357 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑢)))
373370, 372oveq12d 7359 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
374 eqid 2737 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))
375 ovex 7374 . . . . . . . . . . . . . . 15 (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) ∈ V
376373, 374, 375fvmpt 6935 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
377376fvoveq1d 7363 . . . . . . . . . . . . 13 (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)))
378377breq1d 5106 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
379368, 378syl 17 . . . . . . . . . . 11 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
380379rexbiia 3092 . . . . . . . . . 10 (∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
381364, 380sylibr 233 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
382 ovex 7374 . . . . . . . . . . 11 (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ V
383382, 374fnmpti 6631 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋)
384 fvoveq1 7364 . . . . . . . . . . . 12 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → (abs‘(𝑥𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)))
385384breq1d 5106 . . . . . . . . . . 11 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
386385rexima 7173 . . . . . . . . . 10 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
387383, 367, 386mp2an 690 . . . . . . . . 9 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
388381, 387sylibr 233 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸)
389 dfrex2 3074 . . . . . . . 8 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
390388, 389sylib 217 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
391 ssrab 4021 . . . . . . . 8 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸))
392391simprbi 498 . . . . . . 7 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
393390, 392nsyl 140 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})
394393expr 458 . . . . 5 ((𝜑𝑣 ∈ (TopOpen‘ℂfld)) → (𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
395394ralrimiva 3140 . . . 4 (𝜑 → ∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
396 ralinexa 3101 . . . 4 (∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
397395, 396sylib 217 . . 3 (𝜑 → ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
398 fvoveq1 7364 . . . . . . . 8 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (abs‘(𝑥𝐶)) = (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)))
399398breq1d 5106 . . . . . . 7 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
400399notbid 318 . . . . . 6 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (¬ (abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
401400elrab3 3638 . . . . 5 (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
40221, 401syl 17 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
403 eleq2 2826 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 ↔ ((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
404 sseq2 3961 . . . . . . . 8 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
405404anbi2d 630 . . . . . . 7 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
406405rexbidv 3172 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
407403, 406imbi12d 345 . . . . 5 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))))
4089adantr 482 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑋) ∈ ℂ)
4091ffvelcdmda 7021 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℝ)
410131, 409syldan 592 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℝ)
411410recnd 11108 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℂ)
412408, 411subcld 11437 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑧)) ∈ ℂ)
413130, 134subcld 11437 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ)
414 eldifsn 4738 . . . . . . . . 9 (((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}) ↔ (((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ ∧ ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
415413, 220, 414sylanbrc 584 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}))
416 ssidd 3958 . . . . . . . 8 (𝜑 → ℂ ⊆ ℂ)
417 difss 4082 . . . . . . . . 9 (ℂ ∖ {0}) ⊆ ℂ
418417a1i 11 . . . . . . . 8 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
41946cnfldtopon 24051 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
420 cnex 11057 . . . . . . . . . 10 ℂ ∈ V
421420difexi 5276 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
422 txrest 22887 . . . . . . . . . 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}))))
423419, 419, 420, 421, 422mp4an 691 . . . . . . . . 9 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
424 unicntop 24054 . . . . . . . . . . . 12 ℂ = (TopOpen‘ℂfld)
425424restid 17241 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
426419, 425ax-mp 5 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
427426oveq1i 7351 . . . . . . . . 9 (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
428423, 427eqtr2i 2766 . . . . . . . 8 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0})))
4299subid1d 11426 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) = (𝐹𝑋))
430 txtopon 22847 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
431419, 419, 430mp2an 690 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
432431toponrestid 22175 . . . . . . . . . 10 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
433 limcresi 25154 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
434 ioossre 13245 . . . . . . . . . . . . . 14 (𝐴(,)𝑋) ⊆ ℝ
435 resmpt 5981 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)))
436434, 435ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋))
437436oveq1i 7351 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
438433, 437sseqtri 3971 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
439 cncfmptc 24180 . . . . . . . . . . . . 13 (((𝐹𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
4408, 154, 154, 439syl3anc 1371 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
441 eqidd 2738 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐹𝑋) = (𝐹𝑋))
442440, 39, 441cnmptlimc 25159 . . . . . . . . . . 11 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴))
443438, 442sselid 3933 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴))
444 limcresi 25154 . . . . . . . . . . . 12 (𝐹 lim 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴)
4451, 114feqresmpt 6898 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)))
446445oveq1d 7356 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
447444, 446sseqtrid 3987 . . . . . . . . . . 11 (𝜑 → (𝐹 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
448 lhop1.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
449447, 448sseldd 3936 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
45046subcn 24134 . . . . . . . . . . 11 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
451 0cn 11072 . . . . . . . . . . . 12 0 ∈ ℂ
452 opelxpi 5661 . . . . . . . . . . . 12 (((𝐹𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
4539, 451, 452sylancl 587 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
454431toponunii 22170 . . . . . . . . . . . 12 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
455454cncnpi 22534 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
456450, 453, 455sylancr 588 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
457408, 411, 416, 416, 46, 432, 443, 449, 456limccnp2 25161 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
458429, 457eqeltrrd 2839 . . . . . . . 8 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
45912subid1d 11426 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) = (𝐺𝑋))
460 limcresi 25154 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
461 resmpt 5981 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)))
462434, 461ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋))
463462oveq1i 7351 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
464460, 463sseqtri 3971 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
465 cncfmptc 24180 . . . . . . . . . . . . 13 (((𝐺𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
46611, 154, 154, 465syl3anc 1371 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
467 eqidd 2738 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐺𝑋) = (𝐺𝑋))
468466, 39, 467cnmptlimc 25159 . . . . . . . . . . 11 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴))
469464, 468sselid 3933 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴))
470 limcresi 25154 . . . . . . . . . . . 12 (𝐺 lim 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴)
47110, 114feqresmpt 6898 . . . . . . . . . . . . 13 (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)))
472471oveq1d 7356 . . . . . . . . . . . 12 (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
473470, 472sseqtrid 3987 . . . . . . . . . . 11 (𝜑 → (𝐺 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
474 lhop1.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
475473, 474sseldd 3936 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
476 opelxpi 5661 . . . . . . . . . . . 12 (((𝐺𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
47712, 451, 476sylancl 587 . . . . . . . . . . 11 (𝜑 → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
478454cncnpi 22534 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
479450, 477, 478sylancr 588 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
480130, 134, 416, 416, 46, 432, 469, 475, 479limccnp2 25161 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
481459, 480eqeltrrd 2839 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
482 eqid 2737 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
48346, 482divcn 24136 . . . . . . . . 9 / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld))
484 eldifsn 4738 . . . . . . . . . . 11 ((𝐺𝑋) ∈ (ℂ ∖ {0}) ↔ ((𝐺𝑋) ∈ ℂ ∧ (𝐺𝑋) ≠ 0))
48512, 20, 484sylanbrc 584 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ (ℂ ∖ {0}))
4869, 485opelxpd 5662 . . . . . . . . 9 (𝜑 → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
487 resttopon 22417 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
488419, 417, 487mp2an 690 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))
489 txtopon 22847 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))) → ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0}))))
490419, 488, 489mp2an 690 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0})))
491490toponunii 22170 . . . . . . . . . 10 (ℂ × (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
492491cncnpi 22534 . . . . . . . . 9 (( / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0}))) → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
493483, 486, 492sylancr 588 . . . . . . . 8 (𝜑 → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
494412, 415, 416, 418, 46, 428, 458, 481, 493limccnp2 25161 . . . . . . 7 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴))
495412, 413, 220divcld 11856 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ ℂ)
496495fmpttd 7049 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))):(𝐴(,)𝑋)⟶ℂ)
497434, 153sstri 3944 . . . . . . . . 9 (𝐴(,)𝑋) ⊆ ℂ
498497a1i 11 . . . . . . . 8 (𝜑 → (𝐴(,)𝑋) ⊆ ℂ)
499496, 498, 66, 46ellimc2 25146 . . . . . . 7 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))))
500494, 499mpbid 231 . . . . . 6 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))
501500simprd 497 . . . . 5 (𝜑 → ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))
502 notrab 4262 . . . . . 6 (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}
50368cnmetdval 24039 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶𝑥)))
504 abssub 15137 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (abs‘(𝐶𝑥)) = (abs‘(𝑥𝐶)))
505503, 504eqtrd 2777 . . . . . . . . . . 11 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
50624, 505sylan 581 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
507506breq1d 5106 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥𝐶)) ≤ 𝐸))
508507rabbidva 3411 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸})
50932a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51028rexrd 11130 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ*)
511 eqid 2737 . . . . . . . . . 10 {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸}
51247, 511blcld 23766 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
513509, 24, 510, 512syl3anc 1371 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
514508, 513eqeltrrd 2839 . . . . . . 7 (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
515424cldopn 22287 . . . . . . 7 ({𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
516514, 515syl 17 . . . . . 6 (𝜑 → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
517502, 516eqeltrrid 2843 . . . . 5 (𝜑 → {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (TopOpen‘ℂfld))
518407, 501, 517rspcdva 3574 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
519402, 518sylbird 260 . . 3 (𝜑 → (¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
520397, 519mt3d 148 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸)
52128recnd 11108 . . . 4 (𝜑𝐸 ∈ ℂ)
522521mulid2d 11098 . . 3 (𝜑 → (1 · 𝐸) = 𝐸)
523 1red 11081 . . . 4 (𝜑 → 1 ∈ ℝ)
524 1lt2 12249 . . . . 5 1 < 2
525524a1i 11 . . . 4 (𝜑 → 1 < 2)
526523, 30, 27, 525ltmul1dd 12932 . . 3 (𝜑 → (1 · 𝐸) < (2 · 𝐸))
527522, 526eqbrtrrd 5120 . 2 (𝜑𝐸 < (2 · 𝐸))
52826, 28, 31, 520, 527lelttrd 11238 1 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) < (2 · 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wcel 2106  wne 2941  wral 3062  wrex 3071  {crab 3404  Vcvv 3442  cdif 3898  cin 3900  wss 3901  c0 4273  {csn 4577  cop 4583   class class class wbr 5096  cmpt 5179   × cxp 5622  dom cdm 5624  ran crn 5625  cres 5626  cima 5627  ccom 5628   Fn wfn 6478  wf 6479  cfv 6483  (class class class)co 7341  cc 10974  cr 10975  0cc0 10976  1c1 10977   + caddc 10979   · cmul 10981  *cxr 11113   < clt 11114  cle 11115  cmin 11310   / cdiv 11737  2c2 12133  +crp 12835  (,)cioo 13184  [,]cicc 13187  abscabs 15044  t crest 17228  TopOpenctopn 17229  topGenctg 17245  ∞Metcxmet 20687  ballcbl 20689  fldccnfld 20702  TopOnctopon 22164  Clsdccld 22272  intcnt 22273   Cn ccn 22480   CnP ccnp 22481   ×t ctx 22816  cnccncf 24144   lim climc 25131   D cdv 25132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-cnex 11032  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053  ax-pre-sup 11054  ax-addf 11055  ax-mulf 11056
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4857  df-int 4899  df-iun 4947  df-iin 4948  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-se 5580  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-isom 6492  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-of 7599  df-om 7785  df-1st 7903  df-2nd 7904  df-supp 8052  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-2o 8372  df-er 8573  df-map 8692  df-pm 8693  df-ixp 8761  df-en 8809  df-dom 8810  df-sdom 8811  df-fin 8812  df-fsupp 9231  df-fi 9272  df-sup 9303  df-inf 9304  df-oi 9371  df-card 9800  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-div 11738  df-nn 12079  df-2 12141  df-3 12142  df-4 12143  df-5 12144  df-6 12145  df-7 12146  df-8 12147  df-9 12148  df-n0 12339  df-z 12425  df-dec 12543  df-uz 12688  df-q 12794  df-rp 12836  df-xneg 12953  df-xadd 12954  df-xmul 12955  df-ioo 13188  df-ico 13190  df-icc 13191  df-fz 13345  df-fzo 13488  df-seq 13827  df-exp 13888  df-hash 14150  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-submnd 18528  df-mulg 18797  df-cntz 19019  df-cmn 19483  df-psmet 20694  df-xmet 20695  df-met 20696  df-bl 20697  df-mopn 20698  df-fbas 20699  df-fg 20700  df-cnfld 20703  df-top 22148  df-topon 22165  df-topsp 22187  df-bases 22201  df-cld 22275  df-ntr 22276  df-cls 22277  df-nei 22354  df-lp 22392  df-perf 22393  df-cn 22483  df-cnp 22484  df-haus 22571  df-cmp 22643  df-tx 22818  df-hmeo 23011  df-fil 23102  df-fm 23194  df-flim 23195  df-flf 23196  df-xms 23578  df-ms 23579  df-tms 23580  df-cncf 24146  df-limc 25135  df-dv 25136
This theorem is referenced by:  lhop1  25283
  Copyright terms: Public domain W3C validator