Metamath Proof Explorer

Theorem iserex

Description: An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 27-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 iserex.2 
 |-  ( ph -> N e. Z )
3 iserex.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4 seqeq1 
 |-  ( N = M -> seq N ( + , F ) = seq M ( + , F ) )
5 4 eleq1d 
 |-  ( N = M -> ( seq N ( + , F ) e. dom ~~> <-> seq M ( + , F ) e. dom ~~> ) )
6 5 bicomd 
 |-  ( N = M -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
7 6 a1i 
 |-  ( ph -> ( N = M -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) ) )
8 simpll 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> ph )
9 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
10 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
11 9 10 syl 
 |-  ( ph -> N e. ZZ )
12 11 zcnd 
 |-  ( ph -> N e. CC )
13 ax-1cn 
 |-  1 e. CC
14 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
15 12 13 14 sylancl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
16 15 seqeq1d 
 |-  ( ph -> seq ( ( N - 1 ) + 1 ) ( + , F ) = seq N ( + , F ) )
17 8 16 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) = seq N ( + , F ) )
18 simplr 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
19 18 1 eleqtrrdi 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> ( N - 1 ) e. Z )
20 8 3 sylan 
 |-  ( ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) /\ k e. Z ) -> ( F ` k ) e. CC )
21 climdm 
 |-  ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
22 21 bilani 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
23 1 19 20 22 clim2ser 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( ( ~~> ` seq M ( + , F ) ) - ( seq M ( + , F ) ` ( N - 1 ) ) ) )
24 17 23 eqbrtrrd 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq N ( + , F ) ~~> ( ( ~~> ` seq M ( + , F ) ) - ( seq M ( + , F ) ` ( N - 1 ) ) ) )
25 climrel 
 |-  Rel ~~>
26 25 releldmi 
 |-  ( seq N ( + , F ) ~~> ( ( ~~> ` seq M ( + , F ) ) - ( seq M ( + , F ) ` ( N - 1 ) ) ) -> seq N ( + , F ) e. dom ~~> )
27 24 26 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq N ( + , F ) e. dom ~~> )
28 simpr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
29 28 1 eleqtrrdi 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N - 1 ) e. Z )
30 29 adantr 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> ( N - 1 ) e. Z )
31 simpll 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> ph )
32 31 3 sylan 
 |-  ( ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) /\ k e. Z ) -> ( F ` k ) e. CC )
33 31 16 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) = seq N ( + , F ) )
34 climdm 
 |-  ( seq N ( + , F ) e. dom ~~> <-> seq N ( + , F ) ~~> ( ~~> ` seq N ( + , F ) ) )
35 34 bilani 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq N ( + , F ) ~~> ( ~~> ` seq N ( + , F ) ) )
36 33 35 eqbrtrd 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( ~~> ` seq N ( + , F ) ) )
37 1 30 32 36 clim2ser2 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq M ( + , F ) ~~> ( ( ~~> ` seq N ( + , F ) ) + ( seq M ( + , F ) ` ( N - 1 ) ) ) )
38 25 releldmi 
 |-  ( seq M ( + , F ) ~~> ( ( ~~> ` seq N ( + , F ) ) + ( seq M ( + , F ) ` ( N - 1 ) ) ) -> seq M ( + , F ) e. dom ~~> )
39 37 38 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq M ( + , F ) e. dom ~~> )
40 27 39 impbida 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
41 40 ex 
 |-  ( ph -> ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) ) )
42 uzm1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
43 9 42 syl 
 |-  ( ph -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
44 7 41 43 mpjaod 
 |-  ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )