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 𝑁 ) ) ⇝ 𝐴 ) )