This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupequzmptf

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupequzmptf.j 
|- F/ j ph
limsupequzmptf.o 
|- F/_ j A
limsupequzmptf.p 
|- F/_ j B
limsupequzmptf.m 
|- ( ph -> M e. ZZ )
limsupequzmptf.n 
|- ( ph -> N e. ZZ )
limsupequzmptf.a 
|- A = ( ZZ>= ` M )
limsupequzmptf.b 
|- B = ( ZZ>= ` N )
limsupequzmptf.c 
|- ( ( ph /\ j e. A ) -> C e. V )
limsupequzmptf.d 
|- ( ( ph /\ j e. B ) -> C e. W )
Assertion limsupequzmptf 
|- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )

Proof

Step Hyp Ref Expression
1 limsupequzmptf.j 
 |-  F/ j ph
2 limsupequzmptf.o 
 |-  F/_ j A
3 limsupequzmptf.p 
 |-  F/_ j B
4 limsupequzmptf.m 
 |-  ( ph -> M e. ZZ )
5 limsupequzmptf.n 
 |-  ( ph -> N e. ZZ )
6 limsupequzmptf.a 
 |-  A = ( ZZ>= ` M )
7 limsupequzmptf.b 
 |-  B = ( ZZ>= ` N )
8 limsupequzmptf.c 
 |-  ( ( ph /\ j e. A ) -> C e. V )
9 limsupequzmptf.d 
 |-  ( ( ph /\ j e. B ) -> C e. W )
10 nfv 
 |-  F/ k ph
11 2 nfcri 
 |-  F/ j k e. A
12 1 11 nfan 
 |-  F/ j ( ph /\ k e. A )
13 nfcsb1v 
 |-  F/_ j [_ k / j ]_ C
14 nfcv 
 |-  F/_ j V
15 13 14 nfel 
 |-  F/ j [_ k / j ]_ C e. V
16 12 15 nfim 
 |-  F/ j ( ( ph /\ k e. A ) -> [_ k / j ]_ C e. V )
17 eleq1w 
 |-  ( j = k -> ( j e. A <-> k e. A ) )
18 17 anbi2d 
 |-  ( j = k -> ( ( ph /\ j e. A ) <-> ( ph /\ k e. A ) ) )
19 csbeq1a 
 |-  ( j = k -> C = [_ k / j ]_ C )
20 19 eleq1d 
 |-  ( j = k -> ( C e. V <-> [_ k / j ]_ C e. V ) )
21 18 20 imbi12d 
 |-  ( j = k -> ( ( ( ph /\ j e. A ) -> C e. V ) <-> ( ( ph /\ k e. A ) -> [_ k / j ]_ C e. V ) ) )
22 16 21 8 chvarfv 
 |-  ( ( ph /\ k e. A ) -> [_ k / j ]_ C e. V )
23 3 nfcri 
 |-  F/ j k e. B
24 1 23 nfan 
 |-  F/ j ( ph /\ k e. B )
25 nfcv 
 |-  F/_ j W
26 13 25 nfel 
 |-  F/ j [_ k / j ]_ C e. W
27 24 26 nfim 
 |-  F/ j ( ( ph /\ k e. B ) -> [_ k / j ]_ C e. W )
28 eleq1w 
 |-  ( j = k -> ( j e. B <-> k e. B ) )
29 28 anbi2d 
 |-  ( j = k -> ( ( ph /\ j e. B ) <-> ( ph /\ k e. B ) ) )
30 19 eleq1d 
 |-  ( j = k -> ( C e. W <-> [_ k / j ]_ C e. W ) )
31 29 30 imbi12d 
 |-  ( j = k -> ( ( ( ph /\ j e. B ) -> C e. W ) <-> ( ( ph /\ k e. B ) -> [_ k / j ]_ C e. W ) ) )
32 27 31 9 chvarfv 
 |-  ( ( ph /\ k e. B ) -> [_ k / j ]_ C e. W )
33 10 4 5 6 7 22 32 limsupequzmpt 
 |-  ( ph -> ( limsup ` ( k e. A |-> [_ k / j ]_ C ) ) = ( limsup ` ( k e. B |-> [_ k / j ]_ C ) ) )
34 nfcv 
 |-  F/_ k A
35 nfcv 
 |-  F/_ k C
36 2 34 35 13 19 cbvmptf 
 |-  ( j e. A |-> C ) = ( k e. A |-> [_ k / j ]_ C )
37 36 fveq2i 
 |-  ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( k e. A |-> [_ k / j ]_ C ) )
38 37 a1i 
 |-  ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( k e. A |-> [_ k / j ]_ C ) ) )
39 nfcv 
 |-  F/_ k B
40 3 39 35 13 19 cbvmptf 
 |-  ( j e. B |-> C ) = ( k e. B |-> [_ k / j ]_ C )
41 40 fveq2i 
 |-  ( limsup ` ( j e. B |-> C ) ) = ( limsup ` ( k e. B |-> [_ k / j ]_ C ) )
42 41 a1i 
 |-  ( ph -> ( limsup ` ( j e. B |-> C ) ) = ( limsup ` ( k e. B |-> [_ k / j ]_ C ) ) )
43 33 38 42 3eqtr4d 
 |-  ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )