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	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
	seqsplit.2	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
	seqsplit.3	|- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
	seq1p.4	|- ( ph -> M e. ZZ )
	seq1p.5	|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
Assertion	seq1p	|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( F ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		seqsplit.1	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2		seqsplit.2	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
3		seqsplit.3	|- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
4		seq1p.4	|- ( ph -> M e. ZZ )
5		seq1p.5	|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
6		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
7	4 6	syl	|- ( ph -> M e. ( ZZ>= ` M ) )
8	1 2 3 7 5	seqsplit	|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )
9		seq1	|- ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
10	4 9	syl	|- ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
11	10	oveq1d	|- ( ph -> ( ( seq M ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) = ( ( F ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )
12	8 11	eqtrd	|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( F ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )