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 𝑍 = ( ℤ𝑀 )
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 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )