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

Theorem lhop1lem 26007
Description: Lemma for lhop1 26008. (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 13400 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐷𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
52, 3, 4syl2anc 582 . . . . . . . 8 (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
6 lhop1lem.x . . . . . . . 8 (𝜑𝑋 ∈ (𝐴(,)𝐷))
75, 6sseldd 3977 . . . . . . 7 (𝜑𝑋 ∈ (𝐴(,)𝐵))
81, 7ffvelcdmd 7094 . . . . . 6 (𝜑 → (𝐹𝑋) ∈ ℝ)
98recnd 11279 . . . . 5 (𝜑 → (𝐹𝑋) ∈ ℂ)
10 lhop1.g . . . . . . 7 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
1110, 7ffvelcdmd 7094 . . . . . 6 (𝜑 → (𝐺𝑋) ∈ ℝ)
1211recnd 11279 . . . . 5 (𝜑 → (𝐺𝑋) ∈ ℂ)
13 lhop1.gn0 . . . . . 6 (𝜑 → ¬ 0 ∈ ran 𝐺)
1410ffnd 6724 . . . . . . . . 9 (𝜑𝐺 Fn (𝐴(,)𝐵))
15 fnfvelrn 7089 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺𝑋) ∈ ran 𝐺)
1614, 7, 15syl2anc 582 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ran 𝐺)
17 eleq1 2813 . . . . . . . 8 ((𝐺𝑋) = 0 → ((𝐺𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
1816, 17syl5ibcom 244 . . . . . . 7 (𝜑 → ((𝐺𝑋) = 0 → 0 ∈ ran 𝐺))
1918necon3bd 2943 . . . . . 6 (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺𝑋) ≠ 0))
2013, 19mpd 15 . . . . 5 (𝜑 → (𝐺𝑋) ≠ 0)
219, 12, 20divcld 12028 . . . 4 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ)
22 limccl 25865 . . . . 5 ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) ⊆ ℂ
23 lhop1.c . . . . 5 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
2422, 23sselid 3974 . . . 4 (𝜑𝐶 ∈ ℂ)
2521, 24subcld 11608 . . 3 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) − 𝐶) ∈ ℂ)
2625abscld 15427 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ∈ ℝ)
27 lhop1lem.e . . 3 (𝜑𝐸 ∈ ℝ+)
2827rpred 13056 . 2 (𝜑𝐸 ∈ ℝ)
29 2re 12324 . . . 4 2 ∈ ℝ
3029a1i 11 . . 3 (𝜑 → 2 ∈ ℝ)
3130, 28remulcld 11281 . 2 (𝜑 → (2 · 𝐸) ∈ ℝ)
32 cnxmet 24750 . . . . . . . . . . . . 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 13423 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋𝑋 < 𝐷))
376, 36syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < 𝑋𝑋 < 𝐷))
3837simpld 493 . . . . . . . . . . . . . 14 (𝜑𝐴 < 𝑋)
39 lhop1.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
40 ioossre 13425 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐷) ⊆ ℝ
4140, 6sselid 3974 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
42 difrp 13052 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4339, 41, 42syl2anc 582 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4438, 43mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐴) ∈ ℝ+)
4544adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (𝑋𝐴) ∈ ℝ+)
46 eqid 2725 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4746cnfldtopn 24759 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
4847mopni3 24464 . . . . . . . . . . . 12 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣) ∧ (𝑋𝐴) ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
4933, 34, 35, 45, 48syl31anc 1370 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
50 ssrin 4232 . . . . . . . . . . . . . . . 16 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋)))
51 lbioo 13395 . . . . . . . . . . . . . . . . . . 19 ¬ 𝐴 ∈ (𝐴(,)𝑋)
52 disjsn 4717 . . . . . . . . . . . . . . . . . . 19 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋))
5351, 52mpbir 230 . . . . . . . . . . . . . . . . . 18 ((𝐴(,)𝑋) ∩ {𝐴}) = ∅
54 disj3 4455 . . . . . . . . . . . . . . . . . 18 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}))
5553, 54mpbi 229 . . . . . . . . . . . . . . . . 17 (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})
5655ineq2i 4207 . . . . . . . . . . . . . . . 16 (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))
5750, 56sseqtrdi 4027 . . . . . . . . . . . . . . 15 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))
58 lhop1lem.r . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 = (𝐴 + (𝑟 / 2))
5939adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ)
60 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ+)
6160rpred 13056 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ)
6261rehalfcld 12497 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
6359, 62readdcld 11280 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ)
6458, 63eqeltrid 2829 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ)
6564recnd 11279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℂ)
6639recnd 11279 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℂ)
6766adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℂ)
68 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
6968cnmetdval 24748 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
7065, 67, 69syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
7158oveq1i 7429 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴)
7261recnd 11279 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℂ)
7372halfcld 12495 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℂ)
7467, 73pncan2d 11610 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2))
7571, 74eqtrid 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅𝐴) = (𝑟 / 2))
7675fveq2d 6900 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑅𝐴)) = (abs‘(𝑟 / 2)))
7760rphalfcld 13068 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ+)
7877rpred 13056 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
7977rpge0d 13060 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 0 ≤ (𝑟 / 2))
8078, 79absidd 15413 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
8170, 76, 803eqtrd 2769 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2))
82 rphalflt 13043 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+ → (𝑟 / 2) < 𝑟)
8360, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < 𝑟)
8481, 83eqbrtrd 5171 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟)
8532a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
8661rexrd 11301 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ*)
87 elbl3 24359 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8885, 86, 67, 65, 87syl22anc 837 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8984, 88mpbird 256 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟))
9059, 77ltaddrpd 13089 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2)))
9190, 58breqtrrdi 5191 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < 𝑅)
9241adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ)
9392, 59resubcld 11679 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑋𝐴) ∈ ℝ)
94 simprr 771 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 < (𝑋𝐴))
9578, 61, 93, 83, 94lttrd 11412 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < (𝑋𝐴))
9659, 78, 92ltaddsub2d 11852 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋𝐴)))
9795, 96mpbird 256 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋)
9858, 97eqbrtrid 5184 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 < 𝑋)
9959rexrd 11301 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ*)
10041rexrd 11301 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
101100adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ*)
102 elioo2 13405 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝑋 ∈ ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
10399, 101, 102syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
10464, 91, 98, 103mpbir3and 1339 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝑋))
10589, 104elind 4192 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)))
1069adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑋) ∈ ℂ)
1071adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
108 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ∈ ℝ)
109108rexrd 11301 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℝ*)
11037simprd 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋 < 𝐷)
11141, 108, 110ltled 11399 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑋𝐷)
112100, 109, 2, 111, 3xrletrd 13181 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
113 iooss2 13400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ ℝ*𝑋𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
1142, 112, 113syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
115114adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
116115, 104sseldd 3977 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝐵))
117107, 116ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℝ)
118117recnd 11279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℂ)
119106, 118subcld 11608 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
12012adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑋) ∈ ℂ)
12110adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
122121, 116ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℝ)
123122recnd 11279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℂ)
124120, 123subcld 11608 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
125 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑅 → (𝐺𝑧) = (𝐺𝑅))
126125oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑅 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑅)))
127126neeq1d 2989 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑅 → (((𝐺𝑋) − (𝐺𝑧)) ≠ 0 ↔ ((𝐺𝑋) − (𝐺𝑅)) ≠ 0))
128 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
129128adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
13012adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑋) ∈ ℂ)
131114sselda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵))
13210ffvelcdmda 7093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℝ)
133131, 132syldan 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℝ)
134133recnd 11279 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℂ)
135130, 134subeq0ad 11618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 ↔ (𝐺𝑋) = (𝐺𝑧)))
136 ioossre 13425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴(,)𝐵) ⊆ ℝ
137136, 131sselid 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ)
138137adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 ∈ ℝ)
13941ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑋 ∈ ℝ)
140 eliooord 13423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧𝑧 < 𝑋))
141140adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧𝑧 < 𝑋))
142141simprd 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋)
143142adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 < 𝑋)
14439rexrd 11301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐴 ∈ ℝ*)
145144adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈ ℝ*)
1462adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈ ℝ*)
147141simpld 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧)
148100, 109, 2, 110, 3xrltletrd 13180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑋 < 𝐵)
149148adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵)
150 iccssioo 13433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝑧𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
151145, 146, 147, 149, 150syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
152151adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
153 ax-resscn 11202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℝ ⊆ ℂ
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ℝ ⊆ ℂ)
155 fss 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
15610, 153, 155sylancl 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
157136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
158 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
159 dvcn 25912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
160154, 156, 157, 158, 159syl31anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
161 cncfcdm 24879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ℝ ⊆ ℂ ∧ 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
162153, 160, 161sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
16310, 162mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
164163ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
165 rescncf 24878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)))
166152, 164, 165sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))
167153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ℝ ⊆ ℂ)
168156ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
169136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐴(,)𝐵) ⊆ ℝ)
170152, 136sstrdi 3989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ ℝ)
17146tgioo2 24780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
17246, 171dvres 25901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
173167, 168, 169, 170, 172syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
174 iccntr 24798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
175138, 139, 174syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
176175reseq2d 5985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
177173, 176eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
178177dmeqd 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
179 ioossicc 13450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋)
180179, 152sstrid 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵))
181158ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
182180, 181sseqtrrd 4018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺))
183 ssdmres 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
184182, 183sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
185178, 184eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋))
186137rexrd 11301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*)
187100adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ*)
18841adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ)
189137, 188, 142ltled 11399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧𝑋)
190 ubicc2 13482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑋 ∈ (𝑧[,]𝑋))
191186, 187, 189, 190syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋))
192191fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
193 lbicc2 13481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑧 ∈ (𝑧[,]𝑋))
194186, 187, 189, 193syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋))
195194fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
196192, 195eqeq12d 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺𝑋) = (𝐺𝑧)))
197196biimpar 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧))
198197eqcomd 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋))
199138, 139, 143, 166, 185, 198rolle 25983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0)
200177fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤))
201 fvres 6915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
202200, 201sylan9eq 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
203 dvf 25897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
204158feq2d 6709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
205203, 204mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
206205ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
207206ffnd 6724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
208207adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
209180sselda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
210 fnfvelrn 7089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
211208, 209, 210syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
212202, 211eqeltrd 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺))
213 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
214212, 213syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
215214rexlimdva 3144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
216199, 215mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 0 ∈ ran (ℝ D 𝐺))
217216ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) = (𝐺𝑧) → 0 ∈ ran (ℝ D 𝐺)))
218135, 217sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺)))
219218necon3bd 2943 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
220129, 219mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
221220ralrimiva 3135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
222221adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
223127, 222, 104rspcdva 3607 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
224119, 124, 223divcld 12028 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) ∈ ℂ)
22524adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐶 ∈ ℂ)
226224, 225subcld 11608 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶) ∈ ℂ)
227226abscld 15427 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ∈ ℝ)
22828adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐸 ∈ ℝ)
229109adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐷 ∈ ℝ*)
230110adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 < 𝐷)
231 iccssioo 13433 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ*𝐷 ∈ ℝ*) ∧ (𝐴 < 𝑅𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
23299, 229, 91, 230, 231syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
2335adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
234232, 233sstrd 3987 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵))
235 fss 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
2361, 153, 235sylancl 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
237 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
238 dvcn 25912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
239154, 236, 157, 237, 238syl31anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
240 cncfcdm 24879 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
241153, 239, 240sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
2421, 241mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
243242adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
244 rescncf 24878 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
245234, 243, 244sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
246163adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
247 rescncf 24878 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
248234, 246, 247sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
249153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ℝ ⊆ ℂ)
250236adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
251136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐵) ⊆ ℝ)
252 iccssre 13446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ)
25364, 92, 252syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ ℝ)
25446, 171dvres 25901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
255249, 250, 251, 253, 254syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
256 iccntr 24798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
25764, 92, 256syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
258257reseq2d 5985 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
259255, 258eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
260259dmeqd 5908 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
26159, 64, 91ltled 11399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴𝑅)
262 iooss1 13399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝐴𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
26399, 261, 262syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
264111adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋𝐷)
265 iooss2 13400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐷 ∈ ℝ*𝑋𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
266229, 264, 265syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
267263, 266sstrd 3987 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷))
268267, 233sstrd 3987 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵))
269237adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
270268, 269sseqtrrd 4018 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹))
271 ssdmres 6018 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
272270, 271sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
273260, 272eqtrd 2765 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
274156adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
27546, 171dvres 25901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
276249, 274, 251, 253, 275syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
277257reseq2d 5985 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
278276, 277eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
279278dmeqd 5908 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
280158adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
281268, 280sseqtrrd 4018 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺))
282 ssdmres 6018 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
283281, 282sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
284279, 283eqtrd 2765 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
28564, 92, 98, 245, 248, 273, 284cmvth 25984 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)))
28664rexrd 11301 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ*)
287286adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ ℝ*)
288100ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ ℝ*)
28964, 92, 98ltled 11399 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅𝑋)
290289adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅𝑋)
291 ubicc2 13482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑋 ∈ (𝑅[,]𝑋))
292287, 288, 290, 291syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋))
293292fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
294 lbicc2 13481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑅 ∈ (𝑅[,]𝑋))
295287, 288, 290, 294syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋))
296295fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
297293, 296oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹𝑋) − (𝐹𝑅)))
298278fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤))
299 fvres 6915 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
300298, 299sylan9eq 2785 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
301297, 300oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)))
302292fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
303295fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
304302, 303oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺𝑋) − (𝐺𝑅)))
305259fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤))
306 fvres 6915 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
307305, 306sylan9eq 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
308304, 307oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)))
309124adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
310 dvf 25897 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
311237feq2d 6709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
312310, 311mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
313312ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
314268sselda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
315313, 314ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ)
316309, 315mulcomd 11272 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
317308, 316eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
318301, 317eqeq12d 2741 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
319119adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
320205ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
321320, 314ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ)
322223adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
323128ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
324320ffnd 6724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
325324, 314, 210syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
326 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
327325, 326syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
328327necon3bd 2943 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0))
329323, 328mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0)
330319, 309, 315, 321, 322, 329divmuleqd 12074 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
331318, 330bitr4d 281 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
332331rexbidva 3166 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
333285, 332mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
334 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤))
335 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤))
336334, 335oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
337336fvoveq1d 7441 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
338337breq1d 5159 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
339 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
340339ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
341267sselda 3976 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷))
342338, 340, 341rspcdva 3607 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)
343 fvoveq1 7442 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
344343breq1d 5159 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
345342, 344syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
346345rexlimdva 3144 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
347333, 346mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸)
348227, 228, 347ltled 11399 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸)
349 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐹𝑢) = (𝐹𝑅))
350349oveq2d 7435 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐹𝑋) − (𝐹𝑢)) = ((𝐹𝑋) − (𝐹𝑅)))
351 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐺𝑢) = (𝐺𝑅))
352351oveq2d 7435 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐺𝑋) − (𝐺𝑢)) = ((𝐺𝑋) − (𝐺𝑅)))
353350, 352oveq12d 7437 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑅 → (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) = (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))))
354353fvoveq1d 7441 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑅 → (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)))
355354breq1d 5159 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑅 → ((abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸))
356355rspcev 3606 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
357105, 348, 356syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
358357adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
359 ssrexv 4046 . . . . . . . . . . . . . . 15 (((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
36057, 358, 359syl2imc 41 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
361360anassrs 466 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
362361expimpd 452 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
363362rexlimdva 3144 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
36449, 363mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
365 inss2 4228 . . . . . . . . . . . . . 14 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴})
366 difss 4128 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋)
367365, 366sstri 3986 . . . . . . . . . . . . 13 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)
368367sseli 3972 . . . . . . . . . . . 12 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋))
369 fveq2 6896 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐹𝑧) = (𝐹𝑢))
370369oveq2d 7435 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐹𝑋) − (𝐹𝑧)) = ((𝐹𝑋) − (𝐹𝑢)))
371 fveq2 6896 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐺𝑧) = (𝐺𝑢))
372371oveq2d 7435 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑢)))
373370, 372oveq12d 7437 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
374 eqid 2725 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))
375 ovex 7452 . . . . . . . . . . . . . . 15 (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) ∈ V
376373, 374, 375fvmpt 7004 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
377376fvoveq1d 7441 . . . . . . . . . . . . 13 (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)))
378377breq1d 5159 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
379368, 378syl 17 . . . . . . . . . . 11 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
380379rexbiia 3081 . . . . . . . . . 10 (∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
381364, 380sylibr 233 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
382 ovex 7452 . . . . . . . . . . 11 (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ V
383382, 374fnmpti 6699 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋)
384 fvoveq1 7442 . . . . . . . . . . . 12 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → (abs‘(𝑥𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)))
385384breq1d 5159 . . . . . . . . . . 11 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
386385rexima 7249 . . . . . . . . . 10 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
387383, 367, 386mp2an 690 . . . . . . . . 9 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
388381, 387sylibr 233 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸)
389 dfrex2 3062 . . . . . . . 8 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
390388, 389sylib 217 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
391 ssrab 4066 . . . . . . . 8 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸))
392391simprbi 495 . . . . . . 7 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
393390, 392nsyl 140 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})
394393expr 455 . . . . 5 ((𝜑𝑣 ∈ (TopOpen‘ℂfld)) → (𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
395394ralrimiva 3135 . . . 4 (𝜑 → ∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
396 ralinexa 3090 . . . 4 (∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
397395, 396sylib 217 . . 3 (𝜑 → ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
398 fvoveq1 7442 . . . . . . . 8 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (abs‘(𝑥𝐶)) = (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)))
399398breq1d 5159 . . . . . . 7 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
400399notbid 317 . . . . . 6 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (¬ (abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
401400elrab3 3680 . . . . 5 (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
40221, 401syl 17 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
403 eleq2 2814 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 ↔ ((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
404 sseq2 4003 . . . . . . . 8 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
405404anbi2d 628 . . . . . . 7 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
406405rexbidv 3168 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
407403, 406imbi12d 343 . . . . 5 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))))
4089adantr 479 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑋) ∈ ℂ)
4091ffvelcdmda 7093 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℝ)
410131, 409syldan 589 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℝ)
411410recnd 11279 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℂ)
412408, 411subcld 11608 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑧)) ∈ ℂ)
413130, 134subcld 11608 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ)
414 eldifsn 4792 . . . . . . . . 9 (((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}) ↔ (((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ ∧ ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
415413, 220, 414sylanbrc 581 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}))
416 ssidd 4000 . . . . . . . 8 (𝜑 → ℂ ⊆ ℂ)
417 difss 4128 . . . . . . . . 9 (ℂ ∖ {0}) ⊆ ℂ
418417a1i 11 . . . . . . . 8 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
41946cnfldtopon 24760 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
420 cnex 11226 . . . . . . . . . 10 ℂ ∈ V
421420difexi 5331 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
422 txrest 23596 . . . . . . . . . 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 24763 . . . . . . . . . . . 12 ℂ = (TopOpen‘ℂfld)
425424restid 17434 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
426419, 425ax-mp 5 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
427426oveq1i 7429 . . . . . . . . 9 (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
428423, 427eqtr2i 2754 . . . . . . . 8 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0})))
4299subid1d 11597 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) = (𝐹𝑋))
430 txtopon 23556 . . . . . . . . . . . 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 22884 . . . . . . . . . 10 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
433 limcresi 25875 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
434 ioossre 13425 . . . . . . . . . . . . . 14 (𝐴(,)𝑋) ⊆ ℝ
435 resmpt 6042 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)))
436434, 435ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋))
437436oveq1i 7429 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
438433, 437sseqtri 4013 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
439 cncfmptc 24893 . . . . . . . . . . . . 13 (((𝐹𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
4408, 154, 154, 439syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
441 eqidd 2726 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐹𝑋) = (𝐹𝑋))
442440, 39, 441cnmptlimc 25880 . . . . . . . . . . 11 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴))
443438, 442sselid 3974 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴))
444 limcresi 25875 . . . . . . . . . . . 12 (𝐹 lim 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴)
4451, 114feqresmpt 6967 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)))
446445oveq1d 7434 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
447444, 446sseqtrid 4029 . . . . . . . . . . 11 (𝜑 → (𝐹 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
448 lhop1.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
449447, 448sseldd 3977 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
45046subcn 24843 . . . . . . . . . . 11 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
451 0cn 11243 . . . . . . . . . . . 12 0 ∈ ℂ
452 opelxpi 5715 . . . . . . . . . . . 12 (((𝐹𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
4539, 451, 452sylancl 584 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
454431toponunii 22879 . . . . . . . . . . . 12 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
455454cncnpi 23243 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
456450, 453, 455sylancr 585 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
457408, 411, 416, 416, 46, 432, 443, 449, 456limccnp2 25882 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
458429, 457eqeltrrd 2826 . . . . . . . 8 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
45912subid1d 11597 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) = (𝐺𝑋))
460 limcresi 25875 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
461 resmpt 6042 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)))
462434, 461ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋))
463462oveq1i 7429 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
464460, 463sseqtri 4013 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
465 cncfmptc 24893 . . . . . . . . . . . . 13 (((𝐺𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
46611, 154, 154, 465syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
467 eqidd 2726 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐺𝑋) = (𝐺𝑋))
468466, 39, 467cnmptlimc 25880 . . . . . . . . . . 11 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴))
469464, 468sselid 3974 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴))
470 limcresi 25875 . . . . . . . . . . . 12 (𝐺 lim 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴)
47110, 114feqresmpt 6967 . . . . . . . . . . . . 13 (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)))
472471oveq1d 7434 . . . . . . . . . . . 12 (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
473470, 472sseqtrid 4029 . . . . . . . . . . 11 (𝜑 → (𝐺 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
474 lhop1.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
475473, 474sseldd 3977 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
476 opelxpi 5715 . . . . . . . . . . . 12 (((𝐺𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
47712, 451, 476sylancl 584 . . . . . . . . . . 11 (𝜑 → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
478454cncnpi 23243 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
479450, 477, 478sylancr 585 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
480130, 134, 416, 416, 46, 432, 469, 475, 479limccnp2 25882 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
481459, 480eqeltrrd 2826 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
482 eqid 2725 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
48346, 482divcn 24847 . . . . . . . . 9 / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld))
484 eldifsn 4792 . . . . . . . . . . 11 ((𝐺𝑋) ∈ (ℂ ∖ {0}) ↔ ((𝐺𝑋) ∈ ℂ ∧ (𝐺𝑋) ≠ 0))
48512, 20, 484sylanbrc 581 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ (ℂ ∖ {0}))
4869, 485opelxpd 5717 . . . . . . . . 9 (𝜑 → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
487 resttopon 23126 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
488419, 417, 487mp2an 690 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))
489 txtopon 23556 . . . . . . . . . . . 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 22879 . . . . . . . . . 10 (ℂ × (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
492491cncnpi 23243 . . . . . . . . 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 585 . . . . . . . 8 (𝜑 → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
494412, 415, 416, 418, 46, 428, 458, 481, 493limccnp2 25882 . . . . . . 7 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴))
495412, 413, 220divcld 12028 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ ℂ)
496495fmpttd 7124 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))):(𝐴(,)𝑋)⟶ℂ)
497434, 153sstri 3986 . . . . . . . . 9 (𝐴(,)𝑋) ⊆ ℂ
498497a1i 11 . . . . . . . 8 (𝜑 → (𝐴(,)𝑋) ⊆ ℂ)
499496, 498, 66, 46ellimc2 25867 . . . . . . 7 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))))
500494, 499mpbid 231 . . . . . 6 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))
501500simprd 494 . . . . 5 (𝜑 → ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))
502 notrab 4311 . . . . . 6 (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}
50368cnmetdval 24748 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶𝑥)))
504 abssub 15317 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (abs‘(𝐶𝑥)) = (abs‘(𝑥𝐶)))
505503, 504eqtrd 2765 . . . . . . . . . . 11 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
50624, 505sylan 578 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
507506breq1d 5159 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥𝐶)) ≤ 𝐸))
508507rabbidva 3425 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸})
50932a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51028rexrd 11301 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ*)
511 eqid 2725 . . . . . . . . . 10 {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸}
51247, 511blcld 24475 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
513509, 24, 510, 512syl3anc 1368 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
514508, 513eqeltrrd 2826 . . . . . . 7 (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
515424cldopn 22996 . . . . . . 7 ({𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
516514, 515syl 17 . . . . . 6 (𝜑 → (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) ∈ (TopOpen‘ℂfld))
517502, 516eqeltrrid 2830 . . . . 5 (𝜑 → {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (TopOpen‘ℂfld))
518407, 501, 517rspcdva 3607 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
519402, 518sylbird 259 . . 3 (𝜑 → (¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
520397, 519mt3d 148 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸)
52128recnd 11279 . . . 4 (𝜑𝐸 ∈ ℂ)
522521mullidd 11269 . . 3 (𝜑 → (1 · 𝐸) = 𝐸)
523 1red 11252 . . . 4 (𝜑 → 1 ∈ ℝ)
524 1lt2 12421 . . . . 5 1 < 2
525524a1i 11 . . . 4 (𝜑 → 1 < 2)
526523, 30, 27, 525ltmul1dd 13111 . . 3 (𝜑 → (1 · 𝐸) < (2 · 𝐸))
527522, 526eqbrtrrd 5173 . 2 (𝜑𝐸 < (2 · 𝐸))
52826, 28, 31, 520, 527lelttrd 11409 1 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) < (2 · 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  {crab 3418  Vcvv 3461  cdif 3941  cin 3943  wss 3944  c0 4322  {csn 4630  cop 4636   class class class wbr 5149  cmpt 5232   × cxp 5676  dom cdm 5678  ran crn 5679  cres 5680  cima 5681  ccom 5682   Fn wfn 6544  wf 6545  cfv 6549  (class class class)co 7419  cc 11143  cr 11144  0cc0 11145  1c1 11146   + caddc 11148   · cmul 11150  *cxr 11284   < clt 11285  cle 11286  cmin 11481   / cdiv 11908  2c2 12305  +crp 13014  (,)cioo 13364  [,]cicc 13367  abscabs 15225  t crest 17421  TopOpenctopn 17422  topGenctg 17438  ∞Metcxmet 21298  ballcbl 21300  fldccnfld 21313  TopOnctopon 22873  Clsdccld 22981  intcnt 22982   Cn ccn 23189   CnP ccnp 23190   ×t ctx 23525  cnccncf 24857   lim climc 25852   D cdv 25853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223  ax-addf 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9393  df-fi 9441  df-sup 9472  df-inf 9473  df-oi 9540  df-card 9969  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-seq 14008  df-exp 14068  df-hash 14334  df-cj 15090  df-re 15091  df-im 15092  df-sqrt 15226  df-abs 15227  df-struct 17135  df-sets 17152  df-slot 17170  df-ndx 17182  df-base 17200  df-ress 17229  df-plusg 17265  df-mulr 17266  df-starv 17267  df-sca 17268  df-vsca 17269  df-ip 17270  df-tset 17271  df-ple 17272  df-ds 17274  df-unif 17275  df-hom 17276  df-cco 17277  df-rest 17423  df-topn 17424  df-0g 17442  df-gsum 17443  df-topgen 17444  df-pt 17445  df-prds 17448  df-xrs 17503  df-qtop 17508  df-imas 17509  df-xps 17511  df-mre 17585  df-mrc 17586  df-acs 17588  df-mgm 18619  df-sgrp 18698  df-mnd 18714  df-submnd 18760  df-mulg 19048  df-cntz 19297  df-cmn 19766  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-fbas 21310  df-fg 21311  df-cnfld 21314  df-top 22857  df-topon 22874  df-topsp 22896  df-bases 22910  df-cld 22984  df-ntr 22985  df-cls 22986  df-nei 23063  df-lp 23101  df-perf 23102  df-cn 23192  df-cnp 23193  df-haus 23280  df-cmp 23352  df-tx 23527  df-hmeo 23720  df-fil 23811  df-fm 23903  df-flim 23904  df-flf 23905  df-xms 24287  df-ms 24288  df-tms 24289  df-cncf 24859  df-limc 25856  df-dv 25857
This theorem is referenced by:  lhop1  26008
  Copyright terms: Public domain W3C validator