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

Metamath Proof Explorer

Theorem limsupubuzmpt

Description: If the limsup is not +oo , then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupubuzmpt.j 
|- F/ j ph
limsupubuzmpt.z 
|- Z = ( ZZ>= ` M )
limsupubuzmpt.b 
|- ( ( ph /\ j e. Z ) -> B e. RR )
limsupubuzmpt.n 
|- ( ph -> ( limsup ` ( j e. Z |-> B ) ) =/= +oo )
Assertion limsupubuzmpt 
|- ( ph -> E. x e. RR A. j e. Z B <_ x )

Proof

Step Hyp Ref Expression
1 limsupubuzmpt.j 
 |-  F/ j ph
2 limsupubuzmpt.z 
 |-  Z = ( ZZ>= ` M )
3 limsupubuzmpt.b 
 |-  ( ( ph /\ j e. Z ) -> B e. RR )
4 limsupubuzmpt.n 
 |-  ( ph -> ( limsup ` ( j e. Z |-> B ) ) =/= +oo )
5 nfmpt1 
 |-  F/_ j ( j e. Z |-> B )
6 eqid 
 |-  ( j e. Z |-> B ) = ( j e. Z |-> B )
7 1 3 6 fmptdf 
 |-  ( ph -> ( j e. Z |-> B ) : Z --> RR )
8 5 2 7 4 limsupubuz 
 |-  ( ph -> E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y )
9 6 a1i 
 |-  ( ph -> ( j e. Z |-> B ) = ( j e. Z |-> B ) )
10 9 3 fvmpt2d 
 |-  ( ( ph /\ j e. Z ) -> ( ( j e. Z |-> B ) ` j ) = B )
11 10 breq1d 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( j e. Z |-> B ) ` j ) <_ y <-> B <_ y ) )
12 1 11 ralbida 
 |-  ( ph -> ( A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> A. j e. Z B <_ y ) )
13 12 rexbidv 
 |-  ( ph -> ( E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> E. y e. RR A. j e. Z B <_ y ) )
14 8 13 mpbid 
 |-  ( ph -> E. y e. RR A. j e. Z B <_ y )
15 breq2 
 |-  ( y = x -> ( B <_ y <-> B <_ x ) )
16 15 ralbidv 
 |-  ( y = x -> ( A. j e. Z B <_ y <-> A. j e. Z B <_ x ) )
17 16 cbvrexvw 
 |-  ( E. y e. RR A. j e. Z B <_ y <-> E. x e. RR A. j e. Z B <_ x )
18 14 17 sylib 
 |-  ( ph -> E. x e. RR A. j e. Z B <_ x )