Metamath Proof Explorer

Theorem liminf10ex

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

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

Proof

Step Hyp Ref Expression
1 liminf10ex.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 |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) )
13 2 4 11 12 liminfval5 
 |-  ( T. -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) )
14 13 mptru 
 |-  ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( 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 infeq1d 
 |-  ( k e. RR -> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) = inf ( { 0 , 1 } , RR* , < ) )
18 xrltso 
 |-  < Or RR*
19 infpr 
 |-  ( ( < Or RR* /\ 0 e. RR* /\ 1 e. RR* ) -> inf ( { 0 , 1 } , RR* , < ) = if ( 0 < 1 , 0 , 1 ) )
20 18 5 7 19 mp3an 
 |-  inf ( { 0 , 1 } , RR* , < ) = if ( 0 < 1 , 0 , 1 )
21 0lt1 
 |-  0 < 1
22 21 iftruei 
 |-  if ( 0 < 1 , 0 , 1 ) = 0
23 20 22 eqtri 
 |-  inf ( { 0 , 1 } , RR* , < ) = 0
24 17 23 eqtrdi 
 |-  ( k e. RR -> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) = 0 )
25 24 mpteq2ia 
 |-  ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ( k e. RR |-> 0 )
26 25 rneqi 
 |-  ran ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ran ( k e. RR |-> 0 )
27 eqid 
 |-  ( k e. RR |-> 0 ) = ( k e. RR |-> 0 )
28 ren0 
 |-  RR =/= (/)
29 28 a1i 
 |-  ( T. -> RR =/= (/) )
30 27 29 rnmptc 
 |-  ( T. -> ran ( k e. RR |-> 0 ) = { 0 } )
31 30 mptru 
 |-  ran ( k e. RR |-> 0 ) = { 0 }
32 26 31 eqtri 
 |-  ran ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = { 0 }
33 32 supeq1i 
 |-  sup ( ran ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) = sup ( { 0 } , RR* , < )
34 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
35 18 5 34 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
36 14 33 35 3eqtri 
 |-  ( liminf ` F ) = 0