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 sseldi 
 |-  ( ( ( ( ( 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 sseldi 
 |-  ( ( ( ( ( ( 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 )