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 = ℤ_{\geq M}$
		algrf.2	$⊢ R = seq M ((F \circ 1^{st}), (Z \times \{A\}))$
		algrf.3	$⊢ φ \to M \in ℤ$
		algrf.4	$⊢ φ \to A \in S$
	Assertion	algr0	$⊢ φ \to R (M) = A$

Proof

Step	Hyp	Ref	Expression
1		algrf.1	$⊢ Z = ℤ_{\geq M}$
2		algrf.2	$⊢ R = seq M ((F \circ 1^{st}), (Z \times \{A\}))$
3		algrf.3	$⊢ φ \to M \in ℤ$
4		algrf.4	$⊢ φ \to A \in S$
5	2	fveq1i	$⊢ R (M) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (M)$
6		seq1	$⊢ M \in ℤ \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = (Z \times \{A\}) (M)$
7	3 6	syl	$⊢ φ \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = (Z \times \{A\}) (M)$
8		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
9	3 8	syl	$⊢ φ \to M \in ℤ_{\geq M}$
10	9 1	eleqtrrdi	$⊢ φ \to M \in Z$
11		fvconst2g	$⊢ (A \in S \land M \in Z) \to (Z \times \{A\}) (M) = A$
12	4 10 11	syl2anc	$⊢ φ \to (Z \times \{A\}) (M) = A$
13	7 12	eqtrd	$⊢ φ \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (M) = A$
14	5 13	eqtrid	$⊢ φ \to R (M) = A$