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∈V
Assertion isershft ⊢M∈ℤ∧N∈ℤ→seqM+˙F⇝A↔seqM+N+˙FshiftN⇝A

Proof

Step Hyp Ref Expression
1 isershft.1 ⊢F∈V
2 zaddcl ⊢M∈ℤ∧N∈ℤ→M+N∈ℤ
3 1 seqshft ⊢M+N∈ℤ∧N∈ℤ→seqM+N+˙FshiftN=seqM+N-N+˙FshiftN
4 2 3 sylancom ⊢M∈ℤ∧N∈ℤ→seqM+N+˙FshiftN=seqM+N-N+˙FshiftN
5 zcn ⊢M∈ℤ→M∈ℂ
6 zcn ⊢N∈ℤ→N∈ℂ
7 pncan ⊢M∈ℂ∧N∈ℂ→M+N-N=M
8 5 6 7 syl2an ⊢M∈ℤ∧N∈ℤ→M+N-N=M
9 8 seqeq1d ⊢M∈ℤ∧N∈ℤ→seqM+N-N+˙F=seqM+˙F
10 9 oveq1d ⊢M∈ℤ∧N∈ℤ→seqM+N-N+˙FshiftN=seqM+˙FshiftN
11 4 10 eqtrd ⊢M∈ℤ∧N∈ℤ→seqM+N+˙FshiftN=seqM+˙FshiftN
12 11 breq1d ⊢M∈ℤ∧N∈ℤ→seqM+N+˙FshiftN⇝A↔seqM+˙FshiftN⇝A
13 seqex ⊢seqM+˙F∈V
14 climshft ⊢N∈ℤ∧seqM+˙F∈V→seqM+˙FshiftN⇝A↔seqM+˙F⇝A
15 13 14 mpan2 ⊢N∈ℤ→seqM+˙FshiftN⇝A↔seqM+˙F⇝A
16 15 adantl ⊢M∈ℤ∧N∈ℤ→seqM+˙FshiftN⇝A↔seqM+˙F⇝A
17 12 16 bitr2d ⊢M∈ℤ∧N∈ℤ→seqM+˙F⇝A↔seqM+N+˙FshiftN⇝A