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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	seqp1d.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	seqp1d.3	⊢ 𝐾 = ( 𝑁 + 1 )
	seqp1d.4	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
	seqp1d.5	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
Assertion	seqp1d	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		seqp1d.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		seqp1d.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3		seqp1d.3	⊢ 𝐾 = ( 𝑁 + 1 )
4		seqp1d.4	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
5		seqp1d.5	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
6	3	fveq2i	⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) )
7	6	a1i	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
8	2 1	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
9		seqp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
10	8 9	syl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
11	3	fveq2i	⊢ ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ ( 𝑁 + 1 ) )
12	11 5	syl5eqr	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = 𝐵 )
13	4 12	oveq12d	⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐴 + 𝐵 ) )
14	7 10 13	3eqtrd	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )