Metamath Proof Explorer

Theorem liminf10ex

Description: The inferior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis liminf10ex.1 ⊢ F = n ∈ ℕ ⟼ if 2 ∥ n 0 1
Assertion liminf10ex ⊢ lim inf ⁡ F = 0

Proof

Step Hyp Ref Expression
1 liminf10ex.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 ∈ ℝ ⟼ inf F k +∞ ℝ * < = k ∈ ℝ ⟼ inf F k +∞ ℝ * <
13 2 4 11 12 liminfval5 ⊢ ⊤ → lim inf ⁡ F = sup ran ⁡ k ∈ ℝ ⟼ inf F k +∞ ℝ * < ℝ * <
14 13 mptru ⊢ lim inf ⁡ F = sup ran ⁡ k ∈ ℝ ⟼ inf F k +∞ ℝ * < ℝ * <
15 id ⊢ k ∈ ℝ → k ∈ ℝ
16 1 15 limsup10exlem ⊢ k ∈ ℝ → F k +∞ = 0 1
17 16 infeq1d ⊢ k ∈ ℝ → inf F k +∞ ℝ * < = inf 0 1 ℝ * <
18 xrltso ⊢ < Or ℝ *
19 infpr ⊢ < Or ℝ * ∧ 0 ∈ ℝ * ∧ 1 ∈ ℝ * → inf 0 1 ℝ * < = if 0 < 1 0 1
20 18 5 7 19 mp3an ⊢ inf 0 1 ℝ * < = if 0 < 1 0 1
21 0lt1 ⊢ 0 < 1
22 21 iftruei ⊢ if 0 < 1 0 1 = 0
23 20 22 eqtri ⊢ inf 0 1 ℝ * < = 0
24 17 23 eqtrdi ⊢ k ∈ ℝ → inf F k +∞ ℝ * < = 0
25 24 mpteq2ia ⊢ k ∈ ℝ ⟼ inf F k +∞ ℝ * < = k ∈ ℝ ⟼ 0
26 25 rneqi ⊢ ran ⁡ k ∈ ℝ ⟼ inf F k +∞ ℝ * < = ran ⁡ k ∈ ℝ ⟼ 0
27 eqid ⊢ k ∈ ℝ ⟼ 0 = k ∈ ℝ ⟼ 0
28 ren0 ⊢ ℝ ≠ ∅
29 28 a1i ⊢ ⊤ → ℝ ≠ ∅
30 27 29 rnmptc ⊢ ⊤ → ran ⁡ k ∈ ℝ ⟼ 0 = 0
31 30 mptru ⊢ ran ⁡ k ∈ ℝ ⟼ 0 = 0
32 26 31 eqtri ⊢ ran ⁡ k ∈ ℝ ⟼ inf F k +∞ ℝ * < = 0
33 32 supeq1i ⊢ sup ran ⁡ k ∈ ℝ ⟼ inf F k +∞ ℝ * < ℝ * < = sup 0 ℝ * <
34 supsn ⊢ < Or ℝ * ∧ 0 ∈ ℝ * → sup 0 ℝ * < = 0
35 18 5 34 mp2an ⊢ sup 0 ℝ * < = 0
36 14 33 35 3eqtri ⊢ lim inf ⁡ F = 0