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 ∈ ℕ ⟼ if 2 ∥ n 0 1
limsup10exlem.2 ⊢ φ → K ∈ ℝ
Assertion limsup10exlem ⊢ φ → F K +∞ = 0 1

Proof

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