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

Metamath Proof Explorer

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 )