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 Z = M
seqp1iOLD.2 N Z
seqp1iOLD.3 K = N + 1
seqp1iOLD.4 φ seq M + ˙ F N = A
seqp1iOLD.5 φ F K = B
Assertion seqp1iOLD φ seq M + ˙ F K = A + ˙ B

Proof

Step Hyp Ref Expression
1 seqp1iOLD.1 Z = M
2 seqp1iOLD.2 N Z
3 seqp1iOLD.3 K = N + 1
4 seqp1iOLD.4 φ seq M + ˙ F N = A
5 seqp1iOLD.5 φ F K = B
6 2 a1i φ N Z
7 1 6 3 4 5 seqp1d φ seq M + ˙ F K = A + ˙ B