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	syl5eq	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑀 ) = 𝐴 )