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 simpr 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq M ( + , F ) e. dom ~~> )
22 climdm 
 |-  ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
23 21 22 sylib 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
24 1 19 20 23 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 ) ) ) )
25 17 24 eqbrtrrd 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq N ( + , F ) ~~> ( ( ~~> ` seq M ( + , F ) ) - ( seq M ( + , F ) ` ( N - 1 ) ) ) )
26 climrel 
 |-  Rel ~~>
27 26 releldmi 
 |-  ( seq N ( + , F ) ~~> ( ( ~~> ` seq M ( + , F ) ) - ( seq M ( + , F ) ` ( N - 1 ) ) ) -> seq N ( + , F ) e. dom ~~> )
28 25 27 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq M ( + , F ) e. dom ~~> ) -> seq N ( + , F ) e. dom ~~> )
29 simpr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
30 29 1 eleqtrrdi 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N - 1 ) e. Z )
31 30 adantr 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> ( N - 1 ) e. Z )
32 simpll 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> ph )
33 32 3 sylan 
 |-  ( ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) /\ k e. Z ) -> ( F ` k ) e. CC )
34 32 16 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) = seq N ( + , F ) )
35 simpr 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq N ( + , F ) e. dom ~~> )
36 climdm 
 |-  ( seq N ( + , F ) e. dom ~~> <-> seq N ( + , F ) ~~> ( ~~> ` seq N ( + , F ) ) )
37 35 36 sylib 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq N ( + , F ) ~~> ( ~~> ` seq N ( + , F ) ) )
38 34 37 eqbrtrd 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( ~~> ` seq N ( + , F ) ) )
39 1 31 33 38 clim2ser2 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq M ( + , F ) ~~> ( ( ~~> ` seq N ( + , F ) ) + ( seq M ( + , F ) ` ( N - 1 ) ) ) )
40 26 releldmi 
 |-  ( seq M ( + , F ) ~~> ( ( ~~> ` seq N ( + , F ) ) + ( seq M ( + , F ) ` ( N - 1 ) ) ) -> seq M ( + , F ) e. dom ~~> )
41 39 40 syl 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ seq N ( + , F ) e. dom ~~> ) -> seq M ( + , F ) e. dom ~~> )
42 28 41 impbida 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
43 42 ex 
 |-  ( ph -> ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) ) )
44 uzm1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
45 9 44 syl 
 |-  ( ph -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
46 7 43 45 mpjaod 
 |-  ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )