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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 1 ) )
Assertion	liminf10ex	⊢ ( lim inf ‘ 𝐹 ) = 0

Proof

Step	Hyp	Ref	Expression
1		liminf10ex.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 1 ) )
2		nftru	⊢ Ⅎ 𝑘 ⊤
3		nnex	⊢ ℕ ∈ V
4	3	a1i	⊢ ( ⊤ → ℕ ∈ V )
5		0xr	⊢ 0 ∈ ℝ*
6	5	a1i	⊢ ( 𝑛 ∈ ℕ → 0 ∈ ℝ* )
7		1xr	⊢ 1 ∈ ℝ*
8	7	a1i	⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ* )
9	6 8	ifcld	⊢ ( 𝑛 ∈ ℕ → if ( 2 ∥ 𝑛 , 0 , 1 ) ∈ ℝ* )
10	1 9	fmpti	⊢ 𝐹 : ℕ ⟶ ℝ*
11	10	a1i	⊢ ( ⊤ → 𝐹 : ℕ ⟶ ℝ* )
12		eqid	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
13	2 4 11 12	liminfval5	⊢ ( ⊤ → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) )
14	13	mptru	⊢ ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < )
15		id	⊢ ( 𝑘 ∈ ℝ → 𝑘 ∈ ℝ )
16	1 15	limsup10exlem	⊢ ( 𝑘 ∈ ℝ → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = { 0 , 1 } )
17	16	infeq1d	⊢ ( 𝑘 ∈ ℝ → inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) = 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	⊢ ( 𝑘 ∈ ℝ → inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) = 0 )
25	24	mpteq2ia	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ 0 )
26	25	rneqi	⊢ ran ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ 0 )
27		eqid	⊢ ( 𝑘 ∈ ℝ ↦ 0 ) = ( 𝑘 ∈ ℝ ↦ 0 )
28		ren0	⊢ ℝ ≠ ∅
29	28	a1i	⊢ ( ⊤ → ℝ ≠ ∅ )
30	27 29	rnmptc	⊢ ( ⊤ → ran ( 𝑘 ∈ ℝ ↦ 0 ) = { 0 } )
31	30	mptru	⊢ ran ( 𝑘 ∈ ℝ ↦ 0 ) = { 0 }
32	26 31	eqtri	⊢ ran ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = { 0 }
33	32	supeq1i	⊢ sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
34		supsn	⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
35	18 5 34	mp2an	⊢ sup ( { 0 } , ℝ* , < ) = 0
36	14 33 35	3eqtri	⊢ ( lim inf ‘ 𝐹 ) = 0