Theorem seqf

Description: Range of the recursive sequence builder (special case of seqf2 ). (Contributed by Mario Carneiro, 24-Jun-2013)

	Ref	Expression
Hypotheses	seqf.1	|- Z = ( ZZ>= ` M )
	seqf.2	|- ( ph -> M e. ZZ )
	seqf.3	|- ( ( ph /\ x e. Z ) -> ( F ` x ) e. S )
	seqf.4	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
Assertion	seqf	|- ( ph -> seq M ( .+ , F ) : Z --> S )

Proof

Step	Hyp	Ref	Expression
1		seqf.1	|- Z = ( ZZ>= ` M )
2		seqf.2	|- ( ph -> M e. ZZ )
3		seqf.3	|- ( ( ph /\ x e. Z ) -> ( F ` x ) e. S )
4		seqf.4	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
5		fveq2	|- ( x = M -> ( F ` x ) = ( F ` M ) )
6	5	eleq1d	|- ( x = M -> ( ( F ` x ) e. S <-> ( F ` M ) e. S ) )
7	3	ralrimiva	|- ( ph -> A. x e. Z ( F ` x ) e. S )
8		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
9	2 8	syl	|- ( ph -> M e. ( ZZ>= ` M ) )
10	9 1	eleqtrrdi	|- ( ph -> M e. Z )
11	6 7 10	rspcdva	|- ( ph -> ( F ` M ) e. S )
12		peano2uzr	|- ( ( M e. ZZ /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. ( ZZ>= ` M ) )
13	2 12	sylan	|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. ( ZZ>= ` M ) )
14	13 1	eleqtrrdi	|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. Z )
15	14 3	syldan	|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. S )
16	11 4 1 2 15	seqf2	|- ( ph -> seq M ( .+ , F ) : Z --> S )