Metamath Proof Explorer

Theorem clim2ser

Description: The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
clim2ser.2 
|- ( ph -> N e. Z )
clim2ser.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
clim2ser.5 
|- ( ph -> seq M ( + , F ) ~~> A )
Assertion clim2ser 
|- ( ph -> seq ( N + 1 ) ( + , F ) ~~> ( A - ( seq M ( + , F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 clim2ser.2 
 |-  ( ph -> N e. Z )
3 clim2ser.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4 clim2ser.5 
 |-  ( ph -> seq M ( + , F ) ~~> A )
5 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
6 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
7 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
8 6 7 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
9 eluzelz 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ZZ )
10 8 9 syl 
 |-  ( ph -> ( N + 1 ) e. ZZ )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 6 11 syl 
 |-  ( ph -> M e. ZZ )
13 1 12 3 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
14 13 2 ffvelrnd 
 |-  ( ph -> ( seq M ( + , F ) ` N ) e. CC )
15 seqex 
 |-  seq ( N + 1 ) ( + , F ) e. _V
16 15 a1i 
 |-  ( ph -> seq ( N + 1 ) ( + , F ) e. _V )
17 13 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> seq M ( + , F ) : Z --> CC )
18 8 1 eleqtrrdi 
 |-  ( ph -> ( N + 1 ) e. Z )
19 1 uztrn2 
 |-  ( ( ( N + 1 ) e. Z /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. Z )
20 18 19 sylan 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. Z )
21 17 20 ffvelrnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( + , F ) ` j ) e. CC )
22 addcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k + x ) e. CC )
23 22 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k + x ) e. CC )
24 addass 
 |-  ( ( k e. CC /\ x e. CC /\ y e. CC ) -> ( ( k + x ) + y ) = ( k + ( x + y ) ) )
25 24 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> ( ( k + x ) + y ) = ( k + ( x + y ) ) )
26 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. ( ZZ>= ` ( N + 1 ) ) )
27 6 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ( ZZ>= ` M ) )
28 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
29 28 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
30 29 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
31 30 adantlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
32 23 25 26 27 31 seqsplit 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( + , F ) ` j ) = ( ( seq M ( + , F ) ` N ) + ( seq ( N + 1 ) ( + , F ) ` j ) ) )
33 32 oveq1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( seq M ( + , F ) ` j ) - ( seq M ( + , F ) ` N ) ) = ( ( ( seq M ( + , F ) ` N ) + ( seq ( N + 1 ) ( + , F ) ` j ) ) - ( seq M ( + , F ) ` N ) ) )
34 14 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( + , F ) ` N ) e. CC )
35 1 uztrn2 
 |-  ( ( ( N + 1 ) e. Z /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
36 18 35 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
37 36 3 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` k ) e. CC )
38 5 10 37 serf 
 |-  ( ph -> seq ( N + 1 ) ( + , F ) : ( ZZ>= ` ( N + 1 ) ) --> CC )
39 38 ffvelrnda 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( + , F ) ` j ) e. CC )
40 34 39 pncan2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( seq M ( + , F ) ` N ) + ( seq ( N + 1 ) ( + , F ) ` j ) ) - ( seq M ( + , F ) ` N ) ) = ( seq ( N + 1 ) ( + , F ) ` j ) )
41 33 40 eqtr2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( + , F ) ` j ) = ( ( seq M ( + , F ) ` j ) - ( seq M ( + , F ) ` N ) ) )
42 5 10 4 14 16 21 41 climsubc1 
 |-  ( ph -> seq ( N + 1 ) ( + , F ) ~~> ( A - ( seq M ( + , F ) ` N ) ) )