This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsuplesup

Description: An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypotheses	limsuplesup.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
		limsuplesup.2	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
	Assertion	limsuplesup	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ sup ( ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		limsuplesup.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		limsuplesup.2	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
3		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
4	3	limsupval	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
5	1 4	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
6		nfv	⊢ Ⅎ 𝑘 𝜑
7		inss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) ⊆ ℝ^*
8	7	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) ⊆ ℝ^* )
9	8	supxrcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ ℝ^* )
10		inss2	⊢ ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) ⊆ ℝ^*
11	10	a1i	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) ⊆ ℝ^* )
12	11	supxrcld	⊢ ( 𝜑 → sup ( ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ ℝ^* )
13		oveq1	⊢ ( 𝑘 = 𝐾 → ( 𝑘 [,) +∞ ) = ( 𝐾 [,) +∞ ) )
14	13	imaeq2d	⊢ ( 𝑘 = 𝐾 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝐾 [,) +∞ ) ) )
15	14	ineq1d	⊢ ( 𝑘 = 𝐾 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) )
16	15	supeq1d	⊢ ( 𝑘 = 𝐾 → sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) = sup ( ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
17	6 9 2 12 16	infxrlbrnmpt2	⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
18	5 17	eqbrtrd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ sup ( ( ( 𝐹 “ ( 𝐾 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )