Metamath Proof Explorer

Theorem limsupequzlem

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 limsupequzlem.1 
|- F/ k ph
limsupequzlem.2 
|- ( ph -> M e. ZZ )
limsupequzlem.4 
|- ( ph -> F Fn ( ZZ>= ` M ) )
limsupequzlem.5 
|- ( ph -> N e. ZZ )
limsupequzlem.6 
|- ( ph -> G Fn ( ZZ>= ` N ) )
limsupequzlem.7 
|- ( ph -> K e. ZZ )
limsupequzlem.8 
|- ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) )
Assertion limsupequzlem 
|- ( ph -> ( limsup ` F ) = ( limsup ` G ) )

Proof

Step Hyp Ref Expression
1 limsupequzlem.1 
 |-  F/ k ph
2 limsupequzlem.2 
 |-  ( ph -> M e. ZZ )
3 limsupequzlem.4 
 |-  ( ph -> F Fn ( ZZ>= ` M ) )
4 limsupequzlem.5 
 |-  ( ph -> N e. ZZ )
5 limsupequzlem.6 
 |-  ( ph -> G Fn ( ZZ>= ` N ) )
6 limsupequzlem.7 
 |-  ( ph -> K e. ZZ )
7 limsupequzlem.8 
 |-  ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) )
8 eqid 
 |-  ( ZZ>= ` K ) = ( ZZ>= ` K )
9 6 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> K e. ZZ )
10 eluzelz 
 |-  ( k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) -> k e. ZZ )
11 10 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> k e. ZZ )
12 6 zred 
 |-  ( ph -> K e. RR )
13 12 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> K e. RR )
14 13 rexrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> K e. RR* )
15 zssxr 
 |-  ZZ C_ RR*
16 tpssi 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> { M , N , K } C_ ZZ )
17 2 4 6 16 syl3anc 
 |-  ( ph -> { M , N , K } C_ ZZ )
18 xrltso 
 |-  < Or RR*
19 18 a1i 
 |-  ( ph -> < Or RR* )
20 tpfi 
 |-  { M , N , K } e. Fin
21 20 a1i 
 |-  ( ph -> { M , N , K } e. Fin )
22 2 tpnzd 
 |-  ( ph -> { M , N , K } =/= (/) )
23 15 a1i 
 |-  ( ph -> ZZ C_ RR* )
24 17 23 sstrd 
 |-  ( ph -> { M , N , K } C_ RR* )
25 fisupcl 
 |-  ( ( < Or RR* /\ ( { M , N , K } e. Fin /\ { M , N , K } =/= (/) /\ { M , N , K } C_ RR* ) ) -> sup ( { M , N , K } , RR* , < ) e. { M , N , K } )
26 19 21 22 24 25 syl13anc 
 |-  ( ph -> sup ( { M , N , K } , RR* , < ) e. { M , N , K } )
27 17 26 sseldd 
 |-  ( ph -> sup ( { M , N , K } , RR* , < ) e. ZZ )
28 15 27 sselid 
 |-  ( ph -> sup ( { M , N , K } , RR* , < ) e. RR* )
29 28 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> sup ( { M , N , K } , RR* , < ) e. RR* )
30 eluzelre 
 |-  ( k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) -> k e. RR )
31 30 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> k e. RR )
32 31 rexrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> k e. RR* )
33 tpid3g 
 |-  ( K e. ZZ -> K e. { M , N , K } )
34 6 33 syl 
 |-  ( ph -> K e. { M , N , K } )
35 eqid 
 |-  sup ( { M , N , K } , RR* , < ) = sup ( { M , N , K } , RR* , < )
36 24 34 35 supxrubd 
 |-  ( ph -> K <_ sup ( { M , N , K } , RR* , < ) )
37 36 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> K <_ sup ( { M , N , K } , RR* , < ) )
38 eluzle 
 |-  ( k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) -> sup ( { M , N , K } , RR* , < ) <_ k )
