Metamath Proof Explorer


Theorem limsupgre

Description: If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses limsupval.1
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
limsupgre.z
|- Z = ( ZZ>= ` M )
Assertion limsupgre
|- ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) -> G : RR --> RR )

Proof

Step Hyp Ref Expression
1 limsupval.1
 |-  G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 limsupgre.z
 |-  Z = ( ZZ>= ` M )
3 xrltso
 |-  < Or RR*
4 3 supex
 |-  sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
5 4 a1i
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ k e. RR ) -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V )
6 1 a1i
 |-  ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) -> G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
7 1 limsupgval
 |-  ( a e. RR -> ( G ` a ) = sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) )
8 7 adantl
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( G ` a ) = sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) )
9 simpl3
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( limsup ` F ) < +oo )
10 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
11 2 10 eqsstri
 |-  Z C_ ZZ
12 zssre
 |-  ZZ C_ RR
13 11 12 sstri
 |-  Z C_ RR
14 13 a1i
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> Z C_ RR )
15 simpl2
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> F : Z --> RR )
16 ressxr
 |-  RR C_ RR*
17 fss
 |-  ( ( F : Z --> RR /\ RR C_ RR* ) -> F : Z --> RR* )
18 15 16 17 sylancl
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> F : Z --> RR* )
19 pnfxr
 |-  +oo e. RR*
20 19 a1i
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> +oo e. RR* )
21 1 limsuplt
 |-  ( ( Z C_ RR /\ F : Z --> RR* /\ +oo e. RR* ) -> ( ( limsup ` F ) < +oo <-> E. n e. RR ( G ` n ) < +oo ) )
22 14 18 20 21 syl3anc
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( limsup ` F ) < +oo <-> E. n e. RR ( G ` n ) < +oo ) )
23 9 22 mpbid
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> E. n e. RR ( G ` n ) < +oo )
24 fzfi
 |-  ( M ... ( |_ ` n ) ) e. Fin
25 15 adantr
 |-  ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) -> F : Z --> RR )
26 elfzuz
 |-  ( m e. ( M ... ( |_ ` n ) ) -> m e. ( ZZ>= ` M ) )
27 26 2 eleqtrrdi
 |-  ( m e. ( M ... ( |_ ` n ) ) -> m e. Z )
28 ffvelrn
 |-  ( ( F : Z --> RR /\ m e. Z ) -> ( F ` m ) e. RR )
29 25 27 28 syl2an
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ m e. ( M ... ( |_ ` n ) ) ) -> ( F ` m ) e. RR )
30 29 ralrimiva
 |-  ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) -> A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) e. RR )
31 fimaxre3
 |-  ( ( ( M ... ( |_ ` n ) ) e. Fin /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) e. RR ) -> E. r e. RR A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r )
32 24 30 31 sylancr
 |-  ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) -> E. r e. RR A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r )
33 simpr
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> a e. RR )
34 33 ad2antrr
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> a e. RR )
35 1 limsupgf
 |-  G : RR --> RR*
36 35 ffvelrni
 |-  ( a e. RR -> ( G ` a ) e. RR* )
37 34 36 syl
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( G ` a ) e. RR* )
38 simprl
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> r e. RR )
39 16 38 sselid
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> r e. RR* )
40 simprl
 |-  ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) -> n e. RR )
