Metamath Proof Explorer

Theorem limsup10exlem

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

Ref Expression
Hypotheses limsup10exlem.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 1 ) )
limsup10exlem.2 ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
Assertion limsup10exlem ( 𝜑 → ( 𝐹 “ ( 𝐾 [,) +∞ ) ) = { 0 , 1 } )

Proof

Step Hyp Ref Expression
1 limsup10exlem.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 1 ) )
2 limsup10exlem.2 ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
3 c0ex ⊢ 0 ∈ V
4 3 prid1 ⊢ 0 ∈ { 0 , 1 }
5 1re ⊢ 1 ∈ ℝ
6 5 elexi ⊢ 1 ∈ V
7 6 prid2 ⊢ 1 ∈ { 0 , 1 }
8 4 7 ifcli ⊢ if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ { 0 , 1 }
9 8 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∩ ( 𝐾 [,) +∞ ) ) ) → if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ { 0 , 1 } )
10 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ℕ ∩ ( 𝐾 [,) +∞ ) ) if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ { 0 , 1 } )
11 nfv ⊢ Ⅎ 𝑛 𝜑
12 3 6 ifex ⊢ if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ V
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∩ ( 𝐾 [,) +∞ ) ) ) → if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ V )
14 11 13 1 imassmpt ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ⊆ { 0 , 1 } ↔ ∀ 𝑛 ∈ ( ℕ ∩ ( 𝐾 [,) +∞ ) ) if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ { 0 , 1 } ) )
15 10 14 mpbird ⊢ ( 𝜑 → ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ⊆ { 0 , 1 } )
16 2 ceilcld ⊢ ( 𝜑 → ( ⌈ ‘ 𝐾 ) ∈ ℤ )
17 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
18 16 17 ifcld ⊢ ( 𝜑 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℤ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 = ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℤ )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑛 = ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) → 𝑛 = ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) )
21 2teven ⊢ ( ( if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℤ ∧ 𝑛 = ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) → 2 ∥ 𝑛 )
22 19 20 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 = ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) → 2 ∥ 𝑛 )
23 22 iftrued ⊢ ( ( 𝜑 ∧ 𝑛 = ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) → if ( 2 ∥ 𝑛 , 0 , 1 ) = 0 )
24 2nn ⊢ 2 ∈ ℕ
25 24 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
26 eqid ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ 1 )
27 5 a1i ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 1 ∈ ℝ )
28 2 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 𝐾 ∈ ℝ )
29 16 zred ⊢ ( 𝜑 → ( ⌈ ‘ 𝐾 ) ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → ( ⌈ ‘ 𝐾 ) ∈ ℝ )
31 simpr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 1 ≤ 𝐾 )
32 2 ceilged ⊢ ( 𝜑 → 𝐾 ≤ ( ⌈ ‘ 𝐾 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 𝐾 ≤ ( ⌈ ‘ 𝐾 ) )
34 27 28 30 31 33 letrd ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 1 ≤ ( ⌈ ‘ 𝐾 ) )
35 iftrue ⊢ ( 1 ≤ 𝐾 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) = ( ⌈ ‘ 𝐾 ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) = ( ⌈ ‘ 𝐾 ) )
37 34 36 breqtrrd ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 1 ≤ if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
38 5 leidi ⊢ 1 ≤ 1
39 38 a1i ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 1 ≤ 1 )
40 iffalse ⊢ ( ¬ 1 ≤ 𝐾 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) = 1 )
41 40 adantl ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) = 1 )
42 39 41 breqtrrd ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 1 ≤ if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
43 37 42 pm2.61dan ⊢ ( 𝜑 → 1 ≤ if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
44 26 17 18 43 eluzd ⊢ ( 𝜑 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ( ℤ≥ ‘ 1 ) )
45 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
46 44 45 eleqtrrdi ⊢ ( 𝜑 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℕ )
47 25 46 nnmulcld ⊢ ( 𝜑 → ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ∈ ℕ )
48 3 a1i ⊢ ( 𝜑 → 0 ∈ V )
49 1 23 47 48 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) = 0 )
50 12 1 fnmpti ⊢ 𝐹 Fn ℕ
51 50 a1i ⊢ ( 𝜑 → 𝐹 Fn ℕ )
52 2 rexrd ⊢ ( 𝜑 → 𝐾 ∈ ℝ* )
53 pnfxr ⊢ +∞ ∈ ℝ*
54 53 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
55 47 nnxrd ⊢ ( 𝜑 → ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ∈ ℝ* )
56 47 nnred ⊢ ( 𝜑 → ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ∈ ℝ )
57 46 nnred ⊢ ( 𝜑 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℝ )
58 33 36 breqtrrd ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐾 ) → 𝐾 ≤ if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
59 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 𝐾 ∈ ℝ )
60 5 a1i ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 1 ∈ ℝ )
61 simpr ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → ¬ 1 ≤ 𝐾 )
62 59 60 61 nleltd ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 𝐾 < 1 )
63 59 60 62 ltled ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 𝐾 ≤ 1 )
64 41 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 1 = if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
65 63 64 breqtrd ⊢ ( ( 𝜑 ∧ ¬ 1 ≤ 𝐾 ) → 𝐾 ≤ if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
66 58 65 pm2.61dan ⊢ ( 𝜑 → 𝐾 ≤ if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) )
67 46 nnrpd ⊢ ( 𝜑 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℝ+ )
68 2timesgt ⊢ ( if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℝ+ → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) < ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) )
69 67 68 syl ⊢ ( 𝜑 → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) < ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) )
70 2 57 56 66 69 lelttrd ⊢ ( 𝜑 → 𝐾 < ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) )
71 2 56 70 ltled ⊢ ( 𝜑 → 𝐾 ≤ ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) )
72 56 ltpnfd ⊢ ( 𝜑 → ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) < +∞ )
73 52 54 55 71 72 elicod ⊢ ( 𝜑 → ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ∈ ( 𝐾 [,) +∞ ) )
74 51 47 73 fnfvimad ⊢ ( 𝜑 → ( 𝐹 ‘ ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) ) ∈ ( 𝐹 “ ( 𝐾 [,) +∞ ) ) )
75 49 74 eqeltrrd ⊢ ( 𝜑 → 0 ∈ ( 𝐹 “ ( 𝐾 [,) +∞ ) ) )
76 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) → if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℤ )
77 simpr ⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) → 𝑛 = ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) )
78 2tp1odd ⊢ ( ( if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ∈ ℤ ∧ 𝑛 = ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) → ¬ 2 ∥ 𝑛 )
79 76 77 78 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) → ¬ 2 ∥ 𝑛 )
80 79 iffalsed ⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) → if ( 2 ∥ 𝑛 , 0 , 1 ) = 1 )
81 47 peano2nnd ⊢ ( 𝜑 → ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ∈ ℕ )
82 1xr ⊢ 1 ∈ ℝ*
83 82 a1i ⊢ ( 𝜑 → 1 ∈ ℝ* )
84 1 80 81 83 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) = 1 )
85 81 nnxrd ⊢ ( 𝜑 → ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ∈ ℝ* )
86 81 nnred ⊢ ( 𝜑 → ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ∈ ℝ )
87 56 ltp1d ⊢ ( 𝜑 → ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) < ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) )
88 2 56 86 70 87 lttrd ⊢ ( 𝜑 → 𝐾 < ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) )
89 2 86 88 ltled ⊢ ( 𝜑 → 𝐾 ≤ ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) )
90 86 ltpnfd ⊢ ( 𝜑 → ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) < +∞ )
91 52 54 85 89 90 elicod ⊢ ( 𝜑 → ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ∈ ( 𝐾 [,) +∞ ) )
92 51 81 91 fnfvimad ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 2 · if ( 1 ≤ 𝐾 , ( ⌈ ‘ 𝐾 ) , 1 ) ) + 1 ) ) ∈ ( 𝐹 “ ( 𝐾 [,) +∞ ) ) )
93 84 92 eqeltrrd ⊢ ( 𝜑 → 1 ∈ ( 𝐹 “ ( 𝐾 [,) +∞ ) ) )
94 75 93 prssd ⊢ ( 𝜑 → { 0 , 1 } ⊆ ( 𝐹 “ ( 𝐾 [,) +∞ ) ) )
95 15 94 eqssd ⊢ ( 𝜑 → ( 𝐹 “ ( 𝐾 [,) +∞ ) ) = { 0 , 1 } )