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

Proof

Step	Hyp	Ref	Expression
1		seqp1iOLD.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		seqp1iOLD.2	⊢ 𝑁 ∈ 𝑍
3		seqp1iOLD.3	⊢ 𝐾 = ( 𝑁 + 1 )
4		seqp1iOLD.4	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
5		seqp1iOLD.5	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
6	2	a1i	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
7	1 6 3 4 5	seqp1d	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )