This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 ∈ V
Assertion isershft ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ↔ seq ( 𝑀 + 𝑁 ) ( + , ( 𝐹 shift 𝑁 ) ) ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isershft.1 ⊢ 𝐹 ∈ V
2 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
3 1 seqshft ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq ( 𝑀 + 𝑁 ) ( + , ( 𝐹 shift 𝑁 ) ) = ( seq ( ( 𝑀 + 𝑁 ) − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) )
4 2 3 sylancom ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq ( 𝑀 + 𝑁 ) ( + , ( 𝐹 shift 𝑁 ) ) = ( seq ( ( 𝑀 + 𝑁 ) − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) )
5 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
6 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
8 5 6 7 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
9 8 seqeq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq ( ( 𝑀 + 𝑁 ) − 𝑁 ) ( + , 𝐹 ) = seq 𝑀 ( + , 𝐹 ) )
10 9 oveq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( seq ( ( 𝑀 + 𝑁 ) − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) = ( seq 𝑀 ( + , 𝐹 ) shift 𝑁 ) )
11 4 10 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq ( 𝑀 + 𝑁 ) ( + , ( 𝐹 shift 𝑁 ) ) = ( seq 𝑀 ( + , 𝐹 ) shift 𝑁 ) )
12 11 breq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( seq ( 𝑀 + 𝑁 ) ( + , ( 𝐹 shift 𝑁 ) ) ⇝ 𝐴 ↔ ( seq 𝑀 ( + , 𝐹 ) shift 𝑁 ) ⇝ 𝐴 ) )
13 seqex ⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
14 climshft ⊢ ( ( 𝑁 ∈ ℤ ∧ seq 𝑀 ( + , 𝐹 ) ∈ V ) → ( ( seq 𝑀 ( + , 𝐹 ) shift 𝑁 ) ⇝ 𝐴 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ) )
15 13 14 mpan2 ⊢ ( 𝑁 ∈ ℤ → ( ( seq 𝑀 ( + , 𝐹 ) shift 𝑁 ) ⇝ 𝐴 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ) )
16 15 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( seq 𝑀 ( + , 𝐹 ) shift 𝑁 ) ⇝ 𝐴 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ) )
17 12 16 bitr2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ↔ seq ( 𝑀 + 𝑁 ) ( + , ( 𝐹 shift 𝑁 ) ) ⇝ 𝐴 ) )