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