seqfveq

Description: Equality of sequences. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

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

Step	Hyp	Ref	Expression
1		seqfveq.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		seqfveq.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) = G (k)$
3		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
4	1 3	syl	$⊢ φ \to M \in ℤ$
5		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
6	4 5	syl	$⊢ φ \to M \in ℤ_{\geq M}$
7		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
8	4 7	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
9		fveq2	$⊢ k = M \to F (k) = F (M)$
10		fveq2	$⊢ k = M \to G (k) = G (M)$
11	9 10	eqeq12d	$⊢ k = M \to (F (k) = G (k) \leftrightarrow F (M) = G (M))$
12	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) = G (k)$
13		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
14	1 13	syl	$⊢ φ \to M \in (M \dots N)$
15	11 12 14	rspcdva	$⊢ φ \to F (M) = G (M)$
16	8 15	eqtrd	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) = G (M)$
17		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
18	4 17	syl	$⊢ φ \to (M + 1 \dots N) \subseteq (M \dots N)$
19	18	sselda	$⊢ (φ \land k \in (M + 1 \dots N)) \to k \in (M \dots N)$
20	19 2	syldan	$⊢ (φ \land k \in (M + 1 \dots N)) \to F (k) = G (k)$
21	6 16 1 20	seqfveq2	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer