Metamath Proof Explorer

Theorem limsup10exlem

Description: The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsup10exlem.1 
|- F = ( n e. NN |-> if ( 2 || n , 0 , 1 ) )
limsup10exlem.2 
|- ( ph -> K e. RR )
Assertion limsup10exlem 
|- ( ph -> ( F " ( K [,) +oo ) ) = { 0 , 1 } )

Proof

Step Hyp Ref Expression
1 limsup10exlem.1 
 |-  F = ( n e. NN |-> if ( 2 || n , 0 , 1 ) )
2 limsup10exlem.2 
 |-  ( ph -> K e. RR )
3 c0ex 
 |-  0 e. _V
4 3 prid1 
 |-  0 e. { 0 , 1 }
5 1re 
 |-  1 e. RR
6 5 elexi 
 |-  1 e. _V
7 6 prid2 
 |-  1 e. { 0 , 1 }
8 4 7 ifcli 
 |-  if ( 2 || n , 0 , 1 ) e. { 0 , 1 }
9 8 a1i 
 |-  ( ( ph /\ n e. ( NN i^i ( K [,) +oo ) ) ) -> if ( 2 || n , 0 , 1 ) e. { 0 , 1 } )
10 9 ralrimiva 
 |-  ( ph -> A. n e. ( NN i^i ( K [,) +oo ) ) if ( 2 || n , 0 , 1 ) e. { 0 , 1 } )
11 nfv 
 |-  F/ n ph
12 3 6 ifex 
 |-  if ( 2 || n , 0 , 1 ) e. _V
13 12 a1i 
 |-  ( ( ph /\ n e. ( NN i^i ( K [,) +oo ) ) ) -> if ( 2 || n , 0 , 1 ) e. _V )
14 11 13 1 imassmpt 
 |-  ( ph -> ( ( F " ( K [,) +oo ) ) C_ { 0 , 1 } <-> A. n e. ( NN i^i ( K [,) +oo ) ) if ( 2 || n , 0 , 1 ) e. { 0 , 1 } ) )
15 10 14 mpbird 
 |-  ( ph -> ( F " ( K [,) +oo ) ) C_ { 0 , 1 } )
16 2 ceilcld 
 |-  ( ph -> ( |^ ` K ) e. ZZ )
17 1zzd 
 |-  ( ph -> 1 e. ZZ )
18 16 17 ifcld 
 |-  ( ph -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. ZZ )
19 18 adantr 
 |-  ( ( ph /\ n = ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. ZZ )
20 simpr 
 |-  ( ( ph /\ n = ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) -> n = ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) )
21 2teven 
 |-  ( ( if ( 1 <_ K , ( |^ ` K ) , 1 ) e. ZZ /\ n = ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) -> 2 || n )
22 19 20 21 syl2anc 
 |-  ( ( ph /\ n = ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) -> 2 || n )
23 22 iftrued 
 |-  ( ( ph /\ n = ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) -> if ( 2 || n , 0 , 1 ) = 0 )
24 2nn 
 |-  2 e. NN
25 24 a1i 
 |-  ( ph -> 2 e. NN )
26 eqid 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
27 5 a1i 
 |-  ( ( ph /\ 1 <_ K ) -> 1 e. RR )
28 2 adantr 
 |-  ( ( ph /\ 1 <_ K ) -> K e. RR )
29 16 zred 
 |-  ( ph -> ( |^ ` K ) e. RR )
30 29 adantr 
 |-  ( ( ph /\ 1 <_ K ) -> ( |^ ` K ) e. RR )
31 simpr 
 |-  ( ( ph /\ 1 <_ K ) -> 1 <_ K )
32 2 ceilged 
 |-  ( ph -> K <_ ( |^ ` K ) )
33 32 adantr 
 |-  ( ( ph /\ 1 <_ K ) -> K <_ ( |^ ` K ) )
34 27 28 30 31 33 letrd 
 |-  ( ( ph /\ 1 <_ K ) -> 1 <_ ( |^ ` K ) )
35 iftrue 
 |-  ( 1 <_ K -> if ( 1 <_ K , ( |^ ` K ) , 1 ) = ( |^ ` K ) )
36 35 adantl 
 |-  ( ( ph /\ 1 <_ K ) -> if ( 1 <_ K , ( |^ ` K ) , 1 ) = ( |^ ` K ) )
37 34 36 breqtrrd 
 |-  ( ( ph /\ 1 <_ K ) -> 1 <_ if ( 1 <_ K , ( |^ ` K ) , 1 ) )
38 5 leidi 
 |-  1 <_ 1
39 38 a1i 
 |-  ( ( ph /\ -. 1 <_ K ) -> 1 <_ 1 )
40 iffalse 
 |-  ( -. 1 <_ K -> if ( 1 <_ K , ( |^ ` K ) , 1 ) = 1 )
41 40 adantl 
 |-  ( ( ph /\ -. 1 <_ K ) -> if ( 1 <_ K , ( |^ ` K ) , 1 ) = 1 )
42 39 41 breqtrrd 
 |-  ( ( ph /\ -. 1 <_ K ) -> 1 <_ if ( 1 <_ K , ( |^ ` K ) , 1 ) )
43 37 42 pm2.61dan 
 |-  ( ph -> 1 <_ if ( 1 <_ K , ( |^ ` K ) , 1 ) )
44 26 17 18 43 eluzd 
 |-  ( ph -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. ( ZZ>= ` 1 ) )
45 nnuz 
 |-  NN = ( ZZ>= ` 1 )
46 44 45 eleqtrrdi 
 |-  ( ph -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. NN )
47 25 46 nnmulcld 
 |-  ( ph -> ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) e. NN )
48 3 a1i 
 |-  ( ph -> 0 e. _V )
49 1 23 47 48 fvmptd2 
 |-  ( ph -> ( F ` ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) = 0 )
50 12 1 fnmpti 
 |-  F Fn NN
51 50 a1i 
 |-  ( ph -> F Fn NN )
52 2 rexrd 
 |-  ( ph -> K e. RR* )
53 pnfxr 
 |-  +oo e. RR*
54 53 a1i 
 |-  ( ph -> +oo e. RR* )
55 47 nnxrd 
 |-  ( ph -> ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) e. RR* )
56 47 nnred 
 |-  ( ph -> ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) e. RR )
57 46 nnred 
 |-  ( ph -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. RR )
58 33 36 breqtrrd 
 |-  ( ( ph /\ 1 <_ K ) -> K <_ if ( 1 <_ K , ( |^ ` K ) , 1 ) )
59 2 adantr 
 |-  ( ( ph /\ -. 1 <_ K ) -> K e. RR )
60 5 a1i 
 |-  ( ( ph /\ -. 1 <_ K ) -> 1 e. RR )
61 simpr 
 |-  ( ( ph /\ -. 1 <_ K ) -> -. 1 <_ K )
62 59 60 61 nleltd 
 |-  ( ( ph /\ -. 1 <_ K ) -> K < 1 )
63 59 60 62 ltled 
 |-  ( ( ph /\ -. 1 <_ K ) -> K <_ 1 )
64 41 eqcomd 
 |-  ( ( ph /\ -. 1 <_ K ) -> 1 = if ( 1 <_ K , ( |^ ` K ) , 1 ) )
65 63 64 breqtrd 
 |-  ( ( ph /\ -. 1 <_ K ) -> K <_ if ( 1 <_ K , ( |^ ` K ) , 1 ) )
66 58 65 pm2.61dan 
 |-  ( ph -> K <_ if ( 1 <_ K , ( |^ ` K ) , 1 ) )
67 46 nnrpd 
 |-  ( ph -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. RR+ )
68 2timesgt 
 |-  ( if ( 1 <_ K , ( |^ ` K ) , 1 ) e. RR+ -> if ( 1 <_ K , ( |^ ` K ) , 1 ) < ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) )
69 67 68 syl 
 |-  ( ph -> if ( 1 <_ K , ( |^ ` K ) , 1 ) < ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) )
