Metamath Proof Explorer

Theorem lmlimxrge0

Description: Relate a limit in the nonnegative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses lmlimxrge0.j 
|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
lmlimxrge0.f 
|- ( ph -> F : NN --> X )
lmlimxrge0.p 
|- ( ph -> P e. X )
lmlimxrge0.x 
|- X C_ ( 0 [,) +oo )
Assertion lmlimxrge0 
|- ( ph -> ( F ( ~~>t ` J ) P <-> F ~~> P ) )

Proof

Step Hyp Ref Expression
1 lmlimxrge0.j 
 |-  J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
2 lmlimxrge0.f 
 |-  ( ph -> F : NN --> X )
3 lmlimxrge0.p 
 |-  ( ph -> P e. X )
4 lmlimxrge0.x 
 |-  X C_ ( 0 [,) +oo )
5 xrge0topn 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
6 1 5 eqtri 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
7 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
8 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
9 resttopon 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) )
10 7 8 9 mp2an 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) )
11 6 10 eqeltri 
 |-  J e. ( TopOn ` ( 0 [,] +oo ) )
12 fvex 
 |-  ( ordTop ` <_ ) e. _V
13 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
14 4 13 sstri 
 |-  X C_ ( 0 [,] +oo )
15 ovex 
 |-  ( 0 [,] +oo ) e. _V
16 restabs 
 |-  ( ( ( ordTop ` <_ ) e. _V /\ X C_ ( 0 [,] +oo ) /\ ( 0 [,] +oo ) e. _V ) -> ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t X ) = ( ( ordTop ` <_ ) |`t X ) )
17 12 14 15 16 mp3an 
 |-  ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t X ) = ( ( ordTop ` <_ ) |`t X )
18 6 oveq1i 
 |-  ( J |`t X ) = ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t X )
19 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
20 4 19 sstri 
 |-  X C_ RR
21 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
22 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
23 21 22 xrrest2 
 |-  ( X C_ RR -> ( ( TopOpen ` CCfld ) |`t X ) = ( ( ordTop ` <_ ) |`t X ) )
24 20 23 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t X ) = ( ( ordTop ` <_ ) |`t X )
25 17 18 24 3eqtr4i 
 |-  ( J |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
26 ax-resscn 
 |-  RR C_ CC
27 20 26 sstri 
 |-  X C_ CC
28 11 2 3 25 27 lmlim 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> F ~~> P ) )