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

Metamath Proof Explorer

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 eqtrid 
 |-  ( ph -> ( R ` M ) = A )