Theorem algrp1

Description: The value of the algorithm iterator R at ( K + 1 ) . (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 27-Dec-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 )
	algrf.5	|- ( ph -> F : S --> S )
Assertion	algrp1	|- ( ( ph /\ K e. Z ) -> ( R ` ( K + 1 ) ) = ( F ` ( R ` K ) ) )

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		algrf.5	|- ( ph -> F : S --> S )
6		simpr	|- ( ( ph /\ K e. Z ) -> K e. Z )
7	6 1	eleqtrdi	|- ( ( ph /\ K e. Z ) -> K e. ( ZZ>= ` M ) )
8		seqp1	|- ( K e. ( ZZ>= ` M ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( K + 1 ) ) = ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) ( F o. 1st ) ( ( Z X. { A } ) ` ( K + 1 ) ) ) )
9	7 8	syl	|- ( ( ph /\ K e. Z ) -> ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( K + 1 ) ) = ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) ( F o. 1st ) ( ( Z X. { A } ) ` ( K + 1 ) ) ) )
10	2	fveq1i	|- ( R ` ( K + 1 ) ) = ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` ( K + 1 ) )
11	2	fveq1i	|- ( R ` K ) = ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K )
12	11	fveq2i	|- ( F ` ( R ` K ) ) = ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) )
13		fvex	|- ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) e. _V
14		fvex	|- ( ( Z X. { A } ) ` ( K + 1 ) ) e. _V
15	13 14	opco1i	|- ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) ( F o. 1st ) ( ( Z X. { A } ) ` ( K + 1 ) ) ) = ( F ` ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) )
16	12 15	eqtr4i	|- ( F ` ( R ` K ) ) = ( ( seq M ( ( F o. 1st ) , ( Z X. { A } ) ) ` K ) ( F o. 1st ) ( ( Z X. { A } ) ` ( K + 1 ) ) )
17	9 10 16	3eqtr4g	|- ( ( ph /\ K e. Z ) -> ( R ` ( K + 1 ) ) = ( F ` ( R ` K ) ) )