This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℤ \to seq M (\underset{˙}{+}, ({F ↾}_{ℤ_{\geq M}})) = seq M (\underset{˙}{+}, F)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ M \in ℤ \to M \in ℤ$
2		fvres	$⊢ k \in ℤ_{\geq M} \to ({F ↾}_{ℤ_{\geq M}}) (k) = F (k)$
3	2	adantl	$⊢ (M \in ℤ \land k \in ℤ_{\geq M}) \to ({F ↾}_{ℤ_{\geq M}}) (k) = F (k)$
4	1 3	seqfeq	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, ({F ↾}_{ℤ_{\geq M}})) = seq M (\underset{˙}{+}, F)$