This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 ) ) )