41 40 adantr
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> n e. RR )
42 35 ffvelrni
 |-  ( n e. RR -> ( G ` n ) e. RR* )
43 41 42 syl
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( G ` n ) e. RR* )
44 39 43 ifcld
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> if ( ( G ` n ) <_ r , r , ( G ` n ) ) e. RR* )
45 19 a1i
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> +oo e. RR* )
46 40 ad2antrr
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> n e. RR )
47 13 a1i
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> Z C_ RR )
48 47 sselda
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> i e. RR )
49 43 xrleidd
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( G ` n ) <_ ( G ` n ) )
50 18 ad2antrr
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> F : Z --> RR* )
51 1 limsupgle
 |-  ( ( ( Z C_ RR /\ F : Z --> RR* ) /\ n e. RR /\ ( G ` n ) e. RR* ) -> ( ( G ` n ) <_ ( G ` n ) <-> A. i e. Z ( n <_ i -> ( F ` i ) <_ ( G ` n ) ) ) )
52 47 50 41 43 51 syl211anc
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( ( G ` n ) <_ ( G ` n ) <-> A. i e. Z ( n <_ i -> ( F ` i ) <_ ( G ` n ) ) ) )
53 49 52 mpbid
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> A. i e. Z ( n <_ i -> ( F ` i ) <_ ( G ` n ) ) )
54 53 r19.21bi
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( n <_ i -> ( F ` i ) <_ ( G ` n ) ) )
55 54 imp
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ n <_ i ) -> ( F ` i ) <_ ( G ` n ) )
56 46 42 syl
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( G ` n ) e. RR* )
57 39 adantr
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> r e. RR* )
58 xrmax1
 |-  ( ( ( G ` n ) e. RR* /\ r e. RR* ) -> ( G ` n ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
59 56 57 58 syl2anc
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( G ` n ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
60 50 ffvelrnda
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( F ` i ) e. RR* )
61 44 adantr
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> if ( ( G ` n ) <_ r , r , ( G ` n ) ) e. RR* )
62 xrletr
 |-  ( ( ( F ` i ) e. RR* /\ ( G ` n ) e. RR* /\ if ( ( G ` n ) <_ r , r , ( G ` n ) ) e. RR* ) -> ( ( ( F ` i ) <_ ( G ` n ) /\ ( G ` n ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
63 60 56 61 62 syl3anc
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( ( ( F ` i ) <_ ( G ` n ) /\ ( G ` n ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
64 59 63 mpan2d
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( ( F ` i ) <_ ( G ` n ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
65 64 adantr
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ n <_ i ) -> ( ( F ` i ) <_ ( G ` n ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
66 55 65 mpd
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ n <_ i ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
67 fveq2
 |-  ( m = i -> ( F ` m ) = ( F ` i ) )
68 67 breq1d
 |-  ( m = i -> ( ( F ` m ) <_ r <-> ( F ` i ) <_ r ) )
69 simprr
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r )
70 69 ad2antrr
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ i <_ n ) -> A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r )
71 simpr
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> i e. Z )
72 71 2 eleqtrdi
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> i e. ( ZZ>= ` M ) )
73 41 flcld
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( |_ ` n ) e. ZZ )
74 73 adantr
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( |_ ` n ) e. ZZ )
75 elfz5
 |-  ( ( i e. ( ZZ>= ` M ) /\ ( |_ ` n ) e. ZZ ) -> ( i e. ( M ... ( |_ ` n ) ) <-> i <_ ( |_ ` n ) ) )
76 72 74 75 syl2anc
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( i e. ( M ... ( |_ ` n ) ) <-> i <_ ( |_ ` n ) ) )
77 11 71 sselid
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> i e. ZZ )
78 flge
 |-  ( ( n e. RR /\ i e. ZZ ) -> ( i <_ n <-> i <_ ( |_ ` n ) ) )
