Metamath Proof Explorer

Theorem seqm1

Description: Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Assertion seqm1 
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )

Proof

Step Hyp Ref Expression
1 eluzp1m1 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
2 seqp1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( ( N - 1 ) + 1 ) ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` ( ( N - 1 ) + 1 ) ) ) )
3 1 2 syl 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` ( ( N - 1 ) + 1 ) ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` ( ( N - 1 ) + 1 ) ) ) )
4 eluzelcn 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. CC )
5 ax-1cn 
 |-  1 e. CC
6 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
7 4 5 6 sylancl 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( ( N - 1 ) + 1 ) = N )
8 7 adantl 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
9 8 fveq2d 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` ( ( N - 1 ) + 1 ) ) = ( seq M ( .+ , F ) ` N ) )
10 8 fveq2d 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` ( ( N - 1 ) + 1 ) ) = ( F ` N ) )
11 10 oveq2d 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` ( ( N - 1 ) + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )
12 3 9 11 3eqtr3d 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )