Metamath Proof Explorer

Theorem climresmpt

Description: A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses climresmpt.z 
|- Z = ( ZZ>= ` M )
climresmpt.f 
|- F = ( x e. Z |-> A )
climresmpt.n 
|- ( ph -> N e. Z )
climresmpt.g 
|- G = ( x e. ( ZZ>= ` N ) |-> A )
Assertion climresmpt 
|- ( ph -> ( G ~~> B <-> F ~~> B ) )

Proof

Step Hyp Ref Expression
1 climresmpt.z 
 |-  Z = ( ZZ>= ` M )
2 climresmpt.f 
 |-  F = ( x e. Z |-> A )
3 climresmpt.n 
 |-  ( ph -> N e. Z )
4 climresmpt.g 
 |-  G = ( x e. ( ZZ>= ` N ) |-> A )
5 2 reseq1i 
 |-  ( F |` ( ZZ>= ` N ) ) = ( ( x e. Z |-> A ) |` ( ZZ>= ` N ) )
6 5 a1i 
 |-  ( ph -> ( F |` ( ZZ>= ` N ) ) = ( ( x e. Z |-> A ) |` ( ZZ>= ` N ) ) )
7 3 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
8 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
9 7 8 syl 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
10 9 1 sseqtrrdi 
 |-  ( ph -> ( ZZ>= ` N ) C_ Z )
11 resmpt 
 |-  ( ( ZZ>= ` N ) C_ Z -> ( ( x e. Z |-> A ) |` ( ZZ>= ` N ) ) = ( x e. ( ZZ>= ` N ) |-> A ) )
12 10 11 syl 
 |-  ( ph -> ( ( x e. Z |-> A ) |` ( ZZ>= ` N ) ) = ( x e. ( ZZ>= ` N ) |-> A ) )
13 4 eqcomi 
 |-  ( x e. ( ZZ>= ` N ) |-> A ) = G
14 13 a1i 
 |-  ( ph -> ( x e. ( ZZ>= ` N ) |-> A ) = G )
15 6 12 14 3eqtrrd 
 |-  ( ph -> G = ( F |` ( ZZ>= ` N ) ) )
16 15 breq1d 
 |-  ( ph -> ( G ~~> B <-> ( F |` ( ZZ>= ` N ) ) ~~> B ) )
17 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
18 7 17 syl 
 |-  ( ph -> N e. ZZ )
19 1 fvexi 
 |-  Z e. _V
20 19 mptex 
 |-  ( x e. Z |-> A ) e. _V
21 20 a1i 
 |-  ( ph -> ( x e. Z |-> A ) e. _V )
22 2 21 eqeltrid 
 |-  ( ph -> F e. _V )
23 climres 
 |-  ( ( N e. ZZ /\ F e. _V ) -> ( ( F |` ( ZZ>= ` N ) ) ~~> B <-> F ~~> B ) )
24 18 22 23 syl2anc 
 |-  ( ph -> ( ( F |` ( ZZ>= ` N ) ) ~~> B <-> F ~~> B ) )
25 16 24 bitrd 
 |-  ( ph -> ( G ~~> B <-> F ~~> B ) )