Metamath Proof Explorer

Theorem seqcl2

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 seqcl2.1 
|- ( ph -> ( F ` M ) e. C )
seqcl2.2 
|- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )
seqcl2.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqcl2.4 
|- ( ( ph /\ x e. ( ( M + 1 ) ... N ) ) -> ( F ` x ) e. D )
Assertion seqcl2 
|- ( ph -> ( seq M ( .+ , F ) ` N ) e. 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 seqcl2.3 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 seqcl2.4 
 |-  ( ( ph /\ x e. ( ( M + 1 ) ... N ) ) -> ( F ` x ) e. D )
5 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
6 3 5 syl 
 |-  ( ph -> N e. ( M ... N ) )
7 eleq1 
 |-  ( x = M -> ( x e. ( M ... N ) <-> M e. ( M ... N ) ) )
8 fveq2 
 |-  ( x = M -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` M ) )
9 8 eleq1d 
 |-  ( x = M -> ( ( seq M ( .+ , F ) ` x ) e. C <-> ( seq M ( .+ , F ) ` M ) e. C ) )
10 7 9 imbi12d 
 |-  ( x = M -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) <-> ( M e. ( M ... N ) -> ( seq M ( .+ , F ) ` M ) e. C ) ) )
11 10 imbi2d 
 |-  ( x = M -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) ) <-> ( ph -> ( M e. ( M ... N ) -> ( seq M ( .+ , F ) ` M ) e. C ) ) ) )
12 eleq1 
 |-  ( x = n -> ( x e. ( M ... N ) <-> n e. ( M ... N ) ) )
13 fveq2 
 |-  ( x = n -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` n ) )
14 13 eleq1d 
 |-  ( x = n -> ( ( seq M ( .+ , F ) ` x ) e. C <-> ( seq M ( .+ , F ) ` n ) e. C ) )
15 12 14 imbi12d 
 |-  ( x = n -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) <-> ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) e. C ) ) )
16 15 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) ) <-> ( ph -> ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) e. C ) ) ) )
17 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( M ... N ) <-> ( n + 1 ) e. ( M ... N ) ) )
18 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) )
19 18 eleq1d 
 |-  ( x = ( n + 1 ) -> ( ( seq M ( .+ , F ) ` x ) e. C <-> ( seq M ( .+ , F ) ` ( n + 1 ) ) e. C ) )
20 17 19 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) <-> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) e. C ) ) )
21 20 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) ) <-> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) e. C ) ) ) )
22 eleq1 
 |-  ( x = N -> ( x e. ( M ... N ) <-> N e. ( M ... N ) ) )
23 fveq2 
 |-  ( x = N -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` N ) )
24 23 eleq1d 
 |-  ( x = N -> ( ( seq M ( .+ , F ) ` x ) e. C <-> ( seq M ( .+ , F ) ` N ) e. C ) )
25 22 24 imbi12d 
 |-  ( x = N -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) <-> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) e. C ) ) )
26 25 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) e. C ) ) <-> ( ph -> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) e. C ) ) ) )
27 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
28 27 eleq1d 
 |-  ( M e. ZZ -> ( ( seq M ( .+ , F ) ` M ) e. C <-> ( F ` M ) e. C ) )
29 1 28 syl5ibr 
 |-  ( M e. ZZ -> ( ph -> ( seq M ( .+ , F ) ` M ) e. C ) )
30 29 a1dd 
 |-  ( M e. ZZ -> ( ph -> ( M e. ( M ... N ) -> ( seq M ( .+ , F ) ` M ) e. C ) ) )
31 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) -> n e. ( M ... N ) )
32 31 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... N ) )
33 32 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n + 1 ) e. ( M ... N ) -> n e. ( M ... N ) ) )
34 33 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) e. C ) -> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) e. C ) ) )
35 fveq2 
 |-  ( x = ( n + 1 ) -> ( F ` x ) = ( F ` ( n + 1 ) ) )
36 35 eleq1d 
 |-  ( x = ( n + 1 ) -> ( ( F ` x ) e. D <-> ( F ` ( n + 1 ) ) e. D ) )
37 4 ralrimiva 
 |-  ( ph -> A. x e. ( ( M + 1 ) ... N ) ( F ` x ) e. D )
38 37 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. x e. ( ( M + 1 ) ... N ) ( F ` x ) e. D )
39 eluzp1p1 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
40 39 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
41 elfzuz3 
 |-  ( ( n + 1 ) e. ( M ... N ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
42 41 ad2antll 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
43 elfzuzb 
 |-  ( ( n + 1 ) e. ( ( M + 1 ) ... N ) <-> ( ( n + 1 ) e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ( ZZ>= ` ( n + 1 ) ) ) )
44 40 42 43 sylanbrc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + 1 ) e. ( ( M + 1 ) ... N ) )
45 36 38 44 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` ( n + 1 ) ) e. D )
46 2 caovclg 
 |-  ( ( ph /\ ( ( seq M ( .+ , F ) ` n ) e. C /\ ( F ` ( n + 1 ) ) e. D ) ) -> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) e. C )
47 46 ex 
 |-  ( ph -> ( ( ( seq M ( .+ , F ) ` n ) e. C /\ ( F ` ( n + 1 ) ) e. D ) -> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) e. C ) )
48 47 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( ( seq M ( .+ , F ) ` n ) e. C /\ ( F ` ( n + 1 ) ) e. D ) -> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) e. C ) )
49 45 48 mpan2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( seq M ( .+ , F ) ` n ) e. C -> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) e. C ) )
50 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
51 50 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
52 51 eleq1d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( seq M ( .+ , F ) ` ( n + 1 ) ) e. C <-> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) e. C ) )
53 49 52 sylibrd 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( seq M ( .+ , F ) ` n ) e. C -> ( seq M ( .+ , F ) ` ( n + 1 ) ) e. C ) )
54 34 53 animpimp2impd 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( ph -> ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) e. C ) ) -> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) e. C ) ) ) )
55 11 16 21 26 30 54 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) e. C ) ) )
56 3 55 mpcom 
 |-  ( ph -> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) e. C ) )
57 6 56 mpd 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) e. C )