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 |