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

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 = ℤ ≥ M
algrf.2 ⊢ R = seq M F ∘ 1 st Z × A
algrf.3 ⊢ φ → M ∈ ℤ
algrf.4 ⊢ φ → A ∈ S
algrf.5 ⊢ φ → F : S ⟶ S
Assertion algrp1 ⊢ φ ∧ K ∈ Z → R ⁡ K + 1 = F ⁡ R ⁡ K

Proof

Step Hyp Ref Expression
1 algrf.1 ⊢ Z = ℤ ≥ M
2 algrf.2 ⊢ R = seq M F ∘ 1 st Z × A
3 algrf.3 ⊢ φ → M ∈ ℤ
4 algrf.4 ⊢ φ → A ∈ S
5 algrf.5 ⊢ φ → F : S ⟶ S
6 simpr ⊢ φ ∧ K ∈ Z → K ∈ Z
7 6 1 eleqtrdi ⊢ φ ∧ K ∈ Z → K ∈ ℤ ≥ M
8 seqp1 ⊢ K ∈ ℤ ≥ M → seq M F ∘ 1 st Z × A ⁡ K + 1 = seq M F ∘ 1 st Z × A ⁡ K F ∘ 1 st Z × A ⁡ K + 1
9 7 8 syl ⊢ φ ∧ K ∈ Z → seq M F ∘ 1 st Z × A ⁡ K + 1 = seq M F ∘ 1 st Z × A ⁡ K F ∘ 1 st Z × A ⁡ K + 1
10 2 fveq1i ⊢ R ⁡ K + 1 = seq M F ∘ 1 st Z × A ⁡ K + 1
11 2 fveq1i ⊢ R ⁡ K = seq M F ∘ 1 st Z × A ⁡ K
12 11 fveq2i ⊢ F ⁡ R ⁡ K = F ⁡ seq M F ∘ 1 st Z × A ⁡ K
13 fvex ⊢ seq M F ∘ 1 st Z × A ⁡ K ∈ V
14 fvex ⊢ Z × A ⁡ K + 1 ∈ V
15 13 14 opco1i ⊢ seq M F ∘ 1 st Z × A ⁡ K F ∘ 1 st Z × A ⁡ K + 1 = F ⁡ seq M F ∘ 1 st Z × A ⁡ K
16 12 15 eqtr4i ⊢ F ⁡ R ⁡ K = seq M F ∘ 1 st Z × A ⁡ K F ∘ 1 st Z × A ⁡ K + 1
17 9 10 16 3eqtr4g ⊢ φ ∧ K ∈ Z → R ⁡ K + 1 = F ⁡ R ⁡ K