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 ∈ ℕ ⟼ if 2 ∥ n 0 1
Assertion limsup10ex ⊢ lim sup ⁡ F = 1

Proof

Step Hyp Ref Expression
1 limsup10ex.1 ⊢ F = n ∈ ℕ ⟼ if 2 ∥ n 0 1
2 nftru ⊢ Ⅎ k ⊤
3 nnex ⊢ ℕ ∈ V
4 3 a1i ⊢ ⊤ → ℕ ∈ V
5 0xr ⊢ 0 ∈ ℝ *
6 5 a1i ⊢ n ∈ ℕ → 0 ∈ ℝ *
7 1xr ⊢ 1 ∈ ℝ *
8 7 a1i ⊢ n ∈ ℕ → 1 ∈ ℝ *
9 6 8 ifcld ⊢ n ∈ ℕ → if 2 ∥ n 0 1 ∈ ℝ *
10 1 9 fmpti ⊢ F : ℕ ⟶ ℝ *
11 10 a1i ⊢ ⊤ → F : ℕ ⟶ ℝ *
12 eqid ⊢ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = k ∈ ℝ ⟼ sup F k +∞ ℝ * <
13 2 4 11 12 limsupval3 ⊢ ⊤ → lim sup ⁡ F = sup ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < ℝ * <
14 13 mptru ⊢ lim sup ⁡ F = sup ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < ℝ * <
15 id ⊢ k ∈ ℝ → k ∈ ℝ
16 1 15 limsup10exlem ⊢ k ∈ ℝ → F k +∞ = 0 1
17 16 supeq1d ⊢ k ∈ ℝ → sup F k +∞ ℝ * < = sup 0 1 ℝ * <
18 xrltso ⊢ < Or ℝ *
19 suppr ⊢ < Or ℝ * ∧ 0 ∈ ℝ * ∧ 1 ∈ ℝ * → sup 0 1 ℝ * < = if 1 < 0 0 1
20 18 5 7 19 mp3an ⊢ sup 0 1 ℝ * < = if 1 < 0 0 1
21 0le1 ⊢ 0 ≤ 1
22 0re ⊢ 0 ∈ ℝ
23 1re ⊢ 1 ∈ ℝ
24 lenlt ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ → 0 ≤ 1 ↔ ¬ 1 < 0
25 22 23 24 mp2an ⊢ 0 ≤ 1 ↔ ¬ 1 < 0
26 21 25 mpbi ⊢ ¬ 1 < 0
27 26 iffalsei ⊢ if 1 < 0 0 1 = 1
28 20 27 eqtri ⊢ sup 0 1 ℝ * < = 1
29 28 a1i ⊢ k ∈ ℝ → sup 0 1 ℝ * < = 1
30 17 29 eqtrd ⊢ k ∈ ℝ → sup F k +∞ ℝ * < = 1
31 30 mpteq2ia ⊢ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = k ∈ ℝ ⟼ 1
32 31 rneqi ⊢ ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = ran ⁡ k ∈ ℝ ⟼ 1
33 eqid ⊢ k ∈ ℝ ⟼ 1 = k ∈ ℝ ⟼ 1
34 23 elexi ⊢ 1 ∈ V
35 34 a1i ⊢ ⊤ ∧ k ∈ ℝ → 1 ∈ V
36 ren0 ⊢ ℝ ≠ ∅
37 36 a1i ⊢ ⊤ → ℝ ≠ ∅
38 33 35 37 rnmptc ⊢ ⊤ → ran ⁡ k ∈ ℝ ⟼ 1 = 1
39 38 mptru ⊢ ran ⁡ k ∈ ℝ ⟼ 1 = 1
40 32 39 eqtri ⊢ ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = 1
41 40 infeq1i ⊢ sup ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < ℝ * < = sup 1 ℝ * <
42 infsn ⊢ < Or ℝ * ∧ 1 ∈ ℝ * → sup 1 ℝ * < = 1
43 18 7 42 mp2an ⊢ sup 1 ℝ * < = 1
44 14 41 43 3eqtri ⊢ lim sup ⁡ F = 1