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

Proof

Step	Hyp	Ref	Expression
1		limsup10ex.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	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) )
13	2 4 11 12	limsupval3	⊢ ( ⊤ → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) )
14	13	mptru	⊢ ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < )
15		id	⊢ ( 𝑘 ∈ ℝ → 𝑘 ∈ ℝ )
16	1 15	limsup10exlem	⊢ ( 𝑘 ∈ ℝ → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = { 0 , 1 } )
17	16	supeq1d	⊢ ( 𝑘 ∈ ℝ → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) = 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	⊢ ( 𝑘 ∈ ℝ → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) = 1 )
29	28	mpteq2ia	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ 1 )
30	29	rneqi	⊢ ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ 1 )
31		eqid	⊢ ( 𝑘 ∈ ℝ ↦ 1 ) = ( 𝑘 ∈ ℝ ↦ 1 )
32		ren0	⊢ ℝ ≠ ∅
33	32	a1i	⊢ ( ⊤ → ℝ ≠ ∅ )
34	31 33	rnmptc	⊢ ( ⊤ → ran ( 𝑘 ∈ ℝ ↦ 1 ) = { 1 } )
35	34	mptru	⊢ ran ( 𝑘 ∈ ℝ ↦ 1 ) = { 1 }
36	30 35	eqtri	⊢ ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) = { 1 }
37	36	infeq1i	⊢ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( { 1 } , ℝ* , < )
38		infsn	⊢ ( ( < Or ℝ* ∧ 1 ∈ ℝ* ) → inf ( { 1 } , ℝ* , < ) = 1 )
39	18 7 38	mp2an	⊢ inf ( { 1 } , ℝ* , < ) = 1
40	14 37 39	3eqtri	⊢ ( lim sup ‘ 𝐹 ) = 1