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 ∈ ℤ → seq M + ˙ F ⇝ A ↔ seq M + N + ˙ F shift N ⇝ A

Proof

Step Hyp Ref Expression
1 isershft.1 ⊢ F ∈ V
2 zaddcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + N ∈ ℤ
3 1 seqshft ⊢ M + N ∈ ℤ ∧ N ∈ ℤ → seq M + N + ˙ F shift N = seq M + N - N + ˙ F shift N
4 2 3 sylancom ⊢ M ∈ ℤ ∧ N ∈ ℤ → seq M + N + ˙ F shift N = seq M + N - N + ˙ F shift N
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 ∈ ℤ → seq M + N - N + ˙ F = seq M + ˙ F
10 9 oveq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ → seq M + N - N + ˙ F shift N = seq M + ˙ F shift N
11 4 10 eqtrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → seq M + N + ˙ F shift N = seq M + ˙ F shift N
12 11 breq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ → seq M + N + ˙ F shift N ⇝ A ↔ seq M + ˙ F shift N ⇝ A
13 seqex ⊢ seq M + ˙ F ∈ V
14 climshft ⊢ N ∈ ℤ ∧ seq M + ˙ F ∈ V → seq M + ˙ F shift N ⇝ A ↔ seq M + ˙ F ⇝ A
15 13 14 mpan2 ⊢ N ∈ ℤ → seq M + ˙ F shift N ⇝ A ↔ seq M + ˙ F ⇝ A
16 15 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ → seq M + ˙ F shift N ⇝ A ↔ seq M + ˙ F ⇝ A
17 12 16 bitr2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → seq M + ˙ F ⇝ A ↔ seq M + N + ˙ F shift N ⇝ A