Metamath Proof Explorer

Theorem seqsplit

Description: Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqsplit.1 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqsplit.2 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqsplit.3 
|- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
seqsplit.4 
|- ( ph -> M e. ( ZZ>= ` K ) )
seqsplit.5 
|- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` x ) e. S )
Assertion seqsplit 
|- ( ph -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 seqsplit.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqsplit.2 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
3 seqsplit.3 
 |-  ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
4 seqsplit.4 
 |-  ( ph -> M e. ( ZZ>= ` K ) )
5 seqsplit.5 
 |-  ( ( ph /\ x e. ( K ... N ) ) -> ( F ` x ) e. S )
6 eluzfz2 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. ( ( M + 1 ) ... N ) )
7 3 6 syl 
 |-  ( ph -> N e. ( ( M + 1 ) ... N ) )
8 eleq1 
 |-  ( x = ( M + 1 ) -> ( x e. ( ( M + 1 ) ... N ) <-> ( M + 1 ) e. ( ( M + 1 ) ... N ) ) )
9 fveq2 
 |-  ( x = ( M + 1 ) -> ( seq K ( .+ , F ) ` x ) = ( seq K ( .+ , F ) ` ( M + 1 ) ) )
10 fveq2 
 |-  ( x = ( M + 1 ) -> ( seq ( M + 1 ) ( .+ , F ) ` x ) = ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) )
11 10 oveq2d 
 |-  ( x = ( M + 1 ) -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) )
12 9 11 eqeq12d 
 |-  ( x = ( M + 1 ) -> ( ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) <-> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) ) )
13 8 12 imbi12d 
 |-  ( x = ( M + 1 ) -> ( ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) <-> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) ) ) )
14 13 imbi2d 
 |-  ( x = ( M + 1 ) -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) ) <-> ( ph -> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) ) ) ) )
15 eleq1 
 |-  ( x = n -> ( x e. ( ( M + 1 ) ... N ) <-> n e. ( ( M + 1 ) ... N ) ) )
16 fveq2 
 |-  ( x = n -> ( seq K ( .+ , F ) ` x ) = ( seq K ( .+ , F ) ` n ) )
17 fveq2 
 |-  ( x = n -> ( seq ( M + 1 ) ( .+ , F ) ` x ) = ( seq ( M + 1 ) ( .+ , F ) ` n ) )
18 17 oveq2d 
 |-  ( x = n -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) )
19 16 18 eqeq12d 
 |-  ( x = n -> ( ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) <-> ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) ) )
20 15 19 imbi12d 
 |-  ( x = n -> ( ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) <-> ( n e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) ) ) )
21 20 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) ) <-> ( ph -> ( n e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) ) ) ) )
22 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( ( M + 1 ) ... N ) <-> ( n + 1 ) e. ( ( M + 1 ) ... N ) ) )
23 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq K ( .+ , F ) ` x ) = ( seq K ( .+ , F ) ` ( n + 1 ) ) )
24 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq ( M + 1 ) ( .+ , F ) ` x ) = ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) )
25 24 oveq2d 
 |-  ( x = ( n + 1 ) -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) )
26 23 25 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) <-> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) ) )
27 22 26 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) <-> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) ) ) )
28 27 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) ) ) ) )
29 eleq1 
 |-  ( x = N -> ( x e. ( ( M + 1 ) ... N ) <-> N e. ( ( M + 1 ) ... N ) ) )
30 fveq2 
 |-  ( x = N -> ( seq K ( .+ , F ) ` x ) = ( seq K ( .+ , F ) ` N ) )
31 fveq2 
 |-  ( x = N -> ( seq ( M + 1 ) ( .+ , F ) ` x ) = ( seq ( M + 1 ) ( .+ , F ) ` N ) )
32 31 oveq2d 
 |-  ( x = N -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )
33 30 32 eqeq12d 
 |-  ( x = N -> ( ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) <-> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) ) )
34 29 33 imbi12d 
 |-  ( x = N -> ( ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) <-> ( N e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) ) ) )
35 34 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` x ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` x ) ) ) ) <-> ( ph -> ( N e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) ) ) ) )
36 seqp1 
 |-  ( M e. ( ZZ>= ` K ) -> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( F ` ( M + 1 ) ) ) )
37 4 36 syl 
 |-  ( ph -> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( F ` ( M + 1 ) ) ) )
38 eluzel2 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( M + 1 ) e. ZZ )
39 seq1 
 |-  ( ( M + 1 ) e. ZZ -> ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) = ( F ` ( M + 1 ) ) )
40 3 38 39 3syl 
 |-  ( ph -> ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) = ( F ` ( M + 1 ) ) )
41 40 oveq2d 
 |-  ( ph -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( F ` ( M + 1 ) ) ) )
42 37 41 eqtr4d 
 |-  ( ph -> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) )
43 42 a1i13 
 |-  ( ( M + 1 ) e. ZZ -> ( ph -> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` ( M + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( M + 1 ) ) ) ) ) )
44 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> n e. ( ( M + 1 ) ... N ) )
45 44 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ( ( M + 1 ) ... N ) )
46 45 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> n e. ( ( M + 1 ) ... N ) ) )
47 46 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( n e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) ) -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) ) ) )
48 oveq1 
 |-  ( ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) -> ( ( seq K ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) .+ ( F ` ( n + 1 ) ) ) )
