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 = ℤ_{\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$
		algrf.5	$⊢ φ \to F : S ⟶ S$
	Assertion	algrp1	$⊢ (φ \land K \in Z) \to R (K + 1) = F (R (K))$

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		algrf.5	$⊢ φ \to F : S ⟶ S$
6		simpr	$⊢ (φ \land K \in Z) \to K \in Z$
7	6 1	eleqtrdi	$⊢ (φ \land K \in Z) \to K \in ℤ_{\geq M}$
8		seqp1	$⊢ K \in ℤ_{\geq M} \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (K + 1) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (K) (F \circ 1^{st}) (Z \times \{A\}) (K + 1)$
9	7 8	syl	$⊢ (φ \land K \in Z) \to seq M ((F \circ 1^{st}), (Z \times \{A\})) (K + 1) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (K) (F \circ 1^{st}) (Z \times \{A\}) (K + 1)$
10	2	fveq1i	$⊢ R (K + 1) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (K + 1)$
11	2	fveq1i	$⊢ R (K) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (K)$
12	11	fveq2i	$⊢ F (R (K)) = F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (K))$
13		fvex	$⊢ seq M ((F \circ 1^{st}), (Z \times \{A\})) (K) \in V$
14		fvex	$⊢ (Z \times \{A\}) (K + 1) \in V$
15	13 14	opco1i	$⊢ seq M ((F \circ 1^{st}), (Z \times \{A\})) (K) (F \circ 1^{st}) (Z \times \{A\}) (K + 1) = F (seq M ((F \circ 1^{st}), (Z \times \{A\})) (K))$
16	12 15	eqtr4i	$⊢ F (R (K)) = seq M ((F \circ 1^{st}), (Z \times \{A\})) (K) (F \circ 1^{st}) (Z \times \{A\}) (K + 1)$
17	9 10 16	3eqtr4g	$⊢ (φ \land K \in Z) \to R (K + 1) = F (R (K))$