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