49 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ( ZZ>= ` ( M + 1 ) ) )
50 peano2uz 
 |-  ( M e. ( ZZ>= ` K ) -> ( M + 1 ) e. ( ZZ>= ` K ) )
51 4 50 syl 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` K ) )
52 51 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( M + 1 ) e. ( ZZ>= ` K ) )
53 uztrn 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( M + 1 ) e. ( ZZ>= ` K ) ) -> n e. ( ZZ>= ` K ) )
54 49 52 53 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ( ZZ>= ` K ) )
55 seqp1 
 |-  ( n e. ( ZZ>= ` K ) -> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
56 54 55 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
57 seqp1 
 |-  ( n e. ( ZZ>= ` ( M + 1 ) ) -> ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) = ( ( seq ( M + 1 ) ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
58 49 57 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) = ( ( seq ( M + 1 ) ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
59 58 oveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( ( seq ( M + 1 ) ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
60 simpl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ph )
61 eluzelz 
 |-  ( M e. ( ZZ>= ` K ) -> M e. ZZ )
62 4 61 syl 
 |-  ( ph -> M e. ZZ )
63 peano2uzr 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N e. ( ZZ>= ` M ) )
64 62 3 63 syl2anc 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
65 fzss2 
 |-  ( N e. ( ZZ>= ` M ) -> ( K ... M ) C_ ( K ... N ) )
66 64 65 syl 
 |-  ( ph -> ( K ... M ) C_ ( K ... N ) )
67 66 sselda 
 |-  ( ( ph /\ x e. ( K ... M ) ) -> x e. ( K ... N ) )
68 67 5 syldan 
 |-  ( ( ph /\ x e. ( K ... M ) ) -> ( F ` x ) e. S )
69 4 68 1 seqcl 
 |-  ( ph -> ( seq K ( .+ , F ) ` M ) e. S )
70 69 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( seq K ( .+ , F ) ` M ) e. S )
71 elfzuz3 
 |-  ( n e. ( ( M + 1 ) ... N ) -> N e. ( ZZ>= ` n ) )
72 fzss2 
 |-  ( N e. ( ZZ>= ` n ) -> ( ( M + 1 ) ... n ) C_ ( ( M + 1 ) ... N ) )
73 45 71 72 3syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( M + 1 ) ... n ) C_ ( ( M + 1 ) ... N ) )
74 fzss1 
 |-  ( ( M + 1 ) e. ( ZZ>= ` K ) -> ( ( M + 1 ) ... N ) C_ ( K ... N ) )
75 4 50 74 3syl 
 |-  ( ph -> ( ( M + 1 ) ... N ) C_ ( K ... N ) )
76 75 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( M + 1 ) ... N ) C_ ( K ... N ) )
77 73 76 sstrd 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( M + 1 ) ... n ) C_ ( K ... N ) )
78 77 sselda 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) /\ x e. ( ( M + 1 ) ... n ) ) -> x e. ( K ... N ) )
79 5 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) /\ x e. ( K ... N ) ) -> ( F ` x ) e. S )
80 78 79 syldan 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) /\ x e. ( ( M + 1 ) ... n ) ) -> ( F ` x ) e. S )
81 1 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
82 49 80 81 seqcl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( seq ( M + 1 ) ( .+ , F ) ` n ) e. S )
83 fveq2 
 |-  ( x = ( n + 1 ) -> ( F ` x ) = ( F ` ( n + 1 ) ) )
84 83 eleq1d 
 |-  ( x = ( n + 1 ) -> ( ( F ` x ) e. S <-> ( F ` ( n + 1 ) ) e. S ) )
85 5 ralrimiva 
 |-  ( ph -> A. x e. ( K ... N ) ( F ` x ) e. S )
86 85 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> A. x e. ( K ... N ) ( F ` x ) e. S )
87 simpr 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> ( n + 1 ) e. ( ( M + 1 ) ... N ) )
88 ssel2 
 |-  ( ( ( ( M + 1 ) ... N ) C_ ( K ... N ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> ( n + 1 ) e. ( K ... N ) )
89 75 87 88 syl2an 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( n + 1 ) e. ( K ... N ) )
90 84 86 89 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( F ` ( n + 1 ) ) e. S )
91 2 caovassg 
 |-  ( ( ph /\ ( ( seq K ( .+ , F ) ` M ) e. S /\ ( seq ( M + 1 ) ( .+ , F ) ` n ) e. S /\ ( F ` ( n + 1 ) ) e. S ) ) -> ( ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( ( seq ( M + 1 ) ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
92 60 70 82 90 91 syl13anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( ( seq ( M + 1 ) ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
93 59 92 eqtr4d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) = ( ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) .+ ( F ` ( n + 1 ) ) ) )
94 56 93 eqeq12d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) <-> ( ( seq K ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) .+ ( F ` ( n + 1 ) ) ) ) )
95 48 94 imbitrrid 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) -> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) ) )
96 47 95 animpimp2impd 
 |-  ( n e. ( ZZ>= ` ( M + 1 ) ) -> ( ( ph -> ( n e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` n ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` n ) ) ) ) -> ( ph -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` ( n + 1 ) ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` ( n + 1 ) ) ) ) ) ) )
97 14 21 28 35 43 96 uzind4 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( ph -> ( N e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) ) ) )
98 3 97 mpcom 
 |-  ( ph -> ( N e. ( ( M + 1 ) ... N ) -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) ) )
99 7 98 mpd 
 |-  ( ph -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )