Metamath Proof Explorer

Theorem isershft

Description: Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013) (Revised by Mario Carneiro, 5-Nov-2013)

Ref Expression
Hypothesis isershft.1 
|- F e. _V
Assertion isershft 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( seq M ( .+ , F ) ~~> A <-> seq ( M + N ) ( .+ , ( F shift N ) ) ~~> A ) )

Proof

Step Hyp Ref Expression
1 isershft.1 
 |-  F e. _V
2 zaddcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
3 1 seqshft 
 |-  ( ( ( M + N ) e. ZZ /\ N e. ZZ ) -> seq ( M + N ) ( .+ , ( F shift N ) ) = ( seq ( ( M + N ) - N ) ( .+ , F ) shift N ) )
4 2 3 sylancom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq ( M + N ) ( .+ , ( F shift N ) ) = ( seq ( ( M + N ) - N ) ( .+ , F ) shift N ) )
5 zcn 
 |-  ( M e. ZZ -> M e. CC )
6 zcn 
 |-  ( N e. ZZ -> N e. CC )
7 pncan 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - N ) = M )
8 5 6 7 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + N ) - N ) = M )
9 8 seqeq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq ( ( M + N ) - N ) ( .+ , F ) = seq M ( .+ , F ) )
10 9 oveq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( seq ( ( M + N ) - N ) ( .+ , F ) shift N ) = ( seq M ( .+ , F ) shift N ) )
11 4 10 eqtrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq ( M + N ) ( .+ , ( F shift N ) ) = ( seq M ( .+ , F ) shift N ) )
12 11 breq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( seq ( M + N ) ( .+ , ( F shift N ) ) ~~> A <-> ( seq M ( .+ , F ) shift N ) ~~> A ) )
13 seqex 
 |-  seq M ( .+ , F ) e. _V
14 climshft 
 |-  ( ( N e. ZZ /\ seq M ( .+ , F ) e. _V ) -> ( ( seq M ( .+ , F ) shift N ) ~~> A <-> seq M ( .+ , F ) ~~> A ) )
15 13 14 mpan2 
 |-  ( N e. ZZ -> ( ( seq M ( .+ , F ) shift N ) ~~> A <-> seq M ( .+ , F ) ~~> A ) )
16 15 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( seq M ( .+ , F ) shift N ) ~~> A <-> seq M ( .+ , F ) ~~> A ) )
17 12 16 bitr2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( seq M ( .+ , F ) ~~> A <-> seq ( M + N ) ( .+ , ( F shift N ) ) ~~> A ) )