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	|- ( ph -> N e. ( ZZ>= ` M ) )
	seqcl.2	|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
	seqcl.3	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
Assertion	seqcl	|- ( ph -> ( seq M ( .+ , F ) ` N ) e. S )

Proof

Step	Hyp	Ref	Expression
1		seqcl.1	|- ( ph -> N e. ( ZZ>= ` M ) )
2		seqcl.2	|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
3		seqcl.3	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
4		fveq2	|- ( x = M -> ( F ` x ) = ( F ` M ) )
5	4	eleq1d	|- ( x = M -> ( ( F ` x ) e. S <-> ( F ` M ) e. S ) )
6	2	ralrimiva	|- ( ph -> A. x e. ( M ... N ) ( F ` x ) e. S )
7		eluzfz1	|- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
8	1 7	syl	|- ( ph -> M e. ( M ... N ) )
9	5 6 8	rspcdva	|- ( ph -> ( F ` M ) e. S )
10		eluzel2	|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
11	1 10	syl	|- ( ph -> M e. ZZ )
12		fzp1ss	|- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
13	11 12	syl	|- ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
14	13	sselda	|- ( ( ph /\ x e. ( ( M + 1 ) ... N ) ) -> x e. ( M ... N ) )
15	14 2	syldan	|- ( ( ph /\ x e. ( ( M + 1 ) ... N ) ) -> ( F ` x ) e. S )
16	9 3 1 15	seqcl2	|- ( ph -> ( seq M ( .+ , F ) ` N ) e. S )