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

Metamath Proof Explorer

Theorem seqp1d

Description: Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by AV, 3-May-2024)

Ref Expression
Hypotheses seqp1d.1 ⊢ Z = ℤ ≥ M
seqp1d.2 ⊢ φ → N ∈ Z
seqp1d.3 ⊢ K = N + 1
seqp1d.4 ⊢ φ → seq M + ˙ F ⁡ N = A
seqp1d.5 ⊢ φ → F ⁡ K = B
Assertion seqp1d ⊢ φ → seq M + ˙ F ⁡ K = A + ˙ B

Proof

Step Hyp Ref Expression
1 seqp1d.1 ⊢ Z = ℤ ≥ M
2 seqp1d.2 ⊢ φ → N ∈ Z
3 seqp1d.3 ⊢ K = N + 1
4 seqp1d.4 ⊢ φ → seq M + ˙ F ⁡ N = A
5 seqp1d.5 ⊢ φ → F ⁡ K = B
6 3 fveq2i ⊢ seq M + ˙ F ⁡ K = seq M + ˙ F ⁡ N + 1
7 6 a1i ⊢ φ → seq M + ˙ F ⁡ K = seq M + ˙ F ⁡ N + 1
8 2 1 eleqtrdi ⊢ φ → N ∈ ℤ ≥ M
9 seqp1 ⊢ N ∈ ℤ ≥ M → seq M + ˙ F ⁡ N + 1 = seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1
10 8 9 syl ⊢ φ → seq M + ˙ F ⁡ N + 1 = seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1
11 3 fveq2i ⊢ F ⁡ K = F ⁡ N + 1
12 11 5 eqtr3id ⊢ φ → F ⁡ N + 1 = B
13 4 12 oveq12d ⊢ φ → seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1 = A + ˙ B
14 7 10 13 3eqtrd ⊢ φ → seq M + ˙ F ⁡ K = A + ˙ B