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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
algrf.2 ⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
algrf.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
algrf.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
Assertion algr0 ( 𝜑 → ( 𝑅 ‘ 𝑀 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 algrf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 algrf.2 ⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
3 algrf.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 algrf.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
5 2 fveq1i ⊢ ( 𝑅 ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 )
6 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
7 3 6 syl ⊢ ( 𝜑 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
8 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 3 8 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 9 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
11 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑀 ∈ 𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = 𝐴 )
12 4 10 11 syl2anc ⊢ ( 𝜑 → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = 𝐴 )
13 7 12 eqtrd ⊢ ( 𝜑 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = 𝐴 )
14 5 13 eqtrid ⊢ ( 𝜑 → ( 𝑅 ‘ 𝑀 ) = 𝐴 )