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 e. ZZ -> seq M ( .+ , ( F |` ( ZZ>= ` M ) ) ) = seq M ( .+ , F ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( M e. ZZ -> M e. ZZ )
2		fvres	|- ( k e. ( ZZ>= ` M ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
3	2	adantl	|- ( ( M e. ZZ /\ k e. ( ZZ>= ` M ) ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
4	1 3	seqfeq	|- ( M e. ZZ -> seq M ( .+ , ( F |` ( ZZ>= ` M ) ) ) = seq M ( .+ , F ) )