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

Metamath Proof Explorer

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 )