Metamath Proof Explorer


Theorem seqp1iOLD

Description: Obsolete version of seqp1d as of 3-May-2024. Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 seqp1iOLD.1
 |-  Z = ( ZZ>= ` M )
2 seqp1iOLD.2
 |-  N e. Z
3 seqp1iOLD.3
 |-  K = ( N + 1 )
4 seqp1iOLD.4
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = A )
5 seqp1iOLD.5
 |-  ( ph -> ( F ` K ) = B )
6 2 a1i
 |-  ( ph -> N e. Z )
7 1 6 3 4 5 seqp1d
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( A .+ B ) )