seqfeq

Description: Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqfeq.1	$⊢ φ \to M \in ℤ$
	seqfeq.2	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = G (k)$
Assertion	seqfeq	$⊢ φ \to seq M (\underset{˙}{+}, F) = seq M (\underset{˙}{+}, G)$

Step	Hyp	Ref	Expression
1		seqfeq.1	$⊢ φ \to M \in ℤ$
2		seqfeq.2	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = G (k)$
3		seqfn	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$
4	1 3	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$
5		seqfn	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, G) Fn ℤ_{\geq M}$
6	1 5	syl	$⊢ φ \to seq M (\underset{˙}{+}, G) Fn ℤ_{\geq M}$
7		simpr	$⊢ (φ \land x \in ℤ_{\geq M}) \to x \in ℤ_{\geq M}$
8		elfzuz	$⊢ k \in (M \dots x) \to k \in ℤ_{\geq M}$
9	8 2	sylan2	$⊢ (φ \land k \in (M \dots x)) \to F (k) = G (k)$
10	9	adantlr	$⊢ ((φ \land x \in ℤ_{\geq M}) \land k \in (M \dots x)) \to F (k) = G (k)$
11	7 10	seqfveq	$⊢ (φ \land x \in ℤ_{\geq M}) \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, G) (x)$
12	4 6 11	eqfnfvd	$⊢ φ \to seq M (\underset{˙}{+}, F) = seq M (\underset{˙}{+}, G)$

Metamath Proof Explorer