Theorem seqres

Description: Restricting its characteristic function to ( ZZ>=M ) does not affect the seq function. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Assertion	seqres	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)=seqM\left(\underset{\dot{}}{+},F\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢M\in \mathbb{Z}\to M\in \mathbb{Z}$$
2		fvres	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\left(k\right)=F\left(k\right)$$
3	2	adantl	$$⊢\left(M\in \mathbb{Z}\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\left(k\right)=F\left(k\right)$$
4	1 3	seqfeq	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)=seqM\left(\underset{\dot{}}{+},F\right)$$