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

Metamath Proof Explorer

Theorem seq1i

Description: Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypotheses seq1i.1 ⊢ M ∈ ℤ
seq1i.2 ⊢ φ → F ⁡ M = A
Assertion seq1i ⊢ φ → seq M + ˙ F ⁡ M = A

Proof

Step Hyp Ref Expression
1 seq1i.1 ⊢ M ∈ ℤ
2 seq1i.2 ⊢ φ → F ⁡ M = A
3 seq1 ⊢ M ∈ ℤ → seq M + ˙ F ⁡ M = F ⁡ M
4 1 3 ax-mp ⊢ seq M + ˙ F ⁡ M = F ⁡ M
5 4 2 eqtrid ⊢ φ → seq M + ˙ F ⁡ M = A