Step |
Hyp |
Ref |
Expression |
1 |
|
climliminflimsup3.1 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
2 |
|
climliminflimsup3.2 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
|
climliminflimsup3.3 |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ ) |
4 |
1 2 3
|
climliminflimsup |
⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) ) ) |
5 |
3
|
frexr |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* ) |
6 |
1 2 5
|
liminfgelimsupuz |
⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ) |
7 |
6
|
anbi2d |
⊢ ( 𝜑 → ( ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ) ) |
8 |
4 7
|
bitrd |
⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ) ) |