Metamath Proof Explorer


Theorem seq1p

Description: Removing the first term from a sequence. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqsplit.1 φxSySx+˙yS
seqsplit.2 φxSySzSx+˙y+˙z=x+˙y+˙z
seqsplit.3 φNM+1
seq1p.4 φM
seq1p.5 φxMNFxS
Assertion seq1p φseqM+˙FN=FM+˙seqM+1+˙FN

Proof

Step Hyp Ref Expression
1 seqsplit.1 φxSySx+˙yS
2 seqsplit.2 φxSySzSx+˙y+˙z=x+˙y+˙z
3 seqsplit.3 φNM+1
4 seq1p.4 φM
5 seq1p.5 φxMNFxS
6 uzid MMM
7 4 6 syl φMM
8 1 2 3 7 5 seqsplit φseqM+˙FN=seqM+˙FM+˙seqM+1+˙FN
9 seq1 MseqM+˙FM=FM
10 4 9 syl φseqM+˙FM=FM
11 10 oveq1d φseqM+˙FM+˙seqM+1+˙FN=FM+˙seqM+1+˙FN
12 8 11 eqtrd φseqM+˙FN=FM+˙seqM+1+˙FN