Metamath Proof Explorer

Theorem lhop1lem

Description: Lemma for lhop1 . (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses 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 lhop1lem ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) < ( 2 · 𝐸 ) )

Proof

Step Hyp Ref Expression
1 lhop1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 lhop1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 lhop1.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 lhop1.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
5 lhop1.g ⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
6 lhop1.if ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
7 lhop1.ig ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
8 lhop1.f0 ⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝐴 ) )
9 lhop1.g0 ⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝐴 ) )
10 lhop1.gn0 ⊢ ( 𝜑 → ¬ 0 ∈ ran 𝐺 )
11 lhop1.gd0 ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
12 lhop1.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
13 lhop1lem.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
14 lhop1lem.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
15 lhop1lem.db ⊢ ( 𝜑 → 𝐷 ≤ 𝐵 )
16 lhop1lem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 (,) 𝐷 ) )
17 lhop1lem.t ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝐴 (,) 𝐷 ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑡 ) / ( ( ℝ D 𝐺 ) ‘ 𝑡 ) ) − 𝐶 ) ) < 𝐸 )
18 lhop1lem.r ⊢ 𝑅 = ( 𝐴 + ( 𝑟 / 2 ) )
19 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐷 ≤ 𝐵 ) → ( 𝐴 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
20 2 15 19 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
21 20 16 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 (,) 𝐵 ) )
22 4 21 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
24 5 21 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ℝ )
25 24 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
26 5 ffnd ⊢ ( 𝜑 → 𝐺 Fn ( 𝐴 (,) 𝐵 ) )
27 fnfvelrn ⊢ ( ( 𝐺 Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 )
28 26 21 27 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 )
29 eleq1 ⊢ ( ( 𝐺 ‘ 𝑋 ) = 0 → ( ( 𝐺 ‘ 𝑋 ) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺 ) )
30 28 29 syl5ibcom ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = 0 → 0 ∈ ran 𝐺 ) )
31 30 necon3bd ⊢ ( 𝜑 → ( ¬ 0 ∈ ran 𝐺 → ( 𝐺 ‘ 𝑋 ) ≠ 0 ) )
32 10 31 mpd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
33 23 25 32 divcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ ℂ )
34 limccl ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐴 ) ⊆ ℂ
35 34 12 sselid ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
36 33 35 subcld ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ∈ ℂ )
37 36 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ∈ ℝ )
38 13 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
39 2re ⊢ 2 ∈ ℝ
40 39 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
41 40 38 remulcld ⊢ ( 𝜑 → ( 2 · 𝐸 ) ∈ ℝ )
42 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
43 42 a1i ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
44 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → 𝑣 ∈ ( TopOpen ‘ ℂfld ) )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → 𝐴 ∈ 𝑣 )
46 eliooord ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐷 ) → ( 𝐴 < 𝑋 ∧ 𝑋 < 𝐷 ) )
47 16 46 syl ⊢ ( 𝜑 → ( 𝐴 < 𝑋 ∧ 𝑋 < 𝐷 ) )
48 47 simpld ⊢ ( 𝜑 → 𝐴 < 𝑋 )
49 ioossre ⊢ ( 𝐴 (,) 𝐷 ) ⊆ ℝ
50 49 16 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
51 difrp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝐴 < 𝑋 ↔ ( 𝑋 − 𝐴 ) ∈ ℝ+ ) )
52 1 50 51 syl2anc ⊢ ( 𝜑 → ( 𝐴 < 𝑋 ↔ ( 𝑋 − 𝐴 ) ∈ ℝ+ ) )
53 48 52 mpbid ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℝ+ )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ( 𝑋 − 𝐴 ) ∈ ℝ+ )
55 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
56 55 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
57 56 mopni3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ∧ ( 𝑋 − 𝐴 ) ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ ( 𝑟 < ( 𝑋 − 𝐴 ) ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 ) )
58 43 44 45 54 57 syl31anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑟 < ( 𝑋 − 𝐴 ) ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 ) )
59 ssrin ⊢ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 → ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ⊆ ( 𝑣 ∩ ( 𝐴 (,) 𝑋 ) ) )
60 lbioo ⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝑋 )
61 disjsn ⊢ ( ( ( 𝐴 (,) 𝑋 ) ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ ( 𝐴 (,) 𝑋 ) )
62 60 61 mpbir ⊢ ( ( 𝐴 (,) 𝑋 ) ∩ { 𝐴 } ) = ∅
63 disj3 ⊢ ( ( ( 𝐴 (,) 𝑋 ) ∩ { 𝐴 } ) = ∅ ↔ ( 𝐴 (,) 𝑋 ) = ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) )
64 62 63 mpbi ⊢ ( 𝐴 (,) 𝑋 ) = ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } )
65 64 ineq2i ⊢ ( 𝑣 ∩ ( 𝐴 (,) 𝑋 ) ) = ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) )
66 59 65 sseqtrdi ⊢ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 → ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ⊆ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) )
67 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐴 ∈ ℝ )
68 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑟 ∈ ℝ+ )
69 68 rpred ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑟 ∈ ℝ )
70 69 rehalfcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑟 / 2 ) ∈ ℝ )
71 67 70 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐴 + ( 𝑟 / 2 ) ) ∈ ℝ )
72 18 71 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ℝ )
73 72 recnd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ℂ )
74 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
75 74 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐴 ∈ ℂ )
76 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
77 76 cnmetdval ⊢ ( ( 𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑅 ( abs ∘ − ) 𝐴 ) = ( abs ‘ ( 𝑅 − 𝐴 ) ) )
78 73 75 77 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 ( abs ∘ − ) 𝐴 ) = ( abs ‘ ( 𝑅 − 𝐴 ) ) )
79 18 oveq1i ⊢ ( 𝑅 − 𝐴 ) = ( ( 𝐴 + ( 𝑟 / 2 ) ) − 𝐴 )
80 69 recnd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑟 ∈ ℂ )
81 80 halfcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑟 / 2 ) ∈ ℂ )
82 75 81 pncan2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( 𝐴 + ( 𝑟 / 2 ) ) − 𝐴 ) = ( 𝑟 / 2 ) )
83 79 82 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 − 𝐴 ) = ( 𝑟 / 2 ) )
84 83 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( abs ‘ ( 𝑅 − 𝐴 ) ) = ( abs ‘ ( 𝑟 / 2 ) ) )
85 68 rphalfcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
86 85 rpred ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑟 / 2 ) ∈ ℝ )
87 85 rpge0d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 0 ≤ ( 𝑟 / 2 ) )
88 86 87 absidd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( abs ‘ ( 𝑟 / 2 ) ) = ( 𝑟 / 2 ) )
89 78 84 88 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 ( abs ∘ − ) 𝐴 ) = ( 𝑟 / 2 ) )
90 rphalflt ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) < 𝑟 )
91 68 90 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑟 / 2 ) < 𝑟 )
92 89 91 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 ( abs ∘ − ) 𝐴 ) < 𝑟 )
93 42 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
94 69 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑟 ∈ ℝ* )
95 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑟 ∈ ℝ* ) ∧ ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ) ) → ( 𝑅 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑅 ( abs ∘ − ) 𝐴 ) < 𝑟 ) )
96 93 94 75 73 95 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑅 ( abs ∘ − ) 𝐴 ) < 𝑟 ) )
97 92 96 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
98 67 85 ltaddrpd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐴 < ( 𝐴 + ( 𝑟 / 2 ) ) )
99 98 18 breqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐴 < 𝑅 )
100 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑋 ∈ ℝ )
101 100 67 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑋 − 𝐴 ) ∈ ℝ )
102 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑟 < ( 𝑋 − 𝐴 ) )
103 86 69 101 91 102 lttrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑟 / 2 ) < ( 𝑋 − 𝐴 ) )
104 67 86 100 ltaddsub2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( 𝐴 + ( 𝑟 / 2 ) ) < 𝑋 ↔ ( 𝑟 / 2 ) < ( 𝑋 − 𝐴 ) ) )
105 103 104 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐴 + ( 𝑟 / 2 ) ) < 𝑋 )
106 18 105 eqbrtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 < 𝑋 )
107 67 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐴 ∈ ℝ* )
108 50 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
109 108 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑋 ∈ ℝ* )
110 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑅 ∈ ( 𝐴 (,) 𝑋 ) ↔ ( 𝑅 ∈ ℝ ∧ 𝐴 < 𝑅 ∧ 𝑅 < 𝑋 ) ) )
111 107 109 110 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 ∈ ( 𝐴 (,) 𝑋 ) ↔ ( 𝑅 ∈ ℝ ∧ 𝐴 < 𝑅 ∧ 𝑅 < 𝑋 ) ) )
112 72 99 106 111 mpbir3and ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ( 𝐴 (,) 𝑋 ) )
113 97 112 elind ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) )
114 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
115 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
116 14 rexrd ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
117 47 simprd ⊢ ( 𝜑 → 𝑋 < 𝐷 )
118 50 14 117 ltled ⊢ ( 𝜑 → 𝑋 ≤ 𝐷 )
119 108 116 2 118 15 xrletrd ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
120 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
121 2 119 120 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
123 122 112 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ( 𝐴 (,) 𝐵 ) )
124 115 123 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐹 ‘ 𝑅 ) ∈ ℝ )
125 124 recnd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐹 ‘ 𝑅 ) ∈ ℂ )
126 114 125 subcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) ∈ ℂ )
127 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
128 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
129 128 123 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐺 ‘ 𝑅 ) ∈ ℝ )
130 129 recnd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐺 ‘ 𝑅 ) ∈ ℂ )
131 127 130 subcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ∈ ℂ )
132 fveq2 ⊢ ( 𝑧 = 𝑅 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑅 ) )
133 132 oveq2d ⊢ ( 𝑧 = 𝑅 → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) )
134 133 neeq1d ⊢ ( 𝑧 = 𝑅 → ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ≠ 0 ↔ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ≠ 0 ) )
135 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
136 25 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
137 121 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
138 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
139 137 138 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
140 139 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
141 136 140 subeq0ad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) = 0 ↔ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) )
142 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
143 142 137 sselid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑧 ∈ ℝ )
144 143 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → 𝑧 ∈ ℝ )
145 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → 𝑋 ∈ ℝ )
146 eliooord ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) → ( 𝐴 < 𝑧 ∧ 𝑧 < 𝑋 ) )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐴 < 𝑧 ∧ 𝑧 < 𝑋 ) )
148 147 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑧 < 𝑋 )
149 148 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → 𝑧 < 𝑋 )
150 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
151 150 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝐴 ∈ ℝ* )
152 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝐵 ∈ ℝ* )
153 147 simpld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝐴 < 𝑧 )
154 108 116 2 117 15 xrltletrd ⊢ ( 𝜑 → 𝑋 < 𝐵 )
155 154 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑋 < 𝐵 )
156 iccssioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝑧 ∧ 𝑋 < 𝐵 ) ) → ( 𝑧 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
157 151 152 153 155 156 syl22anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝑧 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
158 157 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝑧 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
159 ax-resscn ⊢ ℝ ⊆ ℂ
160 159 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
161 fss ⊢ ( ( 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
162 5 159 161 sylancl ⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
163 142 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
164 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ∧ dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) ) → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
165 160 162 163 7 164 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
166 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
167 159 165 166 sylancr ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
168 5 167 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
169 168 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
170 rescncf ⊢ ( ( 𝑧 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ∈ ( ( 𝑧 [,] 𝑋 ) –cn→ ℝ ) ) )
171 158 169 170 sylc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ∈ ( ( 𝑧 [,] 𝑋 ) –cn→ ℝ ) )
172 159 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ℝ ⊆ ℂ )
173 162 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
174 142 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
175 158 142 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝑧 [,] 𝑋 ) ⊆ ℝ )
176 55 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
177 55 176 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ ∧ ( 𝑧 [,] 𝑋 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑧 [,] 𝑋 ) ) ) )
178 172 173 174 175 177 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑧 [,] 𝑋 ) ) ) )
179 iccntr ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑧 [,] 𝑋 ) ) = ( 𝑧 (,) 𝑋 ) )
180 144 145 179 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑧 [,] 𝑋 ) ) = ( 𝑧 (,) 𝑋 ) )
181 180 reseq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑧 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) )
182 178 181 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) )
183 182 dmeqd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → dom ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) = dom ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) )
184 ioossicc ⊢ ( 𝑧 (,) 𝑋 ) ⊆ ( 𝑧 [,] 𝑋 )
185 184 158 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝑧 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
186 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
187 185 186 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( 𝑧 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐺 ) )
188 ssdmres ⊢ ( ( 𝑧 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐺 ) ↔ dom ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) = ( 𝑧 (,) 𝑋 ) )
189 187 188 sylib ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → dom ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) = ( 𝑧 (,) 𝑋 ) )
190 183 189 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → dom ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) = ( 𝑧 (,) 𝑋 ) )
191 143 rexrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑧 ∈ ℝ* )
192 108 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑋 ∈ ℝ* )
193 50 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑋 ∈ ℝ )
194 143 193 148 ltled ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑧 ≤ 𝑋 )
195 ubicc2 ⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑧 ≤ 𝑋 ) → 𝑋 ∈ ( 𝑧 [,] 𝑋 ) )
196 191 192 194 195 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑋 ∈ ( 𝑧 [,] 𝑋 ) )
197 196 fvresd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
198 lbicc2 ⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑧 ≤ 𝑋 ) → 𝑧 ∈ ( 𝑧 [,] 𝑋 ) )
199 191 192 194 198 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → 𝑧 ∈ ( 𝑧 [,] 𝑋 ) )
200 199 fvresd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
201 197 200 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑋 ) = ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) )
202 201 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑋 ) = ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑧 ) )
203 202 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑧 ) = ( ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ‘ 𝑋 ) )
204 144 145 149 171 190 203 rolle ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ∃ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) = 0 )
205 182 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) = ( ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) ‘ 𝑤 ) )
206 fvres ⊢ ( 𝑤 ∈ ( 𝑧 (,) 𝑋 ) → ( ( ( ℝ D 𝐺 ) ↾ ( 𝑧 (,) 𝑋 ) ) ‘ 𝑤 ) = ( ( ℝ D 𝐺 ) ‘ 𝑤 ) )
207 205 206 sylan9eq ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) ∧ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) = ( ( ℝ D 𝐺 ) ‘ 𝑤 ) )
208 dvf ⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ
209 7 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ ↔ ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
210 208 209 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
211 210 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
212 211 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) )
213 212 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) ∧ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ) → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) )
214 185 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) ∧ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ) → 𝑤 ∈ ( 𝐴 (,) 𝐵 ) )
215 fnfvelrn ⊢ ( ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ∈ ran ( ℝ D 𝐺 ) )
216 213 214 215 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) ∧ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ∈ ran ( ℝ D 𝐺 ) )
217 207 216 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) ∧ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) ∈ ran ( ℝ D 𝐺 ) )
218 eleq1 ⊢ ( ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) = 0 → ( ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) ∈ ran ( ℝ D 𝐺 ) ↔ 0 ∈ ran ( ℝ D 𝐺 ) ) )
219 217 218 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) ∧ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ) → ( ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) )
220 219 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → ( ∃ 𝑤 ∈ ( 𝑧 (,) 𝑋 ) ( ( ℝ D ( 𝐺 ↾ ( 𝑧 [,] 𝑋 ) ) ) ‘ 𝑤 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) )
221 204 220 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) ) → 0 ∈ ran ( ℝ D 𝐺 ) )
222 221 ex ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑧 ) → 0 ∈ ran ( ℝ D 𝐺 ) ) )
223 141 222 sylbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) )
224 223 necon3bd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ¬ 0 ∈ ran ( ℝ D 𝐺 ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ≠ 0 ) )
225 135 224 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ≠ 0 )
226 225 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ≠ 0 )
227 226 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ∀ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ≠ 0 )
228 134 227 112 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ≠ 0 )
229 126 131 228 divcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) ∈ ℂ )
230 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐶 ∈ ℂ )
231 229 230 subcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ∈ ℂ )
232 231 abscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) ∈ ℝ )
233 38 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐸 ∈ ℝ )
234 116 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐷 ∈ ℝ* )
235 117 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑋 < 𝐷 )
236 iccssioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ∧ ( 𝐴 < 𝑅 ∧ 𝑋 < 𝐷 ) ) → ( 𝑅 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐷 ) )
237 107 234 99 235 236 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐷 ) )
238 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐴 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
239 237 238 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
240 fss ⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
241 4 159 240 sylancl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
242 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ∧ dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
243 160 241 163 6 242 syl31anc ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
244 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
245 159 243 244 sylancr ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
246 4 245 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
247 246 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
248 rescncf ⊢ ( ( 𝑅 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ∈ ( ( 𝑅 [,] 𝑋 ) –cn→ ℝ ) ) )
249 239 247 248 sylc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ∈ ( ( 𝑅 [,] 𝑋 ) –cn→ ℝ ) )
250 168 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
251 rescncf ⊢ ( ( 𝑅 [,] 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ∈ ( ( 𝑅 [,] 𝑋 ) –cn→ ℝ ) ) )
252 239 250 251 sylc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ∈ ( ( 𝑅 [,] 𝑋 ) –cn→ ℝ ) )
253 159 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ℝ ⊆ ℂ )
254 241 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
255 142 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
256 iccssre ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝑅 [,] 𝑋 ) ⊆ ℝ )
257 72 100 256 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 [,] 𝑋 ) ⊆ ℝ )
258 55 176 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ ∧ ( 𝑅 [,] 𝑋 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) ) )
259 253 254 255 257 258 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) ) )
260 iccntr ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) = ( 𝑅 (,) 𝑋 ) )
261 72 100 260 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) = ( 𝑅 (,) 𝑋 ) )
262 261 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) )
263 259 262 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) )
264 263 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) )
265 67 72 99 ltled ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐴 ≤ 𝑅 )
266 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑅 ) → ( 𝑅 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝑋 ) )
267 107 265 266 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝑋 ) )
268 118 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑋 ≤ 𝐷 )
269 iooss2 ⊢ ( ( 𝐷 ∈ ℝ* ∧ 𝑋 ≤ 𝐷 ) → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐷 ) )
270 234 268 269 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐷 ) )
271 267 270 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐷 ) )
272 271 238 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
273 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
274 272 273 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) )
275 ssdmres ⊢ ( ( 𝑅 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) = ( 𝑅 (,) 𝑋 ) )
276 274 275 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) = ( 𝑅 (,) 𝑋 ) )
277 264 276 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( 𝑅 (,) 𝑋 ) )
278 162 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
279 55 176 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ ∧ ( 𝑅 [,] 𝑋 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) ) )
280 253 278 255 257 279 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) ) )
281 261 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) )
282 280 281 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) )
283 282 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) = dom ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) )
284 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
285 272 284 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( 𝑅 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐺 ) )
286 ssdmres ⊢ ( ( 𝑅 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐺 ) ↔ dom ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) = ( 𝑅 (,) 𝑋 ) )
287 285 286 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) = ( 𝑅 (,) 𝑋 ) )
288 283 287 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → dom ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) = ( 𝑅 (,) 𝑋 ) )
289 72 100 106 249 252 277 288 cmvth ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ∃ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ( ( ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) )
290 72 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ∈ ℝ* )
291 290 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑅 ∈ ℝ* )
292 108 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑋 ∈ ℝ* )
293 72 100 106 ltled ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → 𝑅 ≤ 𝑋 )
294 293 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑅 ≤ 𝑋 )
295 ubicc2 ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑅 ≤ 𝑋 ) → 𝑋 ∈ ( 𝑅 [,] 𝑋 ) )
296 291 292 294 295 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑋 ∈ ( 𝑅 [,] 𝑋 ) )
297 296 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
298 lbicc2 ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ∈ ( 𝑅 [,] 𝑋 ) )
299 291 292 294 298 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑅 ∈ ( 𝑅 [,] 𝑋 ) )
300 299 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) = ( 𝐹 ‘ 𝑅 ) )
301 297 300 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) = ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) )
302 282 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) = ( ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) ‘ 𝑤 ) )
303 fvres ⊢ ( 𝑤 ∈ ( 𝑅 (,) 𝑋 ) → ( ( ( ℝ D 𝐺 ) ↾ ( 𝑅 (,) 𝑋 ) ) ‘ 𝑤 ) = ( ( ℝ D 𝐺 ) ‘ 𝑤 ) )
304 302 303 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) = ( ( ℝ D 𝐺 ) ‘ 𝑤 ) )
305 301 304 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) )
306 296 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
307 299 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) = ( 𝐺 ‘ 𝑅 ) )
308 306 307 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) = ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) )
309 263 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) ‘ 𝑤 ) )
310 fvres ⊢ ( 𝑤 ∈ ( 𝑅 (,) 𝑋 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝑅 (,) 𝑋 ) ) ‘ 𝑤 ) = ( ( ℝ D 𝐹 ) ‘ 𝑤 ) )
311 309 310 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) = ( ( ℝ D 𝐹 ) ‘ 𝑤 ) )
312 308 311 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
313 131 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ∈ ℂ )
314 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
315 6 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
316 314 315 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
317 316 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
318 272 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑤 ∈ ( 𝐴 (,) 𝐵 ) )
319 317 318 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ∈ ℂ )
320 313 319 mulcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) · ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) )
321 312 320 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) · ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) )
322 305 321 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) · ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) ) )
323 126 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) ∈ ℂ )
324 210 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
325 324 318 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ∈ ℂ )
326 228 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ≠ 0 )
327 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
328 324 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) )
329 328 318 215 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ∈ ran ( ℝ D 𝐺 ) )
330 eleq1 ⊢ ( ( ( ℝ D 𝐺 ) ‘ 𝑤 ) = 0 → ( ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ∈ ran ( ℝ D 𝐺 ) ↔ 0 ∈ ran ( ℝ D 𝐺 ) ) )
331 329 330 syl5ibcom ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ℝ D 𝐺 ) ‘ 𝑤 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) )
332 331 necon3bd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ¬ 0 ∈ ran ( ℝ D 𝐺 ) → ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ≠ 0 ) )
333 327 332 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ≠ 0 )
334 323 313 319 325 326 333 divmuleqd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) · ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) ) )
335 322 334 bitr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) ) )
336 335 rexbidva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ∃ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ( ( ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) = ( ( ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑋 ) − ( ( 𝐺 ↾ ( 𝑅 [,] 𝑋 ) ) ‘ 𝑅 ) ) · ( ( ℝ D ( 𝐹 ↾ ( 𝑅 [,] 𝑋 ) ) ) ‘ 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) ) )
337 289 336 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ∃ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) )
338 fveq2 ⊢ ( 𝑡 = 𝑤 → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑤 ) )
339 fveq2 ⊢ ( 𝑡 = 𝑤 → ( ( ℝ D 𝐺 ) ‘ 𝑡 ) = ( ( ℝ D 𝐺 ) ‘ 𝑤 ) )
340 338 339 oveq12d ⊢ ( 𝑡 = 𝑤 → ( ( ( ℝ D 𝐹 ) ‘ 𝑡 ) / ( ( ℝ D 𝐺 ) ‘ 𝑡 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) )
341 340 fvoveq1d ⊢ ( 𝑡 = 𝑤 → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑡 ) / ( ( ℝ D 𝐺 ) ‘ 𝑡 ) ) − 𝐶 ) ) = ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) − 𝐶 ) ) )
342 341 breq1d ⊢ ( 𝑡 = 𝑤 → ( ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑡 ) / ( ( ℝ D 𝐺 ) ‘ 𝑡 ) ) − 𝐶 ) ) < 𝐸 ↔ ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) − 𝐶 ) ) < 𝐸 ) )
343 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ∀ 𝑡 ∈ ( 𝐴 (,) 𝐷 ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑡 ) / ( ( ℝ D 𝐺 ) ‘ 𝑡 ) ) − 𝐶 ) ) < 𝐸 )
344 271 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → 𝑤 ∈ ( 𝐴 (,) 𝐷 ) )
345 342 343 344 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) − 𝐶 ) ) < 𝐸 )
346 fvoveq1 ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) = ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) − 𝐶 ) ) )
347 346 breq1d ⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) → ( ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) < 𝐸 ↔ ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) − 𝐶 ) ) < 𝐸 ) )
348 345 347 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) ∧ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) < 𝐸 ) )
349 348 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ∃ 𝑤 ∈ ( 𝑅 (,) 𝑋 ) ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑤 ) / ( ( ℝ D 𝐺 ) ‘ 𝑤 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) < 𝐸 ) )
350 337 349 mpd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) < 𝐸 )
351 232 233 350 ltled ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) ≤ 𝐸 )
352 fveq2 ⊢ ( 𝑢 = 𝑅 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑅 ) )
353 352 oveq2d ⊢ ( 𝑢 = 𝑅 → ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) = ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) )
354 fveq2 ⊢ ( 𝑢 = 𝑅 → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑅 ) )
355 354 oveq2d ⊢ ( 𝑢 = 𝑅 → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) = ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) )
356 353 355 oveq12d ⊢ ( 𝑢 = 𝑅 → ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) = ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) )
357 356 fvoveq1d ⊢ ( 𝑢 = 𝑅 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) )
358 357 breq1d ⊢ ( 𝑢 = 𝑅 → ( ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
359 358 rspcev ⊢ ( ( 𝑅 ∈ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ∧ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑅 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑅 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) → ∃ 𝑢 ∈ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 )
360 113 351 359 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ∃ 𝑢 ∈ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 )
361 360 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ∃ 𝑢 ∈ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 )
362 ssrexv ⊢ ( ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ⊆ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) → ( ∃ 𝑢 ∈ ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 𝐴 (,) 𝑋 ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
363 66 361 362 syl2imc ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) ) → ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
364 363 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑟 < ( 𝑋 − 𝐴 ) ) → ( ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
365 364 expimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑟 < ( 𝑋 − 𝐴 ) ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 ) → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
366 365 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑟 < ( 𝑋 − 𝐴 ) ∧ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑣 ) → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
367 58 366 mpd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 )
368 inss2 ⊢ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ⊆ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } )
369 difss ⊢ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ⊆ ( 𝐴 (,) 𝑋 )
370 368 369 sstri ⊢ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ⊆ ( 𝐴 (,) 𝑋 )
371 370 sseli ⊢ ( 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) → 𝑢 ∈ ( 𝐴 (,) 𝑋 ) )
372 fveq2 ⊢ ( 𝑧 = 𝑢 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑢 ) )
373 372 oveq2d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) )
374 fveq2 ⊢ ( 𝑧 = 𝑢 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑢 ) )
375 374 oveq2d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) )
376 373 375 oveq12d ⊢ ( 𝑧 = 𝑢 → ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) )
377 eqid ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
378 ovex ⊢ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ V
379 376 377 378 fvmpt ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝑋 ) → ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) = ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) )
380 379 fvoveq1d ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝑋 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) )
381 380 breq1d ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝑋 ) → ( ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
382 371 381 syl ⊢ ( 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) → ( ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 ) )
383 382 rexbiia ⊢ ( ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 ↔ ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑢 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑢 ) ) ) − 𝐶 ) ) ≤ 𝐸 )
384 367 383 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 )
385 ovex ⊢ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ∈ V
386 385 377 fnmpti ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) Fn ( 𝐴 (,) 𝑋 )
387 fvoveq1 ⊢ ( 𝑥 = ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) → ( abs ‘ ( 𝑥 − 𝐶 ) ) = ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) )
388 387 breq1d ⊢ ( 𝑥 = ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) → ( ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 ) )
389 388 rexima ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) Fn ( 𝐴 (,) 𝑋 ) ∧ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ⊆ ( 𝐴 (,) 𝑋 ) ) → ( ∃ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ↔ ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 ) )
390 386 370 389 mp2an ⊢ ( ∃ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ↔ ∃ 𝑢 ∈ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ‘ 𝑢 ) − 𝐶 ) ) ≤ 𝐸 )
391 384 390 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ∃ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 )
392 dfrex2 ⊢ ( ∃ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ↔ ¬ ∀ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 )
393 391 392 sylib ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ¬ ∀ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 )
394 ssrab ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ↔ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ ℂ ∧ ∀ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ) )
395 394 simprbi ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ∀ 𝑥 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 )
396 393 395 nsyl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐴 ∈ 𝑣 ) ) → ¬ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } )
397 396 expr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝐴 ∈ 𝑣 → ¬ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) )
398 397 ralrimiva ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 → ¬ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) )
399 ralinexa ⊢ ( ∀ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 → ¬ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ↔ ¬ ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) )
400 398 399 sylib ⊢ ( 𝜑 → ¬ ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) )
401 fvoveq1 ⊢ ( 𝑥 = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) → ( abs ‘ ( 𝑥 − 𝐶 ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) )
402 401 breq1d ⊢ ( 𝑥 = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) → ( ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ≤ 𝐸 ) )
403 402 notbid ⊢ ( 𝑥 = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) → ( ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ↔ ¬ ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ≤ 𝐸 ) )
404 403 elrab3 ⊢ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ ℂ → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ↔ ¬ ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ≤ 𝐸 ) )
405 33 404 syl ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ↔ ¬ ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ≤ 𝐸 ) )
406 eleq2 ⊢ ( 𝑢 = { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑢 ↔ ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) )
407 sseq2 ⊢ ( 𝑢 = { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ↔ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) )
408 407 anbi2d ⊢ ( 𝑢 = { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ( ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ) )
409 408 rexbidv ⊢ ( 𝑢 = { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ( ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ) )
410 406 409 imbi12d ⊢ ( 𝑢 = { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ( ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ) ) )
411 23 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
412 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
413 137 412 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
414 413 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
415 411 414 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
416 136 140 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
417 eldifsn ⊢ ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ ∧ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ≠ 0 ) )
418 416 225 417 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ∈ ( ℂ ∖ { 0 } ) )
419 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
420 difss ⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
421 420 a1i ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
422 55 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
423 cnex ⊢ ℂ ∈ V
424 423 difexi ⊢ ( ℂ ∖ { 0 } ) ∈ V
425 txrest ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) ∧ ( ℂ ∈ V ∧ ( ℂ ∖ { 0 } ) ∈ V ) ) → ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℂ × ( ℂ ∖ { 0 } ) ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) )
426 422 422 423 424 425 mp4an ⊢ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℂ × ( ℂ ∖ { 0 } ) ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) )
427 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
428 427 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
429 422 428 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
430 429 oveq1i ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) = ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) )
431 426 430 eqtr2i ⊢ ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) = ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℂ × ( ℂ ∖ { 0 } ) ) )
432 23 subid1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) − 0 ) = ( 𝐹 ‘ 𝑋 ) )
433 txtopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
434 422 422 433 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
435 434 toponrestid ⊢ ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℂ × ℂ ) )
436 limcresi ⊢ ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) limℂ 𝐴 ) ⊆ ( ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 )
437 ioossre ⊢ ( 𝐴 (,) 𝑋 ) ⊆ ℝ
438 resmpt ⊢ ( ( 𝐴 (,) 𝑋 ) ⊆ ℝ → ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑋 ) ) )
439 437 438 ax-mp ⊢ ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑋 ) )
440 439 oveq1i ⊢ ( ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑋 ) ) limℂ 𝐴 )
441 436 440 sseqtri ⊢ ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) limℂ 𝐴 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑋 ) ) limℂ 𝐴 )
442 cncfmptc ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
443 22 160 160 442 syl3anc ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
444 eqidd ⊢ ( 𝑧 = 𝐴 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
445 443 1 444 cnmptlimc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝑧 ∈ ℝ ↦ ( 𝐹 ‘ 𝑋 ) ) limℂ 𝐴 ) )
446 441 445 sselid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑋 ) ) limℂ 𝐴 ) )
447 limcresi ⊢ ( 𝐹 limℂ 𝐴 ) ⊆ ( ( 𝐹 ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 )
448 4 121 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝑋 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
449 448 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑧 ) ) limℂ 𝐴 ) )
450 447 449 sseqtrid ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐴 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑧 ) ) limℂ 𝐴 ) )
451 450 8 sseldd ⊢ ( 𝜑 → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑧 ) ) limℂ 𝐴 ) )
452 55 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
453 0cn ⊢ 0 ∈ ℂ
454 opelxpi ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ⟨ ( 𝐹 ‘ 𝑋 ) , 0 ⟩ ∈ ( ℂ × ℂ ) )
455 23 453 454 sylancl ⊢ ( 𝜑 → ⟨ ( 𝐹 ‘ 𝑋 ) , 0 ⟩ ∈ ( ℂ × ℂ ) )
456 434 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) )
457 456 cncnpi ⊢ ( ( − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ⟨ ( 𝐹 ‘ 𝑋 ) , 0 ⟩ ∈ ( ℂ × ℂ ) ) → − ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , 0 ⟩ ) )
458 452 455 457 sylancr ⊢ ( 𝜑 → − ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , 0 ⟩ ) )
459 411 414 419 419 55 435 446 451 458 limccnp2 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) − 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
460 432 459 eqeltrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
461 25 subid1d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) − 0 ) = ( 𝐺 ‘ 𝑋 ) )
462 limcresi ⊢ ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) limℂ 𝐴 ) ⊆ ( ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 )
463 resmpt ⊢ ( ( 𝐴 (,) 𝑋 ) ⊆ ℝ → ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑋 ) ) )
464 437 463 ax-mp ⊢ ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑋 ) )
465 464 oveq1i ⊢ ( ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑋 ) ) limℂ 𝐴 )
466 462 465 sseqtri ⊢ ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) limℂ 𝐴 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑋 ) ) limℂ 𝐴 )
467 cncfmptc ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ℝ ∧ ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
468 24 160 160 467 syl3anc ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
469 eqidd ⊢ ( 𝑧 = 𝐴 → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
470 468 1 469 cnmptlimc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( ( 𝑧 ∈ ℝ ↦ ( 𝐺 ‘ 𝑋 ) ) limℂ 𝐴 ) )
471 466 470 sselid ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑋 ) ) limℂ 𝐴 ) )
472 limcresi ⊢ ( 𝐺 limℂ 𝐴 ) ⊆ ( ( 𝐺 ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 )
473 5 121 feqresmpt ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐴 (,) 𝑋 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑧 ) ) )
474 473 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝐴 (,) 𝑋 ) ) limℂ 𝐴 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐴 ) )
475 472 474 sseqtrid ⊢ ( 𝜑 → ( 𝐺 limℂ 𝐴 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐴 ) )
476 475 9 sseldd ⊢ ( 𝜑 → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐴 ) )
477 opelxpi ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ⟨ ( 𝐺 ‘ 𝑋 ) , 0 ⟩ ∈ ( ℂ × ℂ ) )
478 25 453 477 sylancl ⊢ ( 𝜑 → ⟨ ( 𝐺 ‘ 𝑋 ) , 0 ⟩ ∈ ( ℂ × ℂ ) )
479 456 cncnpi ⊢ ( ( − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ⟨ ( 𝐺 ‘ 𝑋 ) , 0 ⟩ ∈ ( ℂ × ℂ ) ) → − ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ⟨ ( 𝐺 ‘ 𝑋 ) , 0 ⟩ ) )
480 452 478 479 sylancr ⊢ ( 𝜑 → − ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ⟨ ( 𝐺 ‘ 𝑋 ) , 0 ⟩ ) )
481 136 140 419 419 55 435 471 476 480 limccnp2 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) − 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
482 461 481 eqeltrrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
483 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) )
484 55 483 divcn ⊢ / ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) Cn ( TopOpen ‘ ℂfld ) )
485 eldifsn ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) )
486 25 32 485 sylanbrc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( ℂ ∖ { 0 } ) )
487 23 486 opelxpd ⊢ ( 𝜑 → ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑋 ) ⟩ ∈ ( ℂ × ( ℂ ∖ { 0 } ) ) )
488 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
489 422 420 488 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) )
490 txtopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) ) → ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) ∈ ( TopOn ‘ ( ℂ × ( ℂ ∖ { 0 } ) ) ) )
491 422 489 490 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) ∈ ( TopOn ‘ ( ℂ × ( ℂ ∖ { 0 } ) ) )
492 491 toponunii ⊢ ( ℂ × ( ℂ ∖ { 0 } ) ) = ∪ ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) )
493 492 cncnpi ⊢ ( ( / ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑋 ) ⟩ ∈ ( ℂ × ( ℂ ∖ { 0 } ) ) ) → / ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑋 ) ⟩ ) )
494 484 487 493 sylancr ⊢ ( 𝜑 → / ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑋 ) ⟩ ) )
495 415 418 419 421 55 431 460 482 494 limccnp2 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) limℂ 𝐴 ) )
496 415 416 225 divcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℂ )
497 496 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) : ( 𝐴 (,) 𝑋 ) ⟶ ℂ )
498 437 159 sstri ⊢ ( 𝐴 (,) 𝑋 ) ⊆ ℂ
499 498 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ⊆ ℂ )
500 497 499 74 55 ellimc2 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) limℂ 𝐴 ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) ) ) )
501 495 500 mpbid ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) ) )
502 501 simprd ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) )
503 notrab ⊢ ( ℂ ∖ { 𝑥 ∈ ℂ ∣ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) = { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 }
504 76 cnmetdval ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐶 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝐶 − 𝑥 ) ) )
505 abssub ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 𝐶 − 𝑥 ) ) = ( abs ‘ ( 𝑥 − 𝐶 ) ) )
506 504 505 eqtrd ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐶 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑥 − 𝐶 ) ) )
507 35 506 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐶 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑥 − 𝐶 ) ) )
508 507 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐶 ( abs ∘ − ) 𝑥 ) ≤ 𝐸 ↔ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 ) )
509 508 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ( 𝐶 ( abs ∘ − ) 𝑥 ) ≤ 𝐸 } = { 𝑥 ∈ ℂ ∣ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } )
510 42 a1i ⊢ ( 𝜑 → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
511 38 rexrd ⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
512 eqid ⊢ { 𝑥 ∈ ℂ ∣ ( 𝐶 ( abs ∘ − ) 𝑥 ) ≤ 𝐸 } = { 𝑥 ∈ ℂ ∣ ( 𝐶 ( abs ∘ − ) 𝑥 ) ≤ 𝐸 }
513 56 512 blcld ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ* ) → { 𝑥 ∈ ℂ ∣ ( 𝐶 ( abs ∘ − ) 𝑥 ) ≤ 𝐸 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
514 510 35 511 513 syl3anc ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ( 𝐶 ( abs ∘ − ) 𝑥 ) ≤ 𝐸 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
515 509 514 eqeltrrd ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
516 427 cldopn ⊢ ( { 𝑥 ∈ ℂ ∣ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) → ( ℂ ∖ { 𝑥 ∈ ℂ ∣ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ∈ ( TopOpen ‘ ℂfld ) )
517 515 516 syl ⊢ ( 𝜑 → ( ℂ ∖ { 𝑥 ∈ ℂ ∣ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ∈ ( TopOpen ‘ ℂfld ) )
518 503 517 eqeltrrid ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ∈ ( TopOpen ‘ ℂfld ) )
519 410 502 518 rspcdva ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ) )
520 405 519 sylbird ⊢ ( 𝜑 → ( ¬ ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ≤ 𝐸 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑧 ) ) / ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) “ ( 𝑣 ∩ ( ( 𝐴 (,) 𝑋 ) ∖ { 𝐴 } ) ) ) ⊆ { 𝑥 ∈ ℂ ∣ ¬ ( abs ‘ ( 𝑥 − 𝐶 ) ) ≤ 𝐸 } ) ) )
521 400 520 mt3d ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) ≤ 𝐸 )
522 38 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
523 522 mulid2d ⊢ ( 𝜑 → ( 1 · 𝐸 ) = 𝐸 )
524 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
525 1lt2 ⊢ 1 < 2
526 525 a1i ⊢ ( 𝜑 → 1 < 2 )
527 524 40 13 526 ltmul1dd ⊢ ( 𝜑 → ( 1 · 𝐸 ) < ( 2 · 𝐸 ) )
528 523 527 eqbrtrrd ⊢ ( 𝜑 → 𝐸 < ( 2 · 𝐸 ) )
529 37 38 41 521 528 lelttrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) − 𝐶 ) ) < ( 2 · 𝐸 ) )