Metamath Proof Explorer


Theorem seqcl

Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqcl.1 φ N M
seqcl.2 φ x M N F x S
seqcl.3 φ x S y S x + ˙ y S
Assertion seqcl φ seq M + ˙ F N S

Proof

Step Hyp Ref Expression
1 seqcl.1 φ N M
2 seqcl.2 φ x M N F x S
3 seqcl.3 φ x S y S x + ˙ y S
4 fveq2 x = M F x = F M
5 4 eleq1d x = M F x S F M S
6 2 ralrimiva φ x M N F x S
7 eluzfz1 N M M M N
8 1 7 syl φ M M N
9 5 6 8 rspcdva φ F M S
10 eluzel2 N M M
11 1 10 syl φ M
12 fzp1ss M M + 1 N M N
13 11 12 syl φ M + 1 N M N
14 13 sselda φ x M + 1 N x M N
15 14 2 syldan φ x M + 1 N F x S
16 9 3 1 15 seqcl2 φ seq M + ˙ F N S