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 = inf ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < ℝ * <
14 13 mptru ⊢ lim sup ⁡ F = inf 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 22 23 lenlti ⊢ 0 ≤ 1 ↔ ¬ 1 < 0
25 21 24 mpbi ⊢ ¬ 1 < 0
26 25 iffalsei ⊢ if 1 < 0 0 1 = 1
27 20 26 eqtri ⊢ sup 0 1 ℝ * < = 1
28 17 27 eqtrdi ⊢ k ∈ ℝ → sup F k +∞ ℝ * < = 1
29 28 mpteq2ia ⊢ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = k ∈ ℝ ⟼ 1
30 29 rneqi ⊢ ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = ran ⁡ k ∈ ℝ ⟼ 1
31 eqid ⊢ k ∈ ℝ ⟼ 1 = k ∈ ℝ ⟼ 1
32 ren0 ⊢ ℝ ≠ ∅
33 32 a1i ⊢ ⊤ → ℝ ≠ ∅
34 31 33 rnmptc ⊢ ⊤ → ran ⁡ k ∈ ℝ ⟼ 1 = 1
35 34 mptru ⊢ ran ⁡ k ∈ ℝ ⟼ 1 = 1
36 30 35 eqtri ⊢ ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < = 1
37 36 infeq1i ⊢ inf ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ℝ * < ℝ * < = inf 1 ℝ * <
38 infsn ⊢ < Or ℝ * ∧ 1 ∈ ℝ * → inf 1 ℝ * < = 1
39 18 7 38 mp2an ⊢ inf 1 ℝ * < = 1
40 14 37 39 3eqtri ⊢ lim sup ⁡ F = 1