Metamath Proof Explorer

Theorem seqf2

Description: Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step Hyp Ref Expression
1 seqcl2.1 
 |-  ( ph -> ( F ` M ) e. C )
2 seqcl2.2 
 |-  ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )
3 seqf2.3 
 |-  Z = ( ZZ>= ` M )
4 seqf2.4 
 |-  ( ph -> M e. ZZ )
5 seqf2.5 
 |-  ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. D )
6 seqfn 
 |-  ( M e. ZZ -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
7 4 6 syl 
 |-  ( ph -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
8 1 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` M ) e. C )
9 2 adantlr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )
10 simpr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. ( ZZ>= ` M ) )
11 elfzuz 
 |-  ( x e. ( ( M + 1 ) ... k ) -> x e. ( ZZ>= ` ( M + 1 ) ) )
12 11 5 sylan2 
 |-  ( ( ph /\ x e. ( ( M + 1 ) ... k ) ) -> ( F ` x ) e. D )
13 12 adantlr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ x e. ( ( M + 1 ) ... k ) ) -> ( F ` x ) e. D )
14 8 9 10 13 seqcl2 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , F ) ` k ) e. C )
15 14 ralrimiva 
 |-  ( ph -> A. k e. ( ZZ>= ` M ) ( seq M ( .+ , F ) ` k ) e. C )
16 ffnfv 
 |-  ( seq M ( .+ , F ) : ( ZZ>= ` M ) --> C <-> ( seq M ( .+ , F ) Fn ( ZZ>= ` M ) /\ A. k e. ( ZZ>= ` M ) ( seq M ( .+ , F ) ` k ) e. C ) )
17 7 15 16 sylanbrc 
 |-  ( ph -> seq M ( .+ , F ) : ( ZZ>= ` M ) --> C )
18 3 feq2i 
 |-  ( seq M ( .+ , F ) : Z --> C <-> seq M ( .+ , F ) : ( ZZ>= ` M ) --> C )
19 17 18 sylibr 
 |-  ( ph -> seq M ( .+ , F ) : Z --> C )