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	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) = seq 𝑀 ( + , 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℤ )
2		fvres	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
3	2	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
4	1 3	seqfeq	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) = seq 𝑀 ( + , 𝐹 ) )