Theorem limsupubuz2

Description: A sequence with values in the extended reals, and with limsup that is not +oo , is eventually less than +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	limsupubuz2.1	$$⊢Ⅎj\phi$$
	limsupubuz2.2	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupubuz2.3	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupubuz2.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupubuz2.5	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
	limsupubuz2.6	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }$$
Assertion	limsupubuz2	$$⊢\phi \to \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)<\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		limsupubuz2.1	$$⊢Ⅎj\phi$$
2		limsupubuz2.2	$$⊢\underset{\_}{Ⅎ}jF$$
3		limsupubuz2.3	$$⊢\phi \to M\in \mathbb{Z}$$
4		limsupubuz2.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		limsupubuz2.5	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
6		limsupubuz2.6	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }$$
7	4	uzssre2	$$⊢Z\subseteq ℝ$$
8	7	a1i	$$⊢\phi \to Z\subseteq ℝ$$
9	1 2 8 5 6	limsupub2	$$⊢\phi \to \exists k\in ℝ\forall j\in Z\left(k\le j\to F\left(j\right)<\mathrm{+\infty }\right)$$
10	4	rexuzre	$$⊢M\in \mathbb{Z}\to \left(\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)<\mathrm{+\infty }\leftrightarrow \exists k\in ℝ\forall j\in Z\left(k\le j\to F\left(j\right)<\mathrm{+\infty }\right)\right)$$
11	3 10	syl	$$⊢\phi \to \left(\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)<\mathrm{+\infty }\leftrightarrow \exists k\in ℝ\forall j\in Z\left(k\le j\to F\left(j\right)<\mathrm{+\infty }\right)\right)$$
12	9 11	mpbird	$$⊢\phi \to \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)<\mathrm{+\infty }$$