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

Metamath Proof Explorer

Theorem climresmpt

Proof