| Step |
Hyp |
Ref |
Expression |
| 1 |
|
limsupequz.1 |
|- F/ k ph |
| 2 |
|
limsupequz.2 |
|- F/_ k F |
| 3 |
|
limsupequz.3 |
|- F/_ k G |
| 4 |
|
limsupequz.4 |
|- ( ph -> M e. ZZ ) |
| 5 |
|
limsupequz.5 |
|- ( ph -> F Fn ( ZZ>= ` M ) ) |
| 6 |
|
limsupequz.6 |
|- ( ph -> N e. ZZ ) |
| 7 |
|
limsupequz.7 |
|- ( ph -> G Fn ( ZZ>= ` N ) ) |
| 8 |
|
limsupequz.8 |
|- ( ph -> K e. ZZ ) |
| 9 |
|
limsupequz.9 |
|- ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) ) |
| 10 |
|
nfv |
|- F/ j ph |
| 11 |
|
nfv |
|- F/ k j e. ( ZZ>= ` K ) |
| 12 |
1 11
|
nfan |
|- F/ k ( ph /\ j e. ( ZZ>= ` K ) ) |
| 13 |
|
nfcv |
|- F/_ k j |
| 14 |
2 13
|
nffv |
|- F/_ k ( F ` j ) |
| 15 |
3 13
|
nffv |
|- F/_ k ( G ` j ) |
| 16 |
14 15
|
nfeq |
|- F/ k ( F ` j ) = ( G ` j ) |
| 17 |
12 16
|
nfim |
|- F/ k ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( F ` j ) = ( G ` j ) ) |
| 18 |
|
eleq1w |
|- ( k = j -> ( k e. ( ZZ>= ` K ) <-> j e. ( ZZ>= ` K ) ) ) |
| 19 |
18
|
anbi2d |
|- ( k = j -> ( ( ph /\ k e. ( ZZ>= ` K ) ) <-> ( ph /\ j e. ( ZZ>= ` K ) ) ) ) |
| 20 |
|
fveq2 |
|- ( k = j -> ( F ` k ) = ( F ` j ) ) |
| 21 |
|
fveq2 |
|- ( k = j -> ( G ` k ) = ( G ` j ) ) |
| 22 |
20 21
|
eqeq12d |
|- ( k = j -> ( ( F ` k ) = ( G ` k ) <-> ( F ` j ) = ( G ` j ) ) ) |
| 23 |
19 22
|
imbi12d |
|- ( k = j -> ( ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) ) <-> ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( F ` j ) = ( G ` j ) ) ) ) |
| 24 |
17 23 9
|
chvarfv |
|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( F ` j ) = ( G ` j ) ) |
| 25 |
10 4 5 6 7 8 24
|
limsupequzlem |
|- ( ph -> ( limsup ` F ) = ( limsup ` G ) ) |