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

Proof

Step	Hyp	Ref	Expression
1		seqp1d.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		seqp1d.2	$$⊢\phi \to N\in Z$$
3		seqp1d.3	$$⊢K=N+1$$
4		seqp1d.4	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=A$$
5		seqp1d.5	$$⊢\phi \to F\left(K\right)=B$$
6	3	fveq2i	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(N+1\right)$$
7	6	a1i	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(N+1\right)$$
8	2 1	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
9		seqp1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to seqM\left(\underset{\dot{}}{+},F\right)\left(N+1\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\underset{\dot{}}{+}F\left(N+1\right)$$
10	8 9	syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N+1\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\underset{\dot{}}{+}F\left(N+1\right)$$
11	3	fveq2i	$$⊢F\left(K\right)=F\left(N+1\right)$$
12	11 5	syl5eqr	$$⊢\phi \to F\left(N+1\right)=B$$
13	4 12	oveq12d	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\underset{\dot{}}{+}F\left(N+1\right)=A\underset{\dot{}}{+}B$$
14	7 10 13	3eqtrd	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(K\right)=A\underset{\dot{}}{+}B$$