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={\mathbb{Z}}_{\ge M}$$
	seqp1iOLD.2	$$⊢N\in Z$$
	seqp1iOLD.3	$$⊢K=N+1$$
	seqp1iOLD.4	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=A$$
	seqp1iOLD.5	$$⊢\phi \to F\left(K\right)=B$$
Assertion	seqp1iOLD	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=A\underset{\dot{}}{+}B$$

Proof

Step	Hyp	Ref	Expression
1		seqp1iOLD.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		seqp1iOLD.2	$$⊢N\in Z$$
3		seqp1iOLD.3	$$⊢K=N+1$$
4		seqp1iOLD.4	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=A$$
5		seqp1iOLD.5	$$⊢\phi \to F\left(K\right)=B$$
6	2	a1i	$$⊢\phi \to N\in Z$$
7	1 6 3 4 5	seqp1d	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=A\underset{\dot{}}{+}B$$