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