MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limsupgreOLD Structured version   Visualization version   Unicode version

Theorem limsupgreOLD 13543
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.) Obsolete version of limsupgre 13542 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
limsupval.1  |-  G  =  ( k  e.  RR  |->  sup ( ( ( F
" ( k [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  ) )
limsupgre.z  |-  Z  =  ( ZZ>= `  M )
Assertion
Ref Expression
limsupgreOLD  |-  ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  ->  G : RR --> RR )
Distinct variable groups:    k, F    k, M    k, Z
Allowed substitution hint:    G( k)

Proof of Theorem limsupgreOLD
Dummy variables  a 
i  m  n  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrltso 11440 . . . 4  |-  <  Or  RR*
21supex 7977 . . 3  |-  sup (
( ( F "
( k [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  )  e.  _V
32a1i 11 . 2  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  k  e.  RR )  ->  sup ( ( ( F
" ( k [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  )  e.  _V )
4 limsupval.1 . . 3  |-  G  =  ( k  e.  RR  |->  sup ( ( ( F
" ( k [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  ) )
54a1i 11 . 2  |-  ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  ->  G  =  ( k  e.  RR  |->  sup ( ( ( F " ( k [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) )
64limsupgval 13534 . . . 4  |-  ( a  e.  RR  ->  ( G `  a )  =  sup ( ( ( F " ( a [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  ) )
76adantl 468 . . 3  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( G `  a )  =  sup ( ( ( F " ( a [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  ) )
8 simpl3 1013 . . . . . . 7  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( limsup `
 F )  < +oo )
9 limsupgre.z . . . . . . . . . . 11  |-  Z  =  ( ZZ>= `  M )
10 uzssz 11178 . . . . . . . . . . 11  |-  ( ZZ>= `  M )  C_  ZZ
119, 10eqsstri 3462 . . . . . . . . . 10  |-  Z  C_  ZZ
12 zssre 10944 . . . . . . . . . 10  |-  ZZ  C_  RR
1311, 12sstri 3441 . . . . . . . . 9  |-  Z  C_  RR
1413a1i 11 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  Z  C_  RR )
15 simpl2 1012 . . . . . . . . 9  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  F : Z --> RR )
16 ressxr 9684 . . . . . . . . 9  |-  RR  C_  RR*
17 fss 5737 . . . . . . . . 9  |-  ( ( F : Z --> RR  /\  RR  C_  RR* )  ->  F : Z --> RR* )
1815, 16, 17sylancl 668 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  F : Z --> RR* )
19 pnfxr 11412 . . . . . . . . 9  |- +oo  e.  RR*
2019a1i 11 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  -> +oo  e.  RR* )
214limsupltOLD 13539 . . . . . . . 8  |-  ( ( Z  C_  RR  /\  F : Z --> RR*  /\ +oo  e.  RR* )  ->  ( ( limsup `
 F )  < +oo 
<->  E. n  e.  RR  ( G `  n )  < +oo ) )
2214, 18, 20, 21syl3anc 1268 . . . . . . 7  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( limsup `  F )  < +oo  <->  E. n  e.  RR  ( G `  n )  < +oo ) )
238, 22mpbid 214 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  E. n  e.  RR  ( G `  n )  < +oo )
24 fzfi 12185 . . . . . . . 8  |-  ( M ... ( |_ `  n ) )  e. 
Fin
2515adantr 467 . . . . . . . . . 10  |-  ( ( ( ( M  e.  ZZ  /\  F : Z
--> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  /\  ( n  e.  RR  /\  ( G `
 n )  < +oo ) )  ->  F : Z --> RR )
26 elfzuz 11796 . . . . . . . . . . 11  |-  ( m  e.  ( M ... ( |_ `  n ) )  ->  m  e.  ( ZZ>= `  M )
)
2726, 9syl6eleqr 2540 . . . . . . . . . 10  |-  ( m  e.  ( M ... ( |_ `  n ) )  ->  m  e.  Z )
28 ffvelrn 6020 . . . . . . . . . 10  |-  ( ( F : Z --> RR  /\  m  e.  Z )  ->  ( F `  m
)  e.  RR )
2925, 27, 28syl2an 480 . . . . . . . . 9  |-  ( ( ( ( ( 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 )
3029ralrimiva 2802 . . . . . . . 8  |-  ( ( ( ( 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 10553 . . . . . . . 8  |-  ( ( ( 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 )
3224, 30, 31sylancr 669 . . . . . . 7  |-  ( ( ( ( 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 463 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  a  e.  RR )
3433ad2antrr 732 . . . . . . . . 9  |-  ( ( ( ( ( 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 )
354limsupgf 13533 . . . . . . . . . 10  |-  G : RR
--> RR*
3635ffvelrni 6021 . . . . . . . . 9  |-  ( a  e.  RR  ->  ( G `  a )  e.  RR* )
3734, 36syl 17 . . . . . . . 8  |-  ( ( ( ( ( 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 764 . . . . . . . . . 10  |-  ( ( ( ( ( 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 )
3916, 38sseldi 3430 . . . . . . . . 9  |-  ( ( ( ( ( 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 764 . . . . . . . . . . 11  |-  ( ( ( ( M  e.  ZZ  /\  F : Z
--> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  /\  ( n  e.  RR  /\  ( G `
 n )  < +oo ) )  ->  n  e.  RR )
4140adantr 467 . . . . . . . . . 10  |-  ( ( ( ( ( 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 )
4235ffvelrni 6021 . . . . . . . . . 10  |-  ( n  e.  RR  ->  ( G `  n )  e.  RR* )
4341, 42syl 17 . . . . . . . . 9  |-  ( ( ( ( ( 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* )
4439, 43ifcld 3924 . . . . . . . 8  |-  ( ( ( ( ( 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* )
4519a1i 11 . . . . . . . 8  |-  ( ( ( ( ( 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* )
4640ad2antrr 732 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 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 )
4713a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
4847sselda 3432 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 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 xrleid 11449 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  n )  e.  RR*  ->  ( G `
 n )  <_ 
( G `  n
) )
5043, 49syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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 )
)
5118ad2antrr 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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* )
524limsupgle 13535 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) )
5347, 51, 41, 43, 52syl211anc 1274 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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 ) ) ) )
5450, 53mpbid 214 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 )
) )
5554r19.21bi 2757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 ) ) )
5655imp 431 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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
) )
5746, 42syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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* )
5839adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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* )
59 xrmax1 11470 . . . . . . . . . . . . . . . 16  |-  ( ( ( G `  n
)  e.  RR*  /\  r  e.  RR* )  ->  ( G `  n )  <_  if ( ( G `
 n )  <_ 
r ,  r ,  ( G `  n
) ) )
6057, 58, 59syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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
) ) )
6151ffvelrnda 6022 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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* )
6244adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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* )
63 xrletr 11455 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
6461, 57, 62, 63syl3anc 1268 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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 ) ) ) )
6560, 64mpan2d 680 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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
) ) ) )
6665adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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
) ) ) )
6756, 66mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
) ) )
68 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( 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 )
6968, 9syl6eleq 2539 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( 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 )
)
7041flcld 12034 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 )
7170adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( 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 )
72 elfz5 11792 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( ZZ>= `  M )  /\  ( |_ `  n )  e.  ZZ )  ->  (
i  e.  ( M ... ( |_ `  n ) )  <->  i  <_  ( |_ `  n ) ) )
7369, 71, 72syl2anc 667 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 ) ) )
7411, 68sseldi 3430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( 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 )
75 flge 12041 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  RR  /\  i  e.  ZZ )  ->  ( i  <_  n  <->  i  <_  ( |_ `  n ) ) )
7646, 74, 75syl2anc 667 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 ) ) )
7773, 76bitr4d 260 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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 ) )
7877biimpar 488 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 ) ) )
79 simprr 766 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 )
8079ad2antrr 732 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 )
81 fveq2 5865 . . . . . . . . . . . . . . . 16  |-  ( m  =  i  ->  ( F `  m )  =  ( F `  i ) )
8281breq1d 4412 . . . . . . . . . . . . . . 15  |-  ( m  =  i  ->  (
( F `  m
)  <_  r  <->  ( F `  i )  <_  r
) )
8382rspcv 3146 . . . . . . . . . . . . . 14  |-  ( i  e.  ( M ... ( |_ `  n ) )  ->  ( A. m  e.  ( M ... ( |_ `  n
) ) ( F `
 m )  <_ 
r  ->  ( F `  i )  <_  r
) )
8478, 80, 83sylc 62 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 )
85 xrmax2 11471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( G `  n
)  e.  RR*  /\  r  e.  RR* )  ->  r  <_  if ( ( G `
 n )  <_ 
r ,  r ,  ( G `  n
) ) )
8643, 39, 85syl2anc 667 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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 ) ) )
8786adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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
) ) )
88 xrletr 11455 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
8961, 58, 62, 88syl3anc 1268 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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 ) ) ) )
9087, 89mpan2d 680 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 ) ) ) )
9190adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) ) ) )
9284, 91mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
) ) )
9346, 48, 67, 92lecasei 9740 . . . . . . . . . . 11  |-  ( ( ( ( ( ( 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
) ) )
9493a1d 26 . . . . . . . . . 10  |-  ( ( ( ( ( ( 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 ) ) ) )
9594ralrimiva 2802 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) ) ) )
964limsupgle 13535 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) )
9747, 51, 34, 44, 96syl211anc 1274 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) ) ) ) )
9895, 97mpbird 236 . . . . . . . 8  |-  ( ( ( ( ( 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 ) ) )
99 ltpnf 11422 . . . . . . . . . 10  |-  ( r  e.  RR  ->  r  < +oo )
10038, 99syl 17 . . . . . . . . 9  |-  ( ( ( ( ( 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 )
101 simplrr 771 . . . . . . . . 9  |-  ( ( ( ( ( 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 )
102 breq1 4405 . . . . . . . . . 10  |-  ( r  =  if ( ( G `  n )  <_  r ,  r ,  ( G `  n ) )  -> 
( r  < +oo  <->  if ( ( G `  n )  <_  r ,  r ,  ( G `  n ) )  < +oo )
)
103 breq1 4405 . . . . . . . . . 10  |-  ( ( G `  n )  =  if ( ( G `  n )  <_  r ,  r ,  ( G `  n ) )  -> 
( ( G `  n )  < +oo  <->  if ( ( G `  n )  <_  r ,  r ,  ( G `  n ) )  < +oo )
)
104102, 103ifboth 3917 . . . . . . . . 9  |-  ( ( r  < +oo  /\  ( G `  n )  < +oo )  ->  if ( ( G `  n )  <_  r ,  r ,  ( G `  n ) )  < +oo )
105100, 101, 104syl2anc 667 . . . . . . . 8  |-  ( ( ( ( ( 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 )
10637, 44, 45, 98, 105xrlelttrd 11457 . . . . . . 7  |-  ( ( ( ( ( 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 )
10732, 106rexlimddv 2883 . . . . . 6  |-  ( ( ( ( M  e.  ZZ  /\  F : Z
--> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  /\  ( n  e.  RR  /\  ( G `
 n )  < +oo ) )  ->  ( G `  a )  < +oo )
10823, 107rexlimddv 2883 . . . . 5  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( G `  a )  < +oo )
1097, 108eqbrtrrd 4425 . . . 4  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  sup ( ( ( F
" ( a [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  )  < +oo )
110 imassrn 5179 . . . . . . . . 9  |-  ( F
" ( a [,) +oo ) )  C_  ran  F
111 frn 5735 . . . . . . . . . 10  |-  ( F : Z --> RR  ->  ran 
F  C_  RR )
11215, 111syl 17 . . . . . . . . 9  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ran  F 
C_  RR )
113110, 112syl5ss 3443 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( F " ( a [,) +oo ) )  C_  RR )
114113, 16syl6ss 3444 . . . . . . 7  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( F " ( a [,) +oo ) )  C_  RR* )
115 df-ss 3418 . . . . . . 7  |-  ( ( F " ( a [,) +oo ) ) 
C_  RR*  <->  ( ( F
" ( a [,) +oo ) )  i^i  RR* )  =  ( F " ( a [,) +oo ) ) )
116114, 115sylib 200 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( F " (
a [,) +oo )
)  i^i  RR* )  =  ( F " (
a [,) +oo )
) )
117116, 113eqsstrd 3466 . . . . 5  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( F " (
a [,) +oo )
)  i^i  RR* )  C_  RR )
118 simpl1 1011 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  M  e.  ZZ )
119 flcl 12031 . . . . . . . . . . . . . 14  |-  ( a  e.  RR  ->  ( |_ `  a )  e.  ZZ )
120119adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( |_ `  a )  e.  ZZ )
121120peano2zd 11043 . . . . . . . . . . . 12  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( |_ `  a
)  +  1 )  e.  ZZ )
122121, 118ifcld 3924 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M )  e.  ZZ )
123118zred 11040 . . . . . . . . . . . 12  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  M  e.  RR )
124121zred 11040 . . . . . . . . . . . 12  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( |_ `  a
)  +  1 )  e.  RR )
125 max1 11480 . . . . . . . . . . . 12  |-  ( ( M  e.  RR  /\  ( ( |_ `  a )  +  1 )  e.  RR )  ->  M  <_  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M ) )
126123, 124, 125syl2anc 667 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  M  <_  if ( M  <_ 
( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M ) )
127 eluz2 11165 . . . . . . . . . . 11  |-  ( 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
) ) )
128118, 122, 126, 127syl3anbrc 1192 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M )  e.  ( ZZ>= `  M
) )
129128, 9syl6eleqr 2540 . . . . . . . . 9  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M )  e.  Z )
130 fdm 5733 . . . . . . . . . 10  |-  ( F : Z --> RR  ->  dom 
F  =  Z )
13115, 130syl 17 . . . . . . . . 9  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  dom  F  =  Z )
132129, 131eleqtrrd 2532 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M )  e.  dom  F )
133122zred 11040 . . . . . . . . 9  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M )  e.  RR )
134 fllep1 12037 . . . . . . . . . . 11  |-  ( a  e.  RR  ->  a  <_  ( ( |_ `  a )  +  1 ) )
135134adantl 468 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  a  <_  ( ( |_ `  a )  +  1 ) )
136 max2 11482 . . . . . . . . . . 11  |-  ( ( M  e.  RR  /\  ( ( |_ `  a )  +  1 )  e.  RR )  ->  ( ( |_
`  a )  +  1 )  <_  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M ) )
137123, 124, 136syl2anc 667 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( |_ `  a
)  +  1 )  <_  if ( M  <_  ( ( |_
`  a )  +  1 ) ,  ( ( |_ `  a
)  +  1 ) ,  M ) )
13833, 124, 133, 135, 137letrd 9792 . . . . . . . . 9  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  a  <_  if ( M  <_ 
( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M ) )
139 elicopnf 11730 . . . . . . . . . 10  |-  ( 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 ) ) ) )
140139adantl 468 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) )
141133, 138, 140mpbir2and 933 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  if ( M  <_  ( ( |_ `  a )  +  1 ) ,  ( ( |_ `  a )  +  1 ) ,  M )  e.  ( a [,) +oo ) )
142 inelcm 3819 . . . . . . . 8  |-  ( ( 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 ) )  =/=  (/) )
143132, 141, 142syl2anc 667 . . . . . . 7  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( dom  F  i^i  ( a [,) +oo ) )  =/=  (/) )
144 imadisj 5187 . . . . . . . 8  |-  ( ( F " ( a [,) +oo ) )  =  (/)  <->  ( dom  F  i^i  ( a [,) +oo ) )  =  (/) )
145144necon3bii 2676 . . . . . . 7  |-  ( ( F " ( a [,) +oo ) )  =/=  (/)  <->  ( dom  F  i^i  ( a [,) +oo ) )  =/=  (/) )
146143, 145sylibr 216 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( F " ( a [,) +oo ) )  =/=  (/) )
147116, 146eqnetrd 2691 . . . . 5  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  (
( F " (
a [,) +oo )
)  i^i  RR* )  =/=  (/) )
148 supxrre1 11616 . . . . 5  |-  ( ( ( ( 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 ) )
149117, 147, 148syl2anc 667 . . . 4  |-  ( ( ( 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 ) )
150109, 149mpbird 236 . . 3  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  sup ( ( ( F
" ( a [,) +oo ) )  i^i  RR* ) ,  RR* ,  <  )  e.  RR )
1517, 150eqeltrd 2529 . 2  |-  ( ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  /\  a  e.  RR )  ->  ( G `  a )  e.  RR )
1523, 5, 151fmpt2d 6053 1  |-  ( ( M  e.  ZZ  /\  F : Z --> RR  /\  ( limsup `  F )  < +oo )  ->  G : RR --> RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 985    = wceq 1444    e. wcel 1887    =/= wne 2622   A.wral 2737   E.wrex 2738   _Vcvv 3045    i^i cin 3403    C_ wss 3404   (/)c0 3731   ifcif 3881   class class class wbr 4402    |-> cmpt 4461   dom cdm 4834   ran crn 4835   "cima 4837   -->wf 5578   ` cfv 5582  (class class class)co 6290   Fincfn 7569   supcsup 7954   RRcr 9538   1c1 9540    + caddc 9542   +oocpnf 9672   RR*cxr 9674    < clt 9675    <_ cle 9676   ZZcz 10937   ZZ>=cuz 11159   [,)cico 11637   ...cfz 11784   |_cfl 12026   limsupclspold 13525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-sup 7956  df-inf 7957  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-n0 10870  df-z 10938  df-uz 11160  df-ico 11641  df-fz 11785  df-fl 12028  df-limsupOLD 13527
This theorem is referenced by:  mbflimsupOLD  22624
  Copyright terms: Public domain W3C validator