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 𝐹 = ( 𝑛 ∈ ℕ ↦ 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