70 2 57 56 66 69 lelttrd 
 |-  ( ph -> K < ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) )
71 2 56 70 ltled 
 |-  ( ph -> K <_ ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) )
72 56 ltpnfd 
 |-  ( ph -> ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) < +oo )
73 52 54 55 71 72 elicod 
 |-  ( ph -> ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) e. ( K [,) +oo ) )
74 51 47 73 fnfvimad 
 |-  ( ph -> ( F ` ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) ) e. ( F " ( K [,) +oo ) ) )
75 49 74 eqeltrrd 
 |-  ( ph -> 0 e. ( F " ( K [,) +oo ) ) )
76 18 adantr 
 |-  ( ( ph /\ n = ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) -> if ( 1 <_ K , ( |^ ` K ) , 1 ) e. ZZ )
77 simpr 
 |-  ( ( ph /\ n = ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) -> n = ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) )
78 2tp1odd 
 |-  ( ( if ( 1 <_ K , ( |^ ` K ) , 1 ) e. ZZ /\ n = ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) -> -. 2 || n )
79 76 77 78 syl2anc 
 |-  ( ( ph /\ n = ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) -> -. 2 || n )
80 79 iffalsed 
 |-  ( ( ph /\ n = ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) -> if ( 2 || n , 0 , 1 ) = 1 )
81 47 peano2nnd 
 |-  ( ph -> ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) e. NN )
82 1xr 
 |-  1 e. RR*
83 82 a1i 
 |-  ( ph -> 1 e. RR* )
84 1 80 81 83 fvmptd2 
 |-  ( ph -> ( F ` ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) = 1 )
85 81 nnxrd 
 |-  ( ph -> ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) e. RR* )
86 81 nnred 
 |-  ( ph -> ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) e. RR )
87 56 ltp1d 
 |-  ( ph -> ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) < ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) )
88 2 56 86 70 87 lttrd 
 |-  ( ph -> K < ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) )
89 2 86 88 ltled 
 |-  ( ph -> K <_ ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) )
90 86 ltpnfd 
 |-  ( ph -> ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) < +oo )
91 52 54 85 89 90 elicod 
 |-  ( ph -> ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) e. ( K [,) +oo ) )
92 51 81 91 fnfvimad 
 |-  ( ph -> ( F ` ( ( 2 x. if ( 1 <_ K , ( |^ ` K ) , 1 ) ) + 1 ) ) e. ( F " ( K [,) +oo ) ) )
93 84 92 eqeltrrd 
 |-  ( ph -> 1 e. ( F " ( K [,) +oo ) ) )
94 75 93 prssd 
 |-  ( ph -> { 0 , 1 } C_ ( F " ( K [,) +oo ) ) )
95 15 94 eqssd 
 |-  ( ph -> ( F " ( K [,) +oo ) ) = { 0 , 1 } )