Theorem seqfeq2

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

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

Proof

Step	Hyp	Ref	Expression
1		seqfveq2.1	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge M}$$
2		seqfveq2.2	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=G\left(K\right)$$
3		seqfeq2.4	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge \left(K+1\right)}\right)\to F\left(k\right)=G\left(k\right)$$
4		eluzel2	$$⊢K\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
5		seqfn	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}$$
6	1 4 5	3syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}$$
7		uzss	$$⊢K\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge K}\subseteq {\mathbb{Z}}_{\ge M}$$
8	1 7	syl	$$⊢\phi \to {\mathbb{Z}}_{\ge K}\subseteq {\mathbb{Z}}_{\ge M}$$
9		fnssres	$$⊢\left(seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}\wedge {\mathbb{Z}}_{\ge K}\subseteq {\mathbb{Z}}_{\ge M}\right)\to \left({seqM\left(\underset{\dot{}}{+},F\right)\upharpoonright }_{{\mathbb{Z}}_{\ge K}}\right)Fn{\mathbb{Z}}_{\ge K}$$
10	6 8 9	syl2anc	$$⊢\phi \to \left({seqM\left(\underset{\dot{}}{+},F\right)\upharpoonright }_{{\mathbb{Z}}_{\ge K}}\right)Fn{\mathbb{Z}}_{\ge K}$$
11		eluzelz	$$⊢K\in {\mathbb{Z}}_{\ge M}\to K\in \mathbb{Z}$$
12		seqfn	$$⊢K\in \mathbb{Z}\to seqK\left(\underset{\dot{}}{+},G\right)Fn{\mathbb{Z}}_{\ge K}$$
13	1 11 12	3syl	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},G\right)Fn{\mathbb{Z}}_{\ge K}$$
14		fvres	$$⊢x\in {\mathbb{Z}}_{\ge K}\to \left({seqM\left(\underset{\dot{}}{+},F\right)\upharpoonright }_{{\mathbb{Z}}_{\ge K}}\right)\left(x\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)$$
15	14	adantl	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\to \left({seqM\left(\underset{\dot{}}{+},F\right)\upharpoonright }_{{\mathbb{Z}}_{\ge K}}\right)\left(x\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)$$
16	1	adantr	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\to K\in {\mathbb{Z}}_{\ge M}$$
17	2	adantr	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=G\left(K\right)$$
18		simpr	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\to x\in {\mathbb{Z}}_{\ge K}$$
19		elfzuz	$$⊢k\in \left(K+1\dots x\right)\to k\in {\mathbb{Z}}_{\ge \left(K+1\right)}$$
20	19 3	sylan2	$$⊢\left(\phi \wedge k\in \left(K+1\dots x\right)\right)\to F\left(k\right)=G\left(k\right)$$
21	20	adantlr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\wedge k\in \left(K+1\dots x\right)\right)\to F\left(k\right)=G\left(k\right)$$
22	16 17 18 21	seqfveq2	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},G\right)\left(x\right)$$
23	15 22	eqtrd	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge K}\right)\to \left({seqM\left(\underset{\dot{}}{+},F\right)\upharpoonright }_{{\mathbb{Z}}_{\ge K}}\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},G\right)\left(x\right)$$
24	10 13 23	eqfnfvd	$$⊢\phi \to {seqM\left(\underset{\dot{}}{+},F\right)\upharpoonright }_{{\mathbb{Z}}_{\ge K}}=seqK\left(\underset{\dot{}}{+},G\right)$$