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

Metamath Proof Explorer

Theorem seqp1d

Description: Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by AV, 3-May-2024)

Ref Expression
Hypotheses seqp1d.1 
|- Z = ( ZZ>= ` M )
seqp1d.2 
|- ( ph -> N e. Z )
seqp1d.3 
|- K = ( N + 1 )
seqp1d.4 
|- ( ph -> ( seq M ( .+ , F ) ` N ) = A )
seqp1d.5 
|- ( ph -> ( F ` K ) = B )
Assertion seqp1d 
|- ( ph -> ( seq M ( .+ , F ) ` K ) = ( A .+ B ) )

Proof

Step Hyp Ref Expression
1 seqp1d.1 
 |-  Z = ( ZZ>= ` M )
2 seqp1d.2 
 |-  ( ph -> N e. Z )
3 seqp1d.3 
 |-  K = ( N + 1 )
4 seqp1d.4 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = A )
5 seqp1d.5 
 |-  ( ph -> ( F ` K ) = B )
6 3 fveq2i 
 |-  ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( N + 1 ) )
7 6 a1i 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( N + 1 ) ) )
8 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
9 seqp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
10 8 9 syl 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
11 3 fveq2i 
 |-  ( F ` K ) = ( F ` ( N + 1 ) )
12 11 5 eqtr3id 
 |-  ( ph -> ( F ` ( N + 1 ) ) = B )
13 4 12 oveq12d 
 |-  ( ph -> ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) = ( A .+ B ) )
14 7 10 13 3eqtrd 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( A .+ B ) )