# Metamath Proof Explorer

## 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 {ℤ}_{\ge {M}}$
seqfveq2.2
seqfeq2.4 ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({K}+1\right)}\right)\to {F}\left({k}\right)={G}\left({k}\right)$
Assertion seqfeq2

### Proof

Step Hyp Ref Expression
1 seqfveq2.1 ${⊢}{\phi }\to {K}\in {ℤ}_{\ge {M}}$
2 seqfveq2.2
3 seqfeq2.4 ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({K}+1\right)}\right)\to {F}\left({k}\right)={G}\left({k}\right)$
4 eluzel2 ${⊢}{K}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
5 seqfn
6 1 4 5 3syl
7 uzss ${⊢}{K}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {K}}\subseteq {ℤ}_{\ge {M}}$
8 1 7 syl ${⊢}{\phi }\to {ℤ}_{\ge {K}}\subseteq {ℤ}_{\ge {M}}$
9 fnssres
10 6 8 9 syl2anc
11 eluzelz ${⊢}{K}\in {ℤ}_{\ge {M}}\to {K}\in ℤ$
12 seqfn
13 1 11 12 3syl
14 fvres
15 14 adantl
16 1 adantr ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge {K}}\right)\to {K}\in {ℤ}_{\ge {M}}$
17 2 adantr
18 simpr ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge {K}}\right)\to {x}\in {ℤ}_{\ge {K}}$
19 elfzuz ${⊢}{k}\in \left({K}+1\dots {x}\right)\to {k}\in {ℤ}_{\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 {ℤ}_{\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
23 15 22 eqtrd
24 10 13 23 eqfnfvd