39 38 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> sup ( { M , N , K } , RR* , < ) <_ k )
40 14 29 32 37 39 xrletrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> K <_ k )
41 8 9 11 40 eluzd 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> k e. ( ZZ>= ` K ) )
42 41 7 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) -> ( F ` k ) = ( G ` k ) )
43 1 42 ralrimia 
 |-  ( ph -> A. k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ( F ` k ) = ( G ` k ) )
44 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
45 tpid1g 
 |-  ( M e. ZZ -> M e. { M , N , K } )
46 2 45 syl 
 |-  ( ph -> M e. { M , N , K } )
47 24 46 35 supxrubd 
 |-  ( ph -> M <_ sup ( { M , N , K } , RR* , < ) )
48 44 2 27 47 eluzd 
 |-  ( ph -> sup ( { M , N , K } , RR* , < ) e. ( ZZ>= ` M ) )
49 uzss 
 |-  ( sup ( { M , N , K } , RR* , < ) e. ( ZZ>= ` M ) -> ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) C_ ( ZZ>= ` M ) )
50 48 49 syl 
 |-  ( ph -> ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) C_ ( ZZ>= ` M ) )
51 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
52 tpid2g 
 |-  ( N e. ZZ -> N e. { M , N , K } )
53 4 52 syl 
 |-  ( ph -> N e. { M , N , K } )
54 24 53 35 supxrubd 
 |-  ( ph -> N <_ sup ( { M , N , K } , RR* , < ) )
55 51 4 27 54 eluzd 
 |-  ( ph -> sup ( { M , N , K } , RR* , < ) e. ( ZZ>= ` N ) )
56 uzss 
 |-  ( sup ( { M , N , K } , RR* , < ) e. ( ZZ>= ` N ) -> ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) C_ ( ZZ>= ` N ) )
57 55 56 syl 
 |-  ( ph -> ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) C_ ( ZZ>= ` N ) )
58 fvreseq0 
 |-  ( ( ( F Fn ( ZZ>= ` M ) /\ G Fn ( ZZ>= ` N ) ) /\ ( ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) C_ ( ZZ>= ` M ) /\ ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) C_ ( ZZ>= ` N ) ) ) -> ( ( F |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) = ( G |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) <-> A. k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ( F ` k ) = ( G ` k ) ) )
59 3 5 50 57 58 syl22anc 
 |-  ( ph -> ( ( F |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) = ( G |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) <-> A. k e. ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ( F ` k ) = ( G ` k ) ) )
60 43 59 mpbird 
 |-  ( ph -> ( F |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) = ( G |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) )
61 60 fveq2d 
 |-  ( ph -> ( limsup ` ( F |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) ) = ( limsup ` ( G |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) ) )
62 eqid 
 |-  ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) = ( ZZ>= ` sup ( { M , N , K } , RR* , < ) )
63 fvexd 
 |-  ( ph -> ( ZZ>= ` M ) e. _V )
64 3 63 fnexd 
 |-  ( ph -> F e. _V )
65 3 fndmd 
 |-  ( ph -> dom F = ( ZZ>= ` M ) )
66 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
67 65 66 eqsstrdi 
 |-  ( ph -> dom F C_ ZZ )
68 27 62 64 67 limsupresuz2 
 |-  ( ph -> ( limsup ` ( F |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) ) = ( limsup ` F ) )
69 fvexd 
 |-  ( ph -> ( ZZ>= ` N ) e. _V )
70 5 69 fnexd 
 |-  ( ph -> G e. _V )
71 5 fndmd 
 |-  ( ph -> dom G = ( ZZ>= ` N ) )
72 uzssz 
 |-  ( ZZ>= ` N ) C_ ZZ
73 71 72 eqsstrdi 
 |-  ( ph -> dom G C_ ZZ )
74 27 62 70 73 limsupresuz2 
 |-  ( ph -> ( limsup ` ( G |` ( ZZ>= ` sup ( { M , N , K } , RR* , < ) ) ) ) = ( limsup ` G ) )
75 61 68 74 3eqtr3d 
 |-  ( ph -> ( limsup ` F ) = ( limsup ` G ) )