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	|- F/ j ph
	limsupubuz2.2	|- F/_ j F
	limsupubuz2.3	|- ( ph -> M e. ZZ )
	limsupubuz2.4	|- Z = ( ZZ>= ` M )
	limsupubuz2.5	|- ( ph -> F : Z --> RR* )
	limsupubuz2.6	|- ( ph -> ( limsup ` F ) =/= +oo )
Assertion	limsupubuz2	|- ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) < +oo )

Proof

Step	Hyp	Ref	Expression
1		limsupubuz2.1	|- F/ j ph
2		limsupubuz2.2	|- F/_ j F
3		limsupubuz2.3	|- ( ph -> M e. ZZ )
4		limsupubuz2.4	|- Z = ( ZZ>= ` M )
5		limsupubuz2.5	|- ( ph -> F : Z --> RR* )
6		limsupubuz2.6	|- ( ph -> ( limsup ` F ) =/= +oo )
7	4	uzssre2	|- Z C_ RR
8	7	a1i	|- ( ph -> Z C_ RR )
9	1 2 8 5 6	limsupub2	|- ( ph -> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) < +oo ) )
10	4	rexuzre	|- ( M e. ZZ -> ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) < +oo <-> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) < +oo ) ) )
11	3 10	syl	|- ( ph -> ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) < +oo <-> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) < +oo ) ) )
12	9 11	mpbird	|- ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) < +oo )