This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )