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

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 
|- ( 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 )