This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupresre

Description: The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis limsupresre.1 
|- ( ph -> F e. V )
Assertion limsupresre 
|- ( ph -> ( limsup ` ( F |` RR ) ) = ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 limsupresre.1 
 |-  ( ph -> F e. V )
2 id 
 |-  ( k e. RR -> k e. RR )
3 pnfxr 
 |-  +oo e. RR*
4 3 a1i 
 |-  ( k e. RR -> +oo e. RR* )
5 icossre 
 |-  ( ( k e. RR /\ +oo e. RR* ) -> ( k [,) +oo ) C_ RR )
6 2 4 5 syl2anc 
 |-  ( k e. RR -> ( k [,) +oo ) C_ RR )
7 resima2 
 |-  ( ( k [,) +oo ) C_ RR -> ( ( F |` RR ) " ( k [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
8 6 7 syl 
 |-  ( k e. RR -> ( ( F |` RR ) " ( k [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
9 8 ineq1d 
 |-  ( k e. RR -> ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
10 9 supeq1d 
 |-  ( k e. RR -> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
11 10 mpteq2ia 
 |-  ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
12 11 a1i 
 |-  ( ph -> ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
13 12 rneqd 
 |-  ( ph -> ran ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
14 13 infeq1d 
 |-  ( ph -> inf ( ran ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
15 1 resexd 
 |-  ( ph -> ( F |` RR ) e. _V )
16 eqid 
 |-  ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
17 16 limsupval 
 |-  ( ( F |` RR ) e. _V -> ( limsup ` ( F |` RR ) ) = inf ( ran ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
18 15 17 syl 
 |-  ( ph -> ( limsup ` ( F |` RR ) ) = inf ( ran ( k e. RR |-> sup ( ( ( ( F |` RR ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
19 eqid 
 |-  ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
20 19 limsupval 
 |-  ( F e. V -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
21 1 20 syl 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
22 14 18 21 3eqtr4d 
 |-  ( ph -> ( limsup ` ( F |` RR ) ) = ( limsup ` F ) )