Theorem seqfeq

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

	Ref	Expression
Hypotheses	seqfeq.1	$$⊢\phi \to M\in \mathbb{Z}$$
	seqfeq.2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=G\left(k\right)$$
Assertion	seqfeq	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)=seqM\left(\underset{\dot{}}{+},G\right)$$

Proof

Step	Hyp	Ref	Expression
1		seqfeq.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		seqfeq.2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=G\left(k\right)$$
3		seqfn	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}$$
4	1 3	syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}$$
5		seqfn	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},G\right)Fn{\mathbb{Z}}_{\ge M}$$
6	1 5	syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},G\right)Fn{\mathbb{Z}}_{\ge M}$$
7		simpr	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge M}\right)\to x\in {\mathbb{Z}}_{\ge M}$$
8		elfzuz	$$⊢k\in \left(M\dots x\right)\to k\in {\mathbb{Z}}_{\ge M}$$
9	8 2	sylan2	$$⊢\left(\phi \wedge k\in \left(M\dots x\right)\right)\to F\left(k\right)=G\left(k\right)$$
10	9	adantlr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{Z}}_{\ge M}\right)\wedge k\in \left(M\dots x\right)\right)\to F\left(k\right)=G\left(k\right)$$
11	7 10	seqfveq	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge M}\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(x\right)$$
12	4 6 11	eqfnfvd	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)=seqM\left(\underset{\dot{}}{+},G\right)$$