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 = ( ZZ>= ` M )
	algrf.2	|- R = seq M ( ( F o. 1st ) , ( Z X. { A } ) )
	algrf.3	|- ( ph -> M e. ZZ )
	algrf.4	|- ( ph -> A e. S )
Assertion	algr0	|- ( ph -> ( R ` M ) = A )

Proof

Step	Hyp	Ref	Expression
1		algrf.1	|- Z = ( ZZ>= ` M )
2		algrf.2	|- R = seq M ( ( F o. 1st ) , ( Z X. { A } ) )
3		algrf.3	|- ( ph -> M e. ZZ )
4		algrf.4	|- ( ph -> A e. S )
5	2	fveq1i	|- ( R ` M ) = ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M )
6		seq1	|- ( M e. ZZ -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( ( Z X. { A } ) ` M ) )
7	3 6	syl	|- ( ph -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = ( ( Z X. { A } ) ` M ) )
8		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
9	3 8	syl	|- ( ph -> M e. ( ZZ>= ` M ) )
10	9 1	eleqtrrdi	|- ( ph -> M e. Z )
11		fvconst2g	|- ( ( A e. S /\ M e. Z ) -> ( ( Z X. { A } ) ` M ) = A )
12	4 10 11	syl2anc	|- ( ph -> ( ( Z X. { A } ) ` M ) = A )
13	7 12	eqtrd	|- ( ph -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` M ) = A )
14	5 13	syl5eq	|- ( ph -> ( R ` M ) = A )