79 46 77 78 syl2anc
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( i <_ n <-> i <_ ( |_ ` n ) ) )
80 76 79 bitr4d
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( i e. ( M ... ( |_ ` n ) ) <-> i <_ n ) )
81 80 biimpar
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ i <_ n ) -> i e. ( M ... ( |_ ` n ) ) )
82 68 70 81 rspcdva
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ i <_ n ) -> ( F ` i ) <_ r )
83 xrmax2
 |-  ( ( ( G ` n ) e. RR* /\ r e. RR* ) -> r <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
84 43 39 83 syl2anc
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> r <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
85 84 adantr
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> r <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
86 xrletr
 |-  ( ( ( F ` i ) e. RR* /\ r e. RR* /\ if ( ( G ` n ) <_ r , r , ( G ` n ) ) e. RR* ) -> ( ( ( F ` i ) <_ r /\ r <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
87 60 57 61 86 syl3anc
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( ( ( F ` i ) <_ r /\ r <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
88 85 87 mpan2d
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( ( F ` i ) <_ r -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
89 88 adantr
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ i <_ n ) -> ( ( F ` i ) <_ r -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
90 82 89 mpd
 |-  ( ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) /\ i <_ n ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
91 46 48 66 90 lecasei
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
92 91 a1d
 |-  ( ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) /\ i e. Z ) -> ( a <_ i -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
93 92 ralrimiva
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> A. i e. Z ( a <_ i -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) )
94 1 limsupgle
 |-  ( ( ( Z C_ RR /\ F : Z --> RR* ) /\ a e. RR /\ if ( ( G ` n ) <_ r , r , ( G ` n ) ) e. RR* ) -> ( ( G ` a ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) <-> A. i e. Z ( a <_ i -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) ) )
95 47 50 34 44 94 syl211anc
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( ( G ` a ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) <-> A. i e. Z ( a <_ i -> ( F ` i ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) ) ) )
96 93 95 mpbird
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( G ` a ) <_ if ( ( G ` n ) <_ r , r , ( G ` n ) ) )
97 38 ltpnfd
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> r < +oo )
98 simplrr
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( G ` n ) < +oo )
99 breq1
 |-  ( r = if ( ( G ` n ) <_ r , r , ( G ` n ) ) -> ( r < +oo <-> if ( ( G ` n ) <_ r , r , ( G ` n ) ) < +oo ) )
100 breq1
 |-  ( ( G ` n ) = if ( ( G ` n ) <_ r , r , ( G ` n ) ) -> ( ( G ` n ) < +oo <-> if ( ( G ` n ) <_ r , r , ( G ` n ) ) < +oo ) )
101 99 100 ifboth
 |-  ( ( r < +oo /\ ( G ` n ) < +oo ) -> if ( ( G ` n ) <_ r , r , ( G ` n ) ) < +oo )
102 97 98 101 syl2anc
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> if ( ( G ` n ) <_ r , r , ( G ` n ) ) < +oo )
103 37 44 45 96 102 xrlelttrd
 |-  ( ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) /\ ( r e. RR /\ A. m e. ( M ... ( |_ ` n ) ) ( F ` m ) <_ r ) ) -> ( G ` a ) < +oo )
104 32 103 rexlimddv
 |-  ( ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) /\ ( n e. RR /\ ( G ` n ) < +oo ) ) -> ( G ` a ) < +oo )
105 23 104 rexlimddv
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( G ` a ) < +oo )
106 8 105 eqbrtrrd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) < +oo )
107 imassrn
 |-  ( F " ( a [,) +oo ) ) C_ ran F
108 15 frnd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ran F C_ RR )
109 107 108 sstrid
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( F " ( a [,) +oo ) ) C_ RR )
110 109 16 sstrdi
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( F " ( a [,) +oo ) ) C_ RR* )
111 df-ss
 |-  ( ( F " ( a [,) +oo ) ) C_ RR* <-> ( ( F " ( a [,) +oo ) ) i^i RR* ) = ( F " ( a [,) +oo ) ) )
112 110 111 sylib
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( F " ( a [,) +oo ) ) i^i RR* ) = ( F " ( a [,) +oo ) ) )
113 112 109 eqsstrd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( F " ( a [,) +oo ) ) i^i RR* ) C_ RR )
114 simpl1
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> M e. ZZ )
115 flcl
 |-  ( a e. RR -> ( |_ ` a ) e. ZZ )
116 115 adantl
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( |_ ` a ) e. ZZ )
117 116 peano2zd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( |_ ` a ) + 1 ) e. ZZ )
118 117 114 ifcld
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ZZ )
119 114 zred
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> M e. RR )
120 117 zred
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( |_ ` a ) + 1 ) e. RR )
121 max1
 |-  ( ( M e. RR /\ ( ( |_ ` a ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) )
122 119 120 121 syl2anc
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> M <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) )
123 eluz2
 |-  ( if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ZZ /\ M <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) ) )
124 114 118 122 123 syl3anbrc
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ( ZZ>= ` M ) )
125 124 2 eleqtrrdi
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. Z )
126 15 fdmd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> dom F = Z )
127 125 126 eleqtrrd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. dom F )
128 118 zred
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. RR )
129 fllep1
 |-  ( a e. RR -> a <_ ( ( |_ ` a ) + 1 ) )
130 129 adantl
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> a <_ ( ( |_ ` a ) + 1 ) )
131 max2
 |-  ( ( M e. RR /\ ( ( |_ ` a ) + 1 ) e. RR ) -> ( ( |_ ` a ) + 1 ) <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) )
132 119 120 131 syl2anc
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( |_ ` a ) + 1 ) <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) )
133 33 120 128 130 132 letrd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> a <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) )
134 elicopnf
 |-  ( a e. RR -> ( if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ( a [,) +oo ) <-> ( if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. RR /\ a <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) ) ) )
135 134 adantl
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ( a [,) +oo ) <-> ( if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. RR /\ a <_ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) ) ) )
136 128 133 135 mpbir2and
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ( a [,) +oo ) )
137 inelcm
 |-  ( ( if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. dom F /\ if ( M <_ ( ( |_ ` a ) + 1 ) , ( ( |_ ` a ) + 1 ) , M ) e. ( a [,) +oo ) ) -> ( dom F i^i ( a [,) +oo ) ) =/= (/) )
138 127 136 137 syl2anc
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( dom F i^i ( a [,) +oo ) ) =/= (/) )
139 imadisj
 |-  ( ( F " ( a [,) +oo ) ) = (/) <-> ( dom F i^i ( a [,) +oo ) ) = (/) )
140 139 necon3bii
 |-  ( ( F " ( a [,) +oo ) ) =/= (/) <-> ( dom F i^i ( a [,) +oo ) ) =/= (/) )
141 138 140 sylibr
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( F " ( a [,) +oo ) ) =/= (/) )
142 112 141 eqnetrd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( ( F " ( a [,) +oo ) ) i^i RR* ) =/= (/) )
143 supxrre1
 |-  ( ( ( ( F " ( a [,) +oo ) ) i^i RR* ) C_ RR /\ ( ( F " ( a [,) +oo ) ) i^i RR* ) =/= (/) ) -> ( sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR <-> sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) < +oo ) )
144 113 142 143 syl2anc
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR <-> sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) < +oo ) )
145 106 144 mpbird
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> sup ( ( ( F " ( a [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR )
146 8 145 eqeltrd
 |-  ( ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) /\ a e. RR ) -> ( G ` a ) e. RR )
147 5 6 146 fmpt2d
 |-  ( ( M e. ZZ /\ F : Z --> RR /\ ( limsup ` F ) < +oo ) -> G : RR --> RR )