Theorem algr0

Description: The value of the algorithm iterator R at 0 is the initial state A . (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	algrf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	algrf.2	$$⊢R=seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)$$
	algrf.3	$$⊢\phi \to M\in \mathbb{Z}$$
	algrf.4	$$⊢\phi \to A\in S$$
Assertion	algr0	$$⊢\phi \to R\left(M\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		algrf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		algrf.2	$$⊢R=seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)$$
3		algrf.3	$$⊢\phi \to M\in \mathbb{Z}$$
4		algrf.4	$$⊢\phi \to A\in S$$
5	2	fveq1i	$$⊢R\left(M\right)=seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)\left(M\right)$$
6		seq1	$$⊢M\in \mathbb{Z}\to seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)\left(M\right)=\left(Z\times \left\{A\right\}\right)\left(M\right)$$
7	3 6	syl	$$⊢\phi \to seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)\left(M\right)=\left(Z\times \left\{A\right\}\right)\left(M\right)$$
8		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
9	3 8	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
10	9 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
11		fvconst2g	$$⊢\left(A\in S\wedge M\in Z\right)\to \left(Z\times \left\{A\right\}\right)\left(M\right)=A$$
12	4 10 11	syl2anc	$$⊢\phi \to \left(Z\times \left\{A\right\}\right)\left(M\right)=A$$
13	7 12	eqtrd	$$⊢\phi \to seqM\left(\left(F\circ 1^{st}\right),\left(Z\times \left\{A\right\}\right)\right)\left(M\right)=A$$
14	5 13	syl5eq	$$⊢\phi \to R\left(M\right)=A$$