Metamath Proof Explorer

Theorem limsup10ex

Description: The superior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis limsup10ex.1 
|- F = ( n e. NN |-> if ( 2 || n , 0 , 1 ) )
Assertion limsup10ex 
|- ( limsup ` F ) = 1

Proof

Step Hyp Ref Expression
1 limsup10ex.1 
 |-  F = ( n e. NN |-> if ( 2 || n , 0 , 1 ) )
2 nftru 
 |-  F/ k T.
3 nnex 
 |-  NN e. _V
4 3 a1i 
 |-  ( T. -> NN e. _V )
5 0xr 
 |-  0 e. RR*
6 5 a1i 
 |-  ( n e. NN -> 0 e. RR* )
7 1xr 
 |-  1 e. RR*
8 7 a1i 
 |-  ( n e. NN -> 1 e. RR* )
9 6 8 ifcld 
 |-  ( n e. NN -> if ( 2 || n , 0 , 1 ) e. RR* )
10 1 9 fmpti 
 |-  F : NN --> RR*
11 10 a1i 
 |-  ( T. -> F : NN --> RR* )
12 eqid 
 |-  ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )
13 2 4 11 12 limsupval3 
 |-  ( T. -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) )
14 13 mptru 
 |-  ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < )
15 id 
 |-  ( k e. RR -> k e. RR )
16 1 15 limsup10exlem 
 |-  ( k e. RR -> ( F " ( k [,) +oo ) ) = { 0 , 1 } )
17 16 supeq1d 
 |-  ( k e. RR -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) = sup ( { 0 , 1 } , RR* , < ) )
18 xrltso 
 |-  < Or RR*
19 suppr 
 |-  ( ( < Or RR* /\ 0 e. RR* /\ 1 e. RR* ) -> sup ( { 0 , 1 } , RR* , < ) = if ( 1 < 0 , 0 , 1 ) )
20 18 5 7 19 mp3an 
 |-  sup ( { 0 , 1 } , RR* , < ) = if ( 1 < 0 , 0 , 1 )
21 0le1 
 |-  0 <_ 1
22 0re 
 |-  0 e. RR
23 1re 
 |-  1 e. RR
24 22 23 lenlti 
 |-  ( 0 <_ 1 <-> -. 1 < 0 )
25 21 24 mpbi 
 |-  -. 1 < 0
26 25 iffalsei 
 |-  if ( 1 < 0 , 0 , 1 ) = 1
27 20 26 eqtri 
 |-  sup ( { 0 , 1 } , RR* , < ) = 1
28 17 27 eqtrdi 
 |-  ( k e. RR -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) = 1 )
29 28 mpteq2ia 
 |-  ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ( k e. RR |-> 1 )
30 29 rneqi 
 |-  ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ran ( k e. RR |-> 1 )
31 eqid 
 |-  ( k e. RR |-> 1 ) = ( k e. RR |-> 1 )
32 ren0 
 |-  RR =/= (/)
33 32 a1i 
 |-  ( T. -> RR =/= (/) )
34 31 33 rnmptc 
 |-  ( T. -> ran ( k e. RR |-> 1 ) = { 1 } )
35 34 mptru 
 |-  ran ( k e. RR |-> 1 ) = { 1 }
36 30 35 eqtri 
 |-  ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = { 1 }
37 36 infeq1i 
 |-  inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) = inf ( { 1 } , RR* , < )
38 infsn 
 |-  ( ( < Or RR* /\ 1 e. RR* ) -> inf ( { 1 } , RR* , < ) = 1 )
39 18 7 38 mp2an 
 |-  inf ( { 1 } , RR* , < ) = 1
40 14 37 39 3eqtri 
 |-  ( limsup ` F ) = 1