Metamath Proof Explorer

Theorem lhop

Description: L'HΓ΄pital's Rule. If I is an open set of the reals, F and G are real functions on A containing all of I except possibly B , which are differentiable everywhere on I \ { B } , F and G both approach 0, and the limit of F ' ( x ) / G ' ( x ) at B is C , then the limit F ( x ) / G ( x ) at B also exists and equals C . This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses lhop.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
lhop.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 ⟢ ℝ )
lhop.g ⊒ ( πœ‘ β†’ 𝐺 : 𝐴 ⟢ ℝ )
lhop.i ⊒ ( πœ‘ β†’ 𝐼 ∈ ( topGen β€˜ ran (,) ) )
lhop.b ⊒ ( πœ‘ β†’ 𝐡 ∈ 𝐼 )
lhop.d ⊒ 𝐷 = ( 𝐼 βˆ– { 𝐡 } )
lhop.if ⊒ ( πœ‘ β†’ 𝐷 βŠ† dom ( ℝ D 𝐹 ) )
lhop.ig ⊒ ( πœ‘ β†’ 𝐷 βŠ† dom ( ℝ D 𝐺 ) )
lhop.f0 ⊒ ( πœ‘ β†’ 0 ∈ ( 𝐹 limβ„‚ 𝐡 ) )
lhop.g0 ⊒ ( πœ‘ β†’ 0 ∈ ( 𝐺 limβ„‚ 𝐡 ) )
lhop.gn0 ⊒ ( πœ‘ β†’ Β¬ 0 ∈ ( 𝐺 β€œ 𝐷 ) )
lhop.gd0 ⊒ ( πœ‘ β†’ Β¬ 0 ∈ ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
lhop.c ⊒ ( πœ‘ β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
Assertion lhop ( πœ‘ β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )

Proof

Step Hyp Ref Expression
1 lhop.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
2 lhop.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 ⟢ ℝ )
3 lhop.g ⊒ ( πœ‘ β†’ 𝐺 : 𝐴 ⟢ ℝ )
4 lhop.i ⊒ ( πœ‘ β†’ 𝐼 ∈ ( topGen β€˜ ran (,) ) )
5 lhop.b ⊒ ( πœ‘ β†’ 𝐡 ∈ 𝐼 )
6 lhop.d ⊒ 𝐷 = ( 𝐼 βˆ– { 𝐡 } )
7 lhop.if ⊒ ( πœ‘ β†’ 𝐷 βŠ† dom ( ℝ D 𝐹 ) )
8 lhop.ig ⊒ ( πœ‘ β†’ 𝐷 βŠ† dom ( ℝ D 𝐺 ) )
9 lhop.f0 ⊒ ( πœ‘ β†’ 0 ∈ ( 𝐹 limβ„‚ 𝐡 ) )
10 lhop.g0 ⊒ ( πœ‘ β†’ 0 ∈ ( 𝐺 limβ„‚ 𝐡 ) )
11 lhop.gn0 ⊒ ( πœ‘ β†’ Β¬ 0 ∈ ( 𝐺 β€œ 𝐷 ) )
12 lhop.gd0 ⊒ ( πœ‘ β†’ Β¬ 0 ∈ ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
13 lhop.c ⊒ ( πœ‘ β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
14 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
15 14 rexmet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ )
16 15 a1i ⊒ ( πœ‘ β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) )
17 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
18 14 17 tgioo ⊒ ( topGen β€˜ ran (,) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
19 18 mopni2 ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ 𝐼 ∈ ( topGen β€˜ ran (,) ) ∧ 𝐡 ∈ 𝐼 ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝐼 )
20 16 4 5 19 syl3anc ⊒ ( πœ‘ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝐼 )
21 elssuni ⊒ ( 𝐼 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐼 βŠ† βˆͺ ( topGen β€˜ ran (,) ) )
22 uniretop ⊒ ℝ = βˆͺ ( topGen β€˜ ran (,) )
23 21 22 sseqtrrdi ⊒ ( 𝐼 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐼 βŠ† ℝ )
24 4 23 syl ⊒ ( πœ‘ β†’ 𝐼 βŠ† ℝ )
25 24 5 sseldd ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ )
26 rpre ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ )
27 14 bl2ioo ⊒ ( ( 𝐡 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
28 25 26 27 syl2an ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
29 28 sseq1d ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝐼 ↔ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) )
30 25 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐡 ∈ ℝ )
31 simprl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ π‘Ÿ ∈ ℝ+ )
32 31 rpred ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ π‘Ÿ ∈ ℝ )
33 30 32 resubcld ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 βˆ’ π‘Ÿ ) ∈ ℝ )
34 33 rexrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 βˆ’ π‘Ÿ ) ∈ ℝ* )
35 30 31 ltsubrpd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 βˆ’ π‘Ÿ ) < 𝐡 )
36 2 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐹 : 𝐴 ⟢ ℝ )
37 ssun1 ⊒ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
38 unass ⊒ ( ( { 𝐡 } βˆͺ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( { 𝐡 } βˆͺ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
39 uncom ⊒ ( { 𝐡 } βˆͺ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ { 𝐡 } )
40 39 uneq1i ⊒ ( ( { 𝐡 } βˆͺ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ { 𝐡 } ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
41 38 40 eqtr3i ⊒ ( { 𝐡 } βˆͺ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ { 𝐡 } ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
42 30 rexrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐡 ∈ ℝ* )
43 30 32 readdcld ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 + π‘Ÿ ) ∈ ℝ )
44 43 rexrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 + π‘Ÿ ) ∈ ℝ* )
45 30 31 ltaddrpd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐡 < ( 𝐡 + π‘Ÿ ) )
46 ioojoin ⊒ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ ( 𝐡 + π‘Ÿ ) ∈ ℝ* ) ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) < 𝐡 ∧ 𝐡 < ( 𝐡 + π‘Ÿ ) ) ) β†’ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ { 𝐡 } ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
47 34 42 44 35 45 46 syl32anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ { 𝐡 } ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
48 41 47 eqtrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( { 𝐡 } βˆͺ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
49 elioo2 ⊒ ( ( ( 𝐡 βˆ’ π‘Ÿ ) ∈ ℝ* ∧ ( 𝐡 + π‘Ÿ ) ∈ ℝ* ) β†’ ( 𝐡 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ↔ ( 𝐡 ∈ ℝ ∧ ( 𝐡 βˆ’ π‘Ÿ ) < 𝐡 ∧ 𝐡 < ( 𝐡 + π‘Ÿ ) ) ) )
50 34 44 49 syl2anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ↔ ( 𝐡 ∈ ℝ ∧ ( 𝐡 βˆ’ π‘Ÿ ) < 𝐡 ∧ 𝐡 < ( 𝐡 + π‘Ÿ ) ) ) )
51 30 35 45 50 mpbir3and ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐡 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
52 51 snssd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ { 𝐡 } βŠ† ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
53 incom ⊒ ( { 𝐡 } ∩ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ∩ { 𝐡 } )
54 ubioo ⊒ Β¬ 𝐡 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 )
55 lbioo ⊒ Β¬ 𝐡 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) )
56 54 55 pm3.2ni ⊒ Β¬ ( 𝐡 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ∨ 𝐡 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
57 elun ⊒ ( 𝐡 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ↔ ( 𝐡 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ∨ 𝐡 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
58 56 57 mtbir ⊒ Β¬ 𝐡 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
59 disjsn ⊒ ( ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ∩ { 𝐡 } ) = βˆ… ↔ Β¬ 𝐡 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
60 58 59 mpbir ⊒ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ∩ { 𝐡 } ) = βˆ…
61 53 60 eqtri ⊒ ( { 𝐡 } ∩ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = βˆ…
62 uneqdifeq ⊒ ( ( { 𝐡 } βŠ† ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∧ ( { 𝐡 } ∩ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = βˆ… ) β†’ ( ( { 𝐡 } βˆͺ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ↔ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) = ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
63 52 61 62 sylancl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( { 𝐡 } βˆͺ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ↔ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) = ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
64 48 63 mpbid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) = ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
65 37 64 sseqtrrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) )
66 ssdif ⊒ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βŠ† ( 𝐼 βˆ– { 𝐡 } ) )
67 66 ad2antll ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βŠ† ( 𝐼 βˆ– { 𝐡 } ) )
68 67 6 sseqtrrdi ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βŠ† 𝐷 )
69 ax-resscn ⊒ ℝ βŠ† β„‚
70 69 a1i ⊒ ( πœ‘ β†’ ℝ βŠ† β„‚ )
71 fss ⊒ ( ( 𝐹 : 𝐴 ⟢ ℝ ∧ ℝ βŠ† β„‚ ) β†’ 𝐹 : 𝐴 ⟢ β„‚ )
72 2 69 71 sylancl ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 ⟢ β„‚ )
73 70 72 1 dvbss ⊒ ( πœ‘ β†’ dom ( ℝ D 𝐹 ) βŠ† 𝐴 )
74 7 73 sstrd ⊒ ( πœ‘ β†’ 𝐷 βŠ† 𝐴 )
75 74 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐷 βŠ† 𝐴 )
76 68 75 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βŠ† 𝐴 )
77 65 76 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† 𝐴 )
78 36 77 fssresd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) : ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ⟢ ℝ )
79 3 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐺 : 𝐴 ⟢ ℝ )
80 79 77 fssresd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) : ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ⟢ ℝ )
81 69 a1i ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ℝ βŠ† β„‚ )
82 72 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐹 : 𝐴 ⟢ β„‚ )
83 1 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐴 βŠ† ℝ )
84 ioossre ⊒ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† ℝ
85 84 a1i ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† ℝ )
86 eqid ⊒ ( TopOpen β€˜ β„‚fld ) = ( TopOpen β€˜ β„‚fld )
87 86 tgioo2 ⊒ ( topGen β€˜ ran (,) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ )
88 86 87 dvres ⊒ ( ( ( ℝ βŠ† β„‚ ∧ 𝐹 : 𝐴 ⟢ β„‚ ) ∧ ( 𝐴 βŠ† ℝ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† ℝ ) ) β†’ ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) )
89 81 82 83 85 88 syl22anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) )
90 retop ⊒ ( topGen β€˜ ran (,) ) ∈ Top
91 iooretop ⊒ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ∈ ( topGen β€˜ ran (,) )
92 isopn3i ⊒ ( ( ( topGen β€˜ ran (,) ) ∈ Top ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ∈ ( topGen β€˜ ran (,) ) ) β†’ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
93 90 91 92 mp2an ⊒ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 )
94 93 reseq2i ⊒ ( ( ℝ D 𝐹 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
95 89 94 eqtrdi ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
96 95 dmeqd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = dom ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
97 65 68 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† 𝐷 )
98 7 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐷 βŠ† dom ( ℝ D 𝐹 ) )
99 97 98 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† dom ( ℝ D 𝐹 ) )
100 ssdmres ⊒ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
101 99 100 sylib ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
102 96 101 eqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
103 fss ⊒ ( ( 𝐺 : 𝐴 ⟢ ℝ ∧ ℝ βŠ† β„‚ ) β†’ 𝐺 : 𝐴 ⟢ β„‚ )
104 3 69 103 sylancl ⊒ ( πœ‘ β†’ 𝐺 : 𝐴 ⟢ β„‚ )
105 104 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐺 : 𝐴 ⟢ β„‚ )
106 86 87 dvres ⊒ ( ( ( ℝ βŠ† β„‚ ∧ 𝐺 : 𝐴 ⟢ β„‚ ) ∧ ( 𝐴 βŠ† ℝ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† ℝ ) ) β†’ ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) )
107 81 105 83 85 106 syl22anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) )
108 93 reseq2i ⊒ ( ( ℝ D 𝐺 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
109 107 108 eqtrdi ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
110 109 dmeqd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = dom ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
111 8 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐷 βŠ† dom ( ℝ D 𝐺 ) )
112 97 111 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† dom ( ℝ D 𝐺 ) )
113 ssdmres ⊒ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† dom ( ℝ D 𝐺 ) ↔ dom ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
114 112 113 sylib ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
115 110 114 eqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
116 limcresi ⊒ ( 𝐹 limβ„‚ 𝐡 ) βŠ† ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 )
117 9 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 0 ∈ ( 𝐹 limβ„‚ 𝐡 ) )
118 116 117 sselid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 0 ∈ ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) )
119 limcresi ⊒ ( 𝐺 limβ„‚ 𝐡 ) βŠ† ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 )
120 10 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 0 ∈ ( 𝐺 limβ„‚ 𝐡 ) )
121 119 120 sselid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 0 ∈ ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) )
122 df-ima ⊒ ( 𝐺 β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ran ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
123 imass2 ⊒ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† 𝐷 β†’ ( 𝐺 β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βŠ† ( 𝐺 β€œ 𝐷 ) )
124 97 123 syl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐺 β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βŠ† ( 𝐺 β€œ 𝐷 ) )
125 122 124 eqsstrrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βŠ† ( 𝐺 β€œ 𝐷 ) )
126 11 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ Β¬ 0 ∈ ( 𝐺 β€œ 𝐷 ) )
127 125 126 ssneldd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ Β¬ 0 ∈ ran ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
128 109 rneqd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ran ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
129 df-ima ⊒ ( ( ℝ D 𝐺 ) β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ran ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) )
130 128 129 eqtr4di ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) = ( ( ℝ D 𝐺 ) β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) )
131 imass2 ⊒ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† 𝐷 β†’ ( ( ℝ D 𝐺 ) β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βŠ† ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
132 97 131 syl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ℝ D 𝐺 ) β€œ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) βŠ† ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
133 130 132 eqsstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) βŠ† ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
134 12 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ Β¬ 0 ∈ ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
135 133 134 ssneldd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ Β¬ 0 ∈ ran ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) )
136 limcresi ⊒ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) βŠ† ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 )
137 97 resmptd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) )
138 95 fveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) = ( ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) )
139 fvres ⊒ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) β†’ ( ( ( ℝ D 𝐹 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) )
140 138 139 sylan9eq ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β†’ ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) )
141 109 fveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) = ( ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) )
142 fvres ⊒ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) β†’ ( ( ( ℝ D 𝐺 ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) )
143 141 142 sylan9eq ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β†’ ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) )
144 140 143 oveq12d ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β†’ ( ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) )
145 144 mpteq2dva ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) )
146 137 145 eqtr4d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) ) ) )
147 146 oveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) = ( ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
148 136 147 sseqtrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) βŠ† ( ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
149 13 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
150 148 149 sseldd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
151 34 30 35 78 80 102 115 118 121 127 135 150 lhop2 ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
152 65 resmptd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) )
153 fvres ⊒ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) β†’ ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) = ( 𝐹 β€˜ 𝑧 ) )
154 fvres ⊒ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) β†’ ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) = ( 𝐺 β€˜ 𝑧 ) )
155 153 154 oveq12d ⊒ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) β†’ ( ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) ) = ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) )
156 155 mpteq2ia ⊒ ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) )
157 152 156 eqtr4di ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) = ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) ) ) )
158 157 oveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) = ( ( 𝑧 ∈ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ↦ ( ( ( 𝐹 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
159 151 158 eleqtrrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) )
160 ssun2 ⊒ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
161 160 64 sseqtrrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) )
162 161 76 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐴 )
163 36 162 fssresd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) : ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ⟢ ℝ )
164 79 162 fssresd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) : ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ⟢ ℝ )
165 ioossre ⊒ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† ℝ
166 165 a1i ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† ℝ )
167 86 87 dvres ⊒ ( ( ( ℝ βŠ† β„‚ ∧ 𝐹 : 𝐴 ⟢ β„‚ ) ∧ ( 𝐴 βŠ† ℝ ∧ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† ℝ ) ) β†’ ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
168 81 82 83 166 167 syl22anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
169 iooretop ⊒ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( topGen β€˜ ran (,) )
170 isopn3i ⊒ ( ( ( topGen β€˜ ran (,) ) ∈ Top ∧ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( topGen β€˜ ran (,) ) ) β†’ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
171 90 169 170 mp2an ⊒ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) )
172 171 reseq2i ⊒ ( ( ℝ D 𝐹 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
173 168 172 eqtrdi ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
174 173 dmeqd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = dom ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
175 161 68 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐷 )
176 175 98 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† dom ( ℝ D 𝐹 ) )
177 ssdmres ⊒ ( ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
178 176 177 sylib ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
179 174 178 eqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
180 86 87 dvres ⊒ ( ( ( ℝ βŠ† β„‚ ∧ 𝐺 : 𝐴 ⟢ β„‚ ) ∧ ( 𝐴 βŠ† ℝ ∧ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† ℝ ) ) β†’ ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
181 81 105 83 166 180 syl22anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
182 171 reseq2i ⊒ ( ( ℝ D 𝐺 ) β†Ύ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
183 181 182 eqtrdi ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
184 183 dmeqd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = dom ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
185 175 111 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† dom ( ℝ D 𝐺 ) )
186 ssdmres ⊒ ( ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† dom ( ℝ D 𝐺 ) ↔ dom ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
187 185 186 sylib ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
188 184 187 eqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ dom ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
189 limcresi ⊒ ( 𝐹 limβ„‚ 𝐡 ) βŠ† ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 )
190 189 117 sselid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 0 ∈ ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) )
191 limcresi ⊒ ( 𝐺 limβ„‚ 𝐡 ) βŠ† ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 )
192 191 120 sselid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 0 ∈ ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) )
193 df-ima ⊒ ( 𝐺 β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ran ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
194 imass2 ⊒ ( ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐷 β†’ ( 𝐺 β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) βŠ† ( 𝐺 β€œ 𝐷 ) )
195 175 194 syl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐺 β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) βŠ† ( 𝐺 β€œ 𝐷 ) )
196 193 195 eqsstrrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) βŠ† ( 𝐺 β€œ 𝐷 ) )
197 196 126 ssneldd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ Β¬ 0 ∈ ran ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
198 183 rneqd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ran ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
199 df-ima ⊒ ( ( ℝ D 𝐺 ) β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ran ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) )
200 198 199 eqtr4di ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) = ( ( ℝ D 𝐺 ) β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) )
201 imass2 ⊒ ( ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐷 β†’ ( ( ℝ D 𝐺 ) β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) βŠ† ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
202 175 201 syl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ℝ D 𝐺 ) β€œ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) βŠ† ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
203 200 202 eqsstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ran ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) βŠ† ( ( ℝ D 𝐺 ) β€œ 𝐷 ) )
204 203 134 ssneldd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ Β¬ 0 ∈ ran ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) )
205 limcresi ⊒ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) βŠ† ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 )
206 175 resmptd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) )
207 173 fveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) = ( ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) )
208 fvres ⊒ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) β†’ ( ( ( ℝ D 𝐹 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) )
209 207 208 sylan9eq ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β†’ ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) )
210 183 fveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) = ( ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) )
211 fvres ⊒ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) β†’ ( ( ( ℝ D 𝐺 ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) )
212 210 211 sylan9eq ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β†’ ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) = ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) )
213 209 212 oveq12d ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β†’ ( ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) )
214 213 mpteq2dva ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) )
215 206 214 eqtr4d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) ) ) )
216 215 oveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) = ( ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
217 205 216 sseqtrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) β€˜ 𝑧 ) / ( ( ℝ D 𝐺 ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) βŠ† ( ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
218 217 149 sseldd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( ℝ D ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) / ( ( ℝ D ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
219 30 44 45 163 164 179 188 190 192 197 204 218 lhop1 ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
220 161 resmptd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) )
221 fvres ⊒ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) β†’ ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) = ( 𝐹 β€˜ 𝑧 ) )
222 fvres ⊒ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) β†’ ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) = ( 𝐺 β€˜ 𝑧 ) )
223 221 222 oveq12d ⊒ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) β†’ ( ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) ) = ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) )
224 223 mpteq2ia ⊒ ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) )
225 220 224 eqtr4di ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) = ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) ) ) )
226 225 oveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) = ( ( 𝑧 ∈ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ↦ ( ( ( 𝐹 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) / ( ( 𝐺 β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
227 219 226 eleqtrrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) )
228 159 227 elind ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) ∩ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) ) )
229 68 resmptd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ) = ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) )
230 229 oveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ) limβ„‚ 𝐡 ) = ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
231 74 sselda ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ 𝑧 ∈ 𝐴 )
232 2 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐴 ) β†’ ( 𝐹 β€˜ 𝑧 ) ∈ ℝ )
233 231 232 syldan ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐹 β€˜ 𝑧 ) ∈ ℝ )
234 233 recnd ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐹 β€˜ 𝑧 ) ∈ β„‚ )
235 3 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐴 ) β†’ ( 𝐺 β€˜ 𝑧 ) ∈ ℝ )
236 231 235 syldan ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐺 β€˜ 𝑧 ) ∈ ℝ )
237 236 recnd ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐺 β€˜ 𝑧 ) ∈ β„‚ )
238 11 adantr ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ Β¬ 0 ∈ ( 𝐺 β€œ 𝐷 ) )
239 3 ffnd ⊒ ( πœ‘ β†’ 𝐺 Fn 𝐴 )
240 239 adantr ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ 𝐺 Fn 𝐴 )
241 74 adantr ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ 𝐷 βŠ† 𝐴 )
242 simpr ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ 𝑧 ∈ 𝐷 )
243 fnfvima ⊒ ( ( 𝐺 Fn 𝐴 ∧ 𝐷 βŠ† 𝐴 ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐺 β€˜ 𝑧 ) ∈ ( 𝐺 β€œ 𝐷 ) )
244 240 241 242 243 syl3anc ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐺 β€˜ 𝑧 ) ∈ ( 𝐺 β€œ 𝐷 ) )
245 eleq1 ⊒ ( ( 𝐺 β€˜ 𝑧 ) = 0 β†’ ( ( 𝐺 β€˜ 𝑧 ) ∈ ( 𝐺 β€œ 𝐷 ) ↔ 0 ∈ ( 𝐺 β€œ 𝐷 ) ) )
246 244 245 syl5ibcom ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( ( 𝐺 β€˜ 𝑧 ) = 0 β†’ 0 ∈ ( 𝐺 β€œ 𝐷 ) ) )
247 246 necon3bd ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( Β¬ 0 ∈ ( 𝐺 β€œ 𝐷 ) β†’ ( 𝐺 β€˜ 𝑧 ) β‰  0 ) )
248 238 247 mpd ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( 𝐺 β€˜ 𝑧 ) β‰  0 )
249 234 237 248 divcld ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐷 ) β†’ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ∈ β„‚ )
250 249 adantlr ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ 𝐷 ) β†’ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ∈ β„‚ )
251 250 fmpttd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) : 𝐷 ⟢ β„‚ )
252 difss ⊒ ( 𝐼 βˆ– { 𝐡 } ) βŠ† 𝐼
253 6 252 eqsstri ⊒ 𝐷 βŠ† 𝐼
254 24 69 sstrdi ⊒ ( πœ‘ β†’ 𝐼 βŠ† β„‚ )
255 253 254 sstrid ⊒ ( πœ‘ β†’ 𝐷 βŠ† β„‚ )
256 255 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐷 βŠ† β„‚ )
257 eqid ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) )
258 6 uneq1i ⊒ ( 𝐷 βˆͺ { 𝐡 } ) = ( ( 𝐼 βˆ– { 𝐡 } ) βˆͺ { 𝐡 } )
259 undif1 ⊒ ( ( 𝐼 βˆ– { 𝐡 } ) βˆͺ { 𝐡 } ) = ( 𝐼 βˆͺ { 𝐡 } )
260 258 259 eqtri ⊒ ( 𝐷 βˆͺ { 𝐡 } ) = ( 𝐼 βˆͺ { 𝐡 } )
261 simprr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 )
262 52 261 sstrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ { 𝐡 } βŠ† 𝐼 )
263 ssequn2 ⊒ ( { 𝐡 } βŠ† 𝐼 ↔ ( 𝐼 βˆͺ { 𝐡 } ) = 𝐼 )
264 262 263 sylib ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐼 βˆͺ { 𝐡 } ) = 𝐼 )
265 260 264 eqtrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐷 βˆͺ { 𝐡 } ) = 𝐼 )
266 265 oveq2d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) )
267 24 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐼 βŠ† ℝ )
268 eqid ⊒ ( topGen β€˜ ran (,) ) = ( topGen β€˜ ran (,) )
269 86 268 rerest ⊒ ( 𝐼 βŠ† ℝ β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) = ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) )
270 267 269 syl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) = ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) )
271 266 270 eqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) = ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) )
272 271 fveq2d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) = ( int β€˜ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ) )
273 272 fveq1d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( int β€˜ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) )
274 86 cnfldtopon ⊒ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ )
275 254 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐼 βŠ† β„‚ )
276 resttopon ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ ) ∧ 𝐼 βŠ† β„‚ ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) ∈ ( TopOn β€˜ 𝐼 ) )
277 274 275 276 sylancr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) ∈ ( TopOn β€˜ 𝐼 ) )
278 topontop ⊒ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) ∈ ( TopOn β€˜ 𝐼 ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) ∈ Top )
279 277 278 syl ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝐼 ) ∈ Top )
280 270 279 eqeltrrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ∈ Top )
281 iooretop ⊒ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( topGen β€˜ ran (,) )
282 281 a1i ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( topGen β€˜ ran (,) ) )
283 4 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐼 ∈ ( topGen β€˜ ran (,) ) )
284 restopn2 ⊒ ( ( ( topGen β€˜ ran (,) ) ∈ Top ∧ 𝐼 ∈ ( topGen β€˜ ran (,) ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ↔ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( topGen β€˜ ran (,) ) ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) )
285 90 283 284 sylancr ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ↔ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( topGen β€˜ ran (,) ) ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) )
286 282 261 285 mpbir2and ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) )
287 isopn3i ⊒ ( ( ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ∈ Top ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ∈ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ) β†’ ( ( int β€˜ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
288 280 286 287 syl2anc ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( int β€˜ ( ( topGen β€˜ ran (,) ) β†Ύt 𝐼 ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
289 273 288 eqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
290 51 289 eleqtrrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐡 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) )
291 undif1 ⊒ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βˆͺ { 𝐡 } ) = ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆͺ { 𝐡 } )
292 ssequn2 ⊒ ( { 𝐡 } βŠ† ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ↔ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆͺ { 𝐡 } ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
293 52 292 sylib ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆͺ { 𝐡 } ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
294 291 293 eqtrid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βˆͺ { 𝐡 } ) = ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) )
295 294 fveq2d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) β€˜ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βˆͺ { 𝐡 } ) ) = ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) β€˜ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) ) )
296 290 295 eleqtrrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐡 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐷 βˆͺ { 𝐡 } ) ) ) β€˜ ( ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) βˆͺ { 𝐡 } ) ) )
297 251 68 256 86 257 296 limcres ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ) limβ„‚ 𝐡 ) = ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
298 84 69 sstri ⊒ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† β„‚
299 298 a1i ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βŠ† β„‚ )
300 165 69 sstri ⊒ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† β„‚
301 300 a1i ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) βŠ† β„‚ )
302 68 sselda ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ) β†’ 𝑧 ∈ 𝐷 )
303 302 250 syldan ⊒ ( ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) ∧ 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ) β†’ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ∈ β„‚ )
304 303 fmpttd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) : ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ⟢ β„‚ )
305 64 feq2d ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) : ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ⟢ β„‚ ↔ ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) : ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ⟢ β„‚ ) )
306 304 305 mpbid ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) : ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) βˆͺ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) ⟢ β„‚ )
307 299 301 306 limcun ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) = ( ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) ∩ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) ) )
308 230 297 307 3eqtr3rd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ ( ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) 𝐡 ) ) limβ„‚ 𝐡 ) ∩ ( ( ( 𝑧 ∈ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βˆ– { 𝐡 } ) ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) β†Ύ ( 𝐡 (,) ( 𝐡 + π‘Ÿ ) ) ) limβ„‚ 𝐡 ) ) = ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
309 228 308 eleqtrd ⊒ ( ( πœ‘ ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 ) ) β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )
310 309 expr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( ( 𝐡 βˆ’ π‘Ÿ ) (,) ( 𝐡 + π‘Ÿ ) ) βŠ† 𝐼 β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) ) )
311 29 310 sylbid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝐼 β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) ) )
312 311 rexlimdva ⊒ ( πœ‘ β†’ ( βˆƒ π‘Ÿ ∈ ℝ+ ( 𝐡 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝐼 β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) ) )
313 20 312 mpd ⊒ ( πœ‘ β†’ 𝐢 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 β€˜ 𝑧 ) / ( 𝐺 β€˜ 𝑧 ) ) ) limβ„‚ 𝐡 ) )