Theorem seq1i

Description: Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypotheses	seq1i.1	$$⊢M\in \mathbb{Z}$$
	seq1i.2	$$⊢\phi \to F\left(M\right)=A$$
Assertion	seq1i	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		seq1i.1	$$⊢M\in \mathbb{Z}$$
2		seq1i.2	$$⊢\phi \to F\left(M\right)=A$$
3		seq1	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=F\left(M\right)$$
4	1 3	ax-mp	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=F\left(M\right)$$
5	4 2	eqtrid	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=A$$