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