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

Theorem lhop1lem 26066
Description: Lemma for lhop1 26067. (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 13419 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐷𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
52, 3, 4syl2anc 584 . . . . . . . 8 (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
6 lhop1lem.x . . . . . . . 8 (𝜑𝑋 ∈ (𝐴(,)𝐷))
75, 6sseldd 3995 . . . . . . 7 (𝜑𝑋 ∈ (𝐴(,)𝐵))
81, 7ffvelcdmd 7104 . . . . . 6 (𝜑 → (𝐹𝑋) ∈ ℝ)
98recnd 11286 . . . . 5 (𝜑 → (𝐹𝑋) ∈ ℂ)
10 lhop1.g . . . . . . 7 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
1110, 7ffvelcdmd 7104 . . . . . 6 (𝜑 → (𝐺𝑋) ∈ ℝ)
1211recnd 11286 . . . . 5 (𝜑 → (𝐺𝑋) ∈ ℂ)
13 lhop1.gn0 . . . . . 6 (𝜑 → ¬ 0 ∈ ran 𝐺)
1410ffnd 6737 . . . . . . . . 9 (𝜑𝐺 Fn (𝐴(,)𝐵))
15 fnfvelrn 7099 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺𝑋) ∈ ran 𝐺)
1614, 7, 15syl2anc 584 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ran 𝐺)
17 eleq1 2826 . . . . . . . 8 ((𝐺𝑋) = 0 → ((𝐺𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
1816, 17syl5ibcom 245 . . . . . . 7 (𝜑 → ((𝐺𝑋) = 0 → 0 ∈ ran 𝐺))
1918necon3bd 2951 . . . . . 6 (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺𝑋) ≠ 0))
2013, 19mpd 15 . . . . 5 (𝜑 → (𝐺𝑋) ≠ 0)
219, 12, 20divcld 12040 . . . 4 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ)
22 limccl 25924 . . . . 5 ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) ⊆ ℂ
23 lhop1.c . . . . 5 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
2422, 23sselid 3992 . . . 4 (𝜑𝐶 ∈ ℂ)
2521, 24subcld 11617 . . 3 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) − 𝐶) ∈ ℂ)
2625abscld 15471 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ∈ ℝ)
27 lhop1lem.e . . 3 (𝜑𝐸 ∈ ℝ+)
2827rpred 13074 . 2 (𝜑𝐸 ∈ ℝ)
29 2re 12337 . . . 4 2 ∈ ℝ
3029a1i 11 . . 3 (𝜑 → 2 ∈ ℝ)
3130, 28remulcld 11288 . 2 (𝜑 → (2 · 𝐸) ∈ ℝ)
32 cnxmet 24808 . . . . . . . . . . . . 13 (abs ∘ − ) ∈ (∞Met‘ℂ)
3332a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
34 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝑣 ∈ (TopOpen‘ℂfld))
35 simprr 773 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → 𝐴𝑣)
36 eliooord 13442 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋𝑋 < 𝐷))
376, 36syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < 𝑋𝑋 < 𝐷))
3837simpld 494 . . . . . . . . . . . . . 14 (𝜑𝐴 < 𝑋)
39 lhop1.a . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
40 ioossre 13444 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐷) ⊆ ℝ
4140, 6sselid 3992 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
42 difrp 13070 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4339, 41, 42syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 < 𝑋 ↔ (𝑋𝐴) ∈ ℝ+))
4438, 43mpbid 232 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐴) ∈ ℝ+)
4544adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (𝑋𝐴) ∈ ℝ+)
46 eqid 2734 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4746cnfldtopn 24817 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
4847mopni3 24522 . . . . . . . . . . . 12 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣) ∧ (𝑋𝐴) ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
4933, 34, 35, 45, 48syl31anc 1372 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣))
50 ssrin 4249 . . . . . . . . . . . . . . . 16 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋)))
51 lbioo 13414 . . . . . . . . . . . . . . . . . . 19 ¬ 𝐴 ∈ (𝐴(,)𝑋)
52 disjsn 4715 . . . . . . . . . . . . . . . . . . 19 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋))
5351, 52mpbir 231 . . . . . . . . . . . . . . . . . 18 ((𝐴(,)𝑋) ∩ {𝐴}) = ∅
54 disj3 4459 . . . . . . . . . . . . . . . . . 18 (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}))
5553, 54mpbi 230 . . . . . . . . . . . . . . . . 17 (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})
5655ineq2i 4224 . . . . . . . . . . . . . . . 16 (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))
5750, 56sseqtrdi 4045 . . . . . . . . . . . . . . 15 ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))
58 lhop1lem.r . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 = (𝐴 + (𝑟 / 2))
5939adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ)
60 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ+)
6160rpred 13074 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ)
6261rehalfcld 12510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
6359, 62readdcld 11287 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ)
6458, 63eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ)
6564recnd 11286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℂ)
6639recnd 11286 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℂ)
6766adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℂ)
68 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
6968cnmetdval 24806 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
7065, 67, 69syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅𝐴)))
7158oveq1i 7440 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴)
7261recnd 11286 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℂ)
7372halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℂ)
7467, 73pncan2d 11619 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2))
7571, 74eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅𝐴) = (𝑟 / 2))
7675fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑅𝐴)) = (abs‘(𝑟 / 2)))
7760rphalfcld 13086 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ+)
7877rpred 13074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) ∈ ℝ)
7977rpge0d 13078 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 0 ≤ (𝑟 / 2))
8078, 79absidd 15457 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
8170, 76, 803eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2))
82 rphalflt 13061 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+ → (𝑟 / 2) < 𝑟)
8360, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < 𝑟)
8481, 83eqbrtrd 5169 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟)
8532a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
8661rexrd 11308 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 ∈ ℝ*)
87 elbl3 24417 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8885, 86, 67, 65, 87syl22anc 839 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟))
8984, 88mpbird 257 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟))
9059, 77ltaddrpd 13107 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2)))
9190, 58breqtrrdi 5189 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 < 𝑅)
9241adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ)
9392, 59resubcld 11688 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑋𝐴) ∈ ℝ)
94 simprr 773 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑟 < (𝑋𝐴))
9578, 61, 93, 83, 94lttrd 11419 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑟 / 2) < (𝑋𝐴))
9659, 78, 92ltaddsub2d 11861 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋𝐴)))
9795, 96mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋)
9858, 97eqbrtrid 5182 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 < 𝑋)
9959rexrd 11308 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴 ∈ ℝ*)
10041rexrd 11308 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
101100adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 ∈ ℝ*)
102 elioo2 13424 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝑋 ∈ ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
10399, 101, 102syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅𝑅 < 𝑋)))
10464, 91, 98, 103mpbir3and 1341 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝑋))
10589, 104elind 4209 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)))
1069adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑋) ∈ ℂ)
1071adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
108 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ∈ ℝ)
109108rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℝ*)
11037simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋 < 𝐷)
11141, 108, 110ltled 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑋𝐷)
112100, 109, 2, 111, 3xrletrd 13200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
113 iooss2 13419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ ℝ*𝑋𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
1142, 112, 113syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
115114adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵))
116115, 104sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ (𝐴(,)𝐵))
117107, 116ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℝ)
118117recnd 11286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹𝑅) ∈ ℂ)
119106, 118subcld 11617 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
12012adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑋) ∈ ℂ)
12110adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
122121, 116ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℝ)
123122recnd 11286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺𝑅) ∈ ℂ)
124120, 123subcld 11617 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
125 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑅 → (𝐺𝑧) = (𝐺𝑅))
126125oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑅 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑅)))
127126neeq1d 2997 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑅 → (((𝐺𝑋) − (𝐺𝑧)) ≠ 0 ↔ ((𝐺𝑋) − (𝐺𝑅)) ≠ 0))
128 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
129128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
13012adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑋) ∈ ℂ)
131114sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵))
13210ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℝ)
133131, 132syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℝ)
134133recnd 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐺𝑧) ∈ ℂ)
135130, 134subeq0ad 11627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 ↔ (𝐺𝑋) = (𝐺𝑧)))
136 ioossre 13444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴(,)𝐵) ⊆ ℝ
137136, 131sselid 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ)
138137adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 ∈ ℝ)
13941ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑋 ∈ ℝ)
140 eliooord 13442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧𝑧 < 𝑋))
141140adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧𝑧 < 𝑋))
142141simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋)
143142adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝑧 < 𝑋)
14439rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐴 ∈ ℝ*)
145144adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈ ℝ*)
1462adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈ ℝ*)
147141simpld 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧)
148100, 109, 2, 110, 3xrltletrd 13199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑋 < 𝐵)
149148adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵)
150 iccssioo 13452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴 < 𝑧𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
151145, 146, 147, 149, 150syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
152151adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵))
153 ax-resscn 11209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℝ ⊆ ℂ
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ℝ ⊆ ℂ)
155 fss 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
15610, 153, 155sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
157136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
158 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
159 dvcn 25971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
160154, 156, 157, 158, 159syl31anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
161 cncfcdm 24937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ℝ ⊆ ℂ ∧ 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
162153, 160, 161sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ))
16310, 162mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
164163ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
165 rescncf 24936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)))
166152, 164, 165sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))
167153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ℝ ⊆ ℂ)
168156ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
169136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝐴(,)𝐵) ⊆ ℝ)
170152, 136sstrdi 4007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧[,]𝑋) ⊆ ℝ)
17146tgioo2 24838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
17246, 171dvres 25960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
173167, 168, 169, 170, 172syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))))
174 iccntr 24856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
175138, 139, 174syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋))
176175reseq2d 5999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
177173, 176eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
178177dmeqd 5918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)))
179 ioossicc 13469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋)
180179, 152sstrid 4006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵))
181158ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
182180, 181sseqtrrd 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺))
183 ssdmres 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
184182, 183sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋))
185178, 184eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋))
186137rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*)
187100adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ*)
18841adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ)
189137, 188, 142ltled 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧𝑋)
190 ubicc2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑋 ∈ (𝑧[,]𝑋))
191186, 187, 189, 190syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋))
192191fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺𝑋))
193 lbicc2 13500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ ℝ*𝑋 ∈ ℝ*𝑧𝑋) → 𝑧 ∈ (𝑧[,]𝑋))
194186, 187, 189, 193syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋))
195194fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺𝑧))
196192, 195eqeq12d 2750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺𝑋) = (𝐺𝑧)))
197196biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧))
198197eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋))
199138, 139, 143, 166, 185, 198rolle 26042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0)
200177fveq1d 6908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤))
201 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
202200, 201sylan9eq 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
203 dvf 25956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
204158feq2d 6722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
205203, 204mpbii 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
206205ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
207206ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
208207adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
209180sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
210 fnfvelrn 7099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
211208, 209, 210syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
212202, 211eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺))
213 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
214212, 213syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
215214rexlimdva 3152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
216199, 215mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺𝑋) = (𝐺𝑧)) → 0 ∈ ran (ℝ D 𝐺))
217216ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) = (𝐺𝑧) → 0 ∈ ran (ℝ D 𝐺)))
218135, 217sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺)))
219218necon3bd 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
220129, 219mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
221220ralrimiva 3143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
222221adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺𝑋) − (𝐺𝑧)) ≠ 0)
223127, 222, 104rspcdva 3622 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
224119, 124, 223divcld 12040 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) ∈ ℂ)
22524adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐶 ∈ ℂ)
226224, 225subcld 11617 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶) ∈ ℂ)
227226abscld 15471 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ∈ ℝ)
22828adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐸 ∈ ℝ)
229109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐷 ∈ ℝ*)
230110adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋 < 𝐷)
231 iccssioo 13452 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ*𝐷 ∈ ℝ*) ∧ (𝐴 < 𝑅𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
23299, 229, 91, 230, 231syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷))
2335adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵))
234232, 233sstrd 4005 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵))
235 fss 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
2361, 153, 235sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
237 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
238 dvcn 25971 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
239154, 236, 157, 237, 238syl31anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
240 cncfcdm 24937 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
241153, 239, 240sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
2421, 241mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
243242adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
244 rescncf 24936 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
245234, 243, 244sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
246163adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ))
247 rescncf 24936 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)))
248234, 246, 247sylc 65 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))
249153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ℝ ⊆ ℂ)
250236adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
251136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝐵) ⊆ ℝ)
252 iccssre 13465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ)
25364, 92, 252syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅[,]𝑋) ⊆ ℝ)
25446, 171dvres 25960 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
255249, 250, 251, 253, 254syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
256 iccntr 24856 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
25764, 92, 256syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋))
258257reseq2d 5999 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
259255, 258eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
260259dmeqd 5918 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)))
26159, 64, 91ltled 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐴𝑅)
262 iooss1 13418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝐴𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
26399, 261, 262syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋))
264111adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑋𝐷)
265 iooss2 13419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐷 ∈ ℝ*𝑋𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
266229, 264, 265syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷))
267263, 266sstrd 4005 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷))
268267, 233sstrd 4005 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵))
269237adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
270268, 269sseqtrrd 4036 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹))
271 ssdmres 6032 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
272270, 271sylib 218 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
273260, 272eqtrd 2774 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
274156adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
27546, 171dvres 25960 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
276249, 274, 251, 253, 275syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))))
277257reseq2d 5999 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
278276, 277eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
279278dmeqd 5918 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)))
280158adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
281268, 280sseqtrrd 4036 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺))
282 ssdmres 6032 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
283281, 282sylib 218 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋))
284279, 283eqtrd 2774 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋))
28564, 92, 98, 245, 248, 273, 284cmvth 26043 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)))
28664rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅 ∈ ℝ*)
287286adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ ℝ*)
288100ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ ℝ*)
28964, 92, 98ltled 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → 𝑅𝑋)
290289adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅𝑋)
291 ubicc2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑋 ∈ (𝑅[,]𝑋))
292287, 288, 290, 291syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋))
293292fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹𝑋))
294 lbicc2 13500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ*𝑋 ∈ ℝ*𝑅𝑋) → 𝑅 ∈ (𝑅[,]𝑋))
295287, 288, 290, 294syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋))
296295fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹𝑅))
297293, 296oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹𝑋) − (𝐹𝑅)))
298278fveq1d 6908 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤))
299 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
300298, 299sylan9eq 2794 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤))
301297, 300oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)))
302292fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺𝑋))
303295fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺𝑅))
304302, 303oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺𝑋) − (𝐺𝑅)))
305259fveq1d 6908 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤))
306 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
307305, 306sylan9eq 2794 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤))
308304, 307oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)))
309124adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ∈ ℂ)
310 dvf 25956 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
311237feq2d 6722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
312310, 311mpbii 233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
313312ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
314268sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵))
315313, 314ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ)
316309, 315mulcomd 11279 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺𝑋) − (𝐺𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
317308, 316eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅))))
318301, 317eqeq12d 2750 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
319119adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑅)) ∈ ℂ)
320205ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
321320, 314ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ)
322223adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑅)) ≠ 0)
323128ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐺))
324320ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
325324, 314, 210syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺))
326 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
327325, 326syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺)))
328327necon3bd 2951 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0))
329323, 328mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0)
330319, 309, 315, 321, 322, 329divmuleqd 12086 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺𝑋) − (𝐺𝑅)))))
331318, 330bitr4d 282 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
332331rexbidva 3174 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))))
333285, 332mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
334 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤))
335 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤))
336334, 335oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))
337336fvoveq1d 7452 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
338337breq1d 5157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
339 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
340339ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸)
341267sselda 3994 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷))
342338, 340, 341rspcdva 3622 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)
343 fvoveq1 7453 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)))
344343breq1d 5157 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸))
345342, 344syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
346345rexlimdva 3152 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸))
347333, 346mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) < 𝐸)
348227, 228, 347ltled 11406 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸)
349 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐹𝑢) = (𝐹𝑅))
350349oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐹𝑋) − (𝐹𝑢)) = ((𝐹𝑋) − (𝐹𝑅)))
351 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑅 → (𝐺𝑢) = (𝐺𝑅))
352351oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑅 → ((𝐺𝑋) − (𝐺𝑢)) = ((𝐺𝑋) − (𝐺𝑅)))
353350, 352oveq12d 7448 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑅 → (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) = (((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))))
354353fvoveq1d 7452 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑅 → (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)))
355354breq1d 5157 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑅 → ((abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸))
356355rspcev 3621 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹𝑋) − (𝐹𝑅)) / ((𝐺𝑋) − (𝐺𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
357105, 348, 356syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
358357adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
359 ssrexv 4064 . . . . . . . . . . . . . . 15 (((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
36057, 358, 359syl2imc 41 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ (𝑟 ∈ ℝ+𝑟 < (𝑋𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
361360anassrs 467 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
362361expimpd 453 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
363362rexlimdva 3152 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → (∃𝑟 ∈ ℝ+ (𝑟 < (𝑋𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
36449, 363mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
365 inss2 4245 . . . . . . . . . . . . . 14 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴})
366 difss 4145 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋)
367365, 366sstri 4004 . . . . . . . . . . . . 13 (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)
368367sseli 3990 . . . . . . . . . . . 12 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋))
369 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐹𝑧) = (𝐹𝑢))
370369oveq2d 7446 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐹𝑋) − (𝐹𝑧)) = ((𝐹𝑋) − (𝐹𝑢)))
371 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑢 → (𝐺𝑧) = (𝐺𝑢))
372371oveq2d 7446 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑢 → ((𝐺𝑋) − (𝐺𝑧)) = ((𝐺𝑋) − (𝐺𝑢)))
373370, 372oveq12d 7448 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
374 eqid 2734 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))
375 ovex 7463 . . . . . . . . . . . . . . 15 (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) ∈ V
376373, 374, 375fvmpt 7015 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) = (((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))))
377376fvoveq1d 7452 . . . . . . . . . . . . 13 (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)))
378377breq1d 5157 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
379368, 378syl 17 . . . . . . . . . . 11 (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸))
380379rexbiia 3089 . . . . . . . . . 10 (∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹𝑋) − (𝐹𝑢)) / ((𝐺𝑋) − (𝐺𝑢))) − 𝐶)) ≤ 𝐸)
381364, 380sylibr 234 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
382 ovex 7463 . . . . . . . . . . 11 (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ V
383382, 374fnmpti 6711 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋)
384 fvoveq1 7453 . . . . . . . . . . . 12 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → (abs‘(𝑥𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)))
385384breq1d 5157 . . . . . . . . . . 11 (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
386385rexima 7257 . . . . . . . . . 10 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸))
387383, 367, 386mp2an 692 . . . . . . . . 9 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)
388381, 387sylibr 234 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸)
389 dfrex2 3070 . . . . . . . 8 (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
390388, 389sylib 218 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
391 ssrab 4082 . . . . . . . 8 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸))
392391simprbi 496 . . . . . . 7 (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥𝐶)) ≤ 𝐸)
393390, 392nsyl 140 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐴𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})
394393expr 456 . . . . 5 ((𝜑𝑣 ∈ (TopOpen‘ℂfld)) → (𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
395394ralrimiva 3143 . . . 4 (𝜑 → ∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
396 ralinexa 3098 . . . 4 (∀𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
397395, 396sylib 218 . . 3 (𝜑 → ¬ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
398 fvoveq1 7453 . . . . . . . 8 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (abs‘(𝑥𝐶)) = (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)))
399398breq1d 5157 . . . . . . 7 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → ((abs‘(𝑥𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
400399notbid 318 . . . . . 6 (𝑥 = ((𝐹𝑋) / (𝐺𝑋)) → (¬ (abs‘(𝑥𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
401400elrab3 3695 . . . . 5 (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
40221, 401syl 17 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸))
403 eleq2 2827 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 ↔ ((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
404 sseq2 4021 . . . . . . . 8 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))
405404anbi2d 630 . . . . . . 7 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
406405rexbidv 3176 . . . . . 6 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
407403, 406imbi12d 344 . . . . 5 (𝑢 = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ((((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}))))
4089adantr 480 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑋) ∈ ℂ)
4091ffvelcdmda 7103 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℝ)
410131, 409syldan 591 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℝ)
411410recnd 11286 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (𝐹𝑧) ∈ ℂ)
412408, 411subcld 11617 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹𝑋) − (𝐹𝑧)) ∈ ℂ)
413130, 134subcld 11617 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ)
414 eldifsn 4790 . . . . . . . . 9 (((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}) ↔ (((𝐺𝑋) − (𝐺𝑧)) ∈ ℂ ∧ ((𝐺𝑋) − (𝐺𝑧)) ≠ 0))
415413, 220, 414sylanbrc 583 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺𝑋) − (𝐺𝑧)) ∈ (ℂ ∖ {0}))
416 ssidd 4018 . . . . . . . 8 (𝜑 → ℂ ⊆ ℂ)
417 difss 4145 . . . . . . . . 9 (ℂ ∖ {0}) ⊆ ℂ
418417a1i 11 . . . . . . . 8 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
41946cnfldtopon 24818 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
420 cnex 11233 . . . . . . . . . 10 ℂ ∈ V
421420difexi 5335 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
422 txrest 23654 . . . . . . . . . 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 693 . . . . . . . . 9 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
424 unicntop 24821 . . . . . . . . . . . 12 ℂ = (TopOpen‘ℂfld)
425424restid 17479 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
426419, 425ax-mp 5 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
427426oveq1i 7440 . . . . . . . . 9 (((TopOpen‘ℂfld) ↾t ℂ) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
428423, 427eqtr2i 2763 . . . . . . . 8 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × (ℂ ∖ {0})))
4299subid1d 11606 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) = (𝐹𝑋))
430 txtopon 23614 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
431419, 419, 430mp2an 692 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
432431toponrestid 22942 . . . . . . . . . 10 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
433 limcresi 25934 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
434 ioossre 13444 . . . . . . . . . . . . . 14 (𝐴(,)𝑋) ⊆ ℝ
435 resmpt 6056 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)))
436434, 435ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋))
437436oveq1i 7440 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐹𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
438433, 437sseqtri 4031 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴)
439 cncfmptc 24951 . . . . . . . . . . . . 13 (((𝐹𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
4408, 154, 154, 439syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹𝑋)) ∈ (ℝ–cn→ℝ))
441 eqidd 2735 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐹𝑋) = (𝐹𝑋))
442440, 39, 441cnmptlimc 25939 . . . . . . . . . . 11 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹𝑋)) lim 𝐴))
443438, 442sselid 3992 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑋)) lim 𝐴))
444 limcresi 25934 . . . . . . . . . . . 12 (𝐹 lim 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴)
4451, 114feqresmpt 6977 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)))
446445oveq1d 7445 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
447444, 446sseqtrid 4047 . . . . . . . . . . 11 (𝜑 → (𝐹 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
448 lhop1.f0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
449447, 448sseldd 3995 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹𝑧)) lim 𝐴))
45046subcn 24901 . . . . . . . . . . 11 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
451 0cn 11250 . . . . . . . . . . . 12 0 ∈ ℂ
452 opelxpi 5725 . . . . . . . . . . . 12 (((𝐹𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
4539, 451, 452sylancl 586 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ))
454431toponunii 22937 . . . . . . . . . . . 12 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
455454cncnpi 23301 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐹𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
456450, 453, 455sylancr 587 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), 0⟩))
457408, 411, 416, 416, 46, 432, 443, 449, 456limccnp2 25941 . . . . . . . . 9 (𝜑 → ((𝐹𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
458429, 457eqeltrrd 2839 . . . . . . . 8 (𝜑 → (𝐹𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹𝑋) − (𝐹𝑧))) lim 𝐴))
45912subid1d 11606 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) = (𝐺𝑋))
460 limcresi 25934 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴)
461 resmpt 6056 . . . . . . . . . . . . . 14 ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)))
462434, 461ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋))
463462oveq1i 7440 . . . . . . . . . . . 12 (((𝑧 ∈ ℝ ↦ (𝐺𝑋)) ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
464460, 463sseqtri 4031 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴)
465 cncfmptc 24951 . . . . . . . . . . . . 13 (((𝐺𝑋) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
46611, 154, 154, 465syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺𝑋)) ∈ (ℝ–cn→ℝ))
467 eqidd 2735 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝐺𝑋) = (𝐺𝑋))
468466, 39, 467cnmptlimc 25939 . . . . . . . . . . 11 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺𝑋)) lim 𝐴))
469464, 468sselid 3992 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑋)) lim 𝐴))
470 limcresi 25934 . . . . . . . . . . . 12 (𝐺 lim 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴)
47110, 114feqresmpt 6977 . . . . . . . . . . . . 13 (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)))
472471oveq1d 7445 . . . . . . . . . . . 12 (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) lim 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
473470, 472sseqtrid 4047 . . . . . . . . . . 11 (𝜑 → (𝐺 lim 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
474 lhop1.g0 . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
475473, 474sseldd 3995 . . . . . . . . . 10 (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺𝑧)) lim 𝐴))
476 opelxpi 5725 . . . . . . . . . . . 12 (((𝐺𝑋) ∈ ℂ ∧ 0 ∈ ℂ) → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
47712, 451, 476sylancl 586 . . . . . . . . . . 11 (𝜑 → ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ))
478454cncnpi 23301 . . . . . . . . . . 11 (( − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨(𝐺𝑋), 0⟩ ∈ (ℂ × ℂ)) → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
479450, 477, 478sylancr 587 . . . . . . . . . 10 (𝜑 → − ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨(𝐺𝑋), 0⟩))
480130, 134, 416, 416, 46, 432, 469, 475, 479limccnp2 25941 . . . . . . . . 9 (𝜑 → ((𝐺𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
481459, 480eqeltrrd 2839 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺𝑋) − (𝐺𝑧))) lim 𝐴))
482 eqid 2734 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
48346, 482divcn 24905 . . . . . . . . 9 / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld))
484 eldifsn 4790 . . . . . . . . . . 11 ((𝐺𝑋) ∈ (ℂ ∖ {0}) ↔ ((𝐺𝑋) ∈ ℂ ∧ (𝐺𝑋) ≠ 0))
48512, 20, 484sylanbrc 583 . . . . . . . . . 10 (𝜑 → (𝐺𝑋) ∈ (ℂ ∖ {0}))
4869, 485opelxpd 5727 . . . . . . . . 9 (𝜑 → ⟨(𝐹𝑋), (𝐺𝑋)⟩ ∈ (ℂ × (ℂ ∖ {0})))
487 resttopon 23184 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
488419, 417, 487mp2an 692 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))
489 txtopon 23614 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))) → ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0}))))
490419, 488, 489mp2an 692 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) ∈ (TopOn‘(ℂ × (ℂ ∖ {0})))
491490toponunii 22937 . . . . . . . . . 10 (ℂ × (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))
492491cncnpi 23301 . . . . . . . . 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 587 . . . . . . . 8 (𝜑 → / ∈ ((((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) CnP (TopOpen‘ℂfld))‘⟨(𝐹𝑋), (𝐺𝑋)⟩))
494412, 415, 416, 418, 46, 428, 458, 481, 493limccnp2 25941 . . . . . . 7 (𝜑 → ((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴))
495412, 413, 220divcld 12040 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧))) ∈ ℂ)
496495fmpttd 7134 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))):(𝐴(,)𝑋)⟶ℂ)
497434, 153sstri 4004 . . . . . . . . 9 (𝐴(,)𝑋) ⊆ ℂ
498497a1i 11 . . . . . . . 8 (𝜑 → (𝐴(,)𝑋) ⊆ ℂ)
499496, 498, 66, 46ellimc2 25926 . . . . . . 7 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) lim 𝐴) ↔ (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))))
500494, 499mpbid 232 . . . . . 6 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))
501500simprd 495 . . . . 5 (𝜑 → ∀𝑢 ∈ (TopOpen‘ℂfld)(((𝐹𝑋) / (𝐺𝑋)) ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))
502 notrab 4327 . . . . . 6 (ℂ ∖ {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸}
50368cnmetdval 24806 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶𝑥)))
504 abssub 15361 . . . . . . . . . . . 12 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (abs‘(𝐶𝑥)) = (abs‘(𝑥𝐶)))
505503, 504eqtrd 2774 . . . . . . . . . . 11 ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
50624, 505sylan 580 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥𝐶)))
507506breq1d 5157 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥𝐶)) ≤ 𝐸))
508507rabbidva 3439 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸})
50932a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51028rexrd 11308 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ*)
511 eqid 2734 . . . . . . . . . 10 {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸}
51247, 511blcld 24533 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
513509, 24, 510, 512syl3anc 1370 . . . . . . . 8 (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
514508, 513eqeltrrd 2839 . . . . . . 7 (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥𝐶)) ≤ 𝐸} ∈ (Clsd‘(TopOpen‘ℂfld)))
515424cldopn 23054 . . . . . . 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 3622 . . . 4 (𝜑 → (((𝐹𝑋) / (𝐺𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸} → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
519402, 518sylbird 260 . . 3 (𝜑 → (¬ (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐴𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹𝑋) − (𝐹𝑧)) / ((𝐺𝑋) − (𝐺𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬ (abs‘(𝑥𝐶)) ≤ 𝐸})))
520397, 519mt3d 148 . 2 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) ≤ 𝐸)
52128recnd 11286 . . . 4 (𝜑𝐸 ∈ ℂ)
522521mullidd 11276 . . 3 (𝜑 → (1 · 𝐸) = 𝐸)
523 1red 11259 . . . 4 (𝜑 → 1 ∈ ℝ)
524 1lt2 12434 . . . . 5 1 < 2
525524a1i 11 . . . 4 (𝜑 → 1 < 2)
526523, 30, 27, 525ltmul1dd 13129 . . 3 (𝜑 → (1 · 𝐸) < (2 · 𝐸))
527522, 526eqbrtrrd 5171 . 2 (𝜑𝐸 < (2 · 𝐸))
52826, 28, 31, 520, 527lelttrd 11416 1 (𝜑 → (abs‘(((𝐹𝑋) / (𝐺𝑋)) − 𝐶)) < (2 · 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  cin 3961  wss 3962  c0 4338  {csn 4630  cop 4636   class class class wbr 5147  cmpt 5230   × cxp 5686  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  ccom 5692   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  *cxr 11291   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  2c2 12318  +crp 13031  (,)cioo 13383  [,]cicc 13386  abscabs 15269  t crest 17466  TopOpenctopn 17467  topGenctg 17483  ∞Metcxmet 21366  ballcbl 21368  fldccnfld 21381  TopOnctopon 22931  Clsdccld 23039  intcnt 23040   Cn ccn 23247   CnP ccnp 23248   ×t ctx 23583  cnccncf 24915   lim climc 25911   D cdv 25912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916
This theorem is referenced by:  lhop1  26067
  Copyright terms: Public domain W3C validator