seqshft

Description: Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-Feb-2014)

		Ref	Expression
	Hypothesis	seqshft.1	$⊢ F \in V$
	Assertion	seqshft	$⊢ (M \in ℤ \land N \in ℤ) \to seq M (\underset{˙}{+}, (F shift N)) = seq (M - N) (\underset{˙}{+}, F) shift N$

Proof

Step	Hyp	Ref	Expression
1		seqshft.1	$⊢ F \in V$
2		seqfn	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, (F shift N)) Fn ℤ_{\geq M}$
3	2	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to seq M (\underset{˙}{+}, (F shift N)) Fn ℤ_{\geq M}$
4		zsubcl	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$
5		seqfn	$⊢ M - N \in ℤ \to seq (M - N) (\underset{˙}{+}, F) Fn ℤ_{\geq (M - N)}$
6	4 5	syl	$⊢ (M \in ℤ \land N \in ℤ) \to seq (M - N) (\underset{˙}{+}, F) Fn ℤ_{\geq (M - N)}$
7		zcn	$⊢ N \in ℤ \to N \in ℂ$
8	7	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℂ$
9		seqex	$⊢ seq (M - N) (\underset{˙}{+}, F) \in V$
10	9	shftfn	$⊢ (seq (M - N) (\underset{˙}{+}, F) Fn ℤ_{\geq (M - N)} \land N \in ℂ) \to (seq (M - N) (\underset{˙}{+}, F) shift N) Fn \{x \in ℂ \| x - N \in ℤ_{\geq (M - N)}\}$
11	6 8 10	syl2anc	$⊢ (M \in ℤ \land N \in ℤ) \to (seq (M - N) (\underset{˙}{+}, F) shift N) Fn \{x \in ℂ \| x - N \in ℤ_{\geq (M - N)}\}$
12		simpr	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℤ$
13		shftuz	$⊢ (N \in ℤ \land M - N \in ℤ) \to \{x \in ℂ \| x - N \in ℤ_{\geq (M - N)}\} = ℤ_{\geq (M - N + N)}$
14	12 4 13	syl2anc	$⊢ (M \in ℤ \land N \in ℤ) \to \{x \in ℂ \| x - N \in ℤ_{\geq (M - N)}\} = ℤ_{\geq (M - N + N)}$
15		zcn	$⊢ M \in ℤ \to M \in ℂ$
16		npcan	$⊢ (M \in ℂ \land N \in ℂ) \to M - N + N = M$
17	15 7 16	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to M - N + N = M$
18	17	fveq2d	$⊢ (M \in ℤ \land N \in ℤ) \to ℤ_{\geq (M - N + N)} = ℤ_{\geq M}$
19	14 18	eqtrd	$⊢ (M \in ℤ \land N \in ℤ) \to \{x \in ℂ \| x - N \in ℤ_{\geq (M - N)}\} = ℤ_{\geq M}$
20	19	fneq2d	$⊢ (M \in ℤ \land N \in ℤ) \to ((seq (M - N) (\underset{˙}{+}, F) shift N) Fn \{x \in ℂ \| x - N \in ℤ_{\geq (M - N)}\} \leftrightarrow (seq (M - N) (\underset{˙}{+}, F) shift N) Fn ℤ_{\geq M})$
21	11 20	mpbid	$⊢ (M \in ℤ \land N \in ℤ) \to (seq (M - N) (\underset{˙}{+}, F) shift N) Fn ℤ_{\geq M}$
22		negsub	$⊢ (M \in ℂ \land N \in ℂ) \to M + -N = M - N$
23	15 7 22	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to M + -N = M - N$
24	23	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to M + -N = M - N$
25	24	seqeq1d	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to seq (M + -N) (\underset{˙}{+}, F) = seq (M - N) (\underset{˙}{+}, F)$
26		eluzelcn	$⊢ z \in ℤ_{\geq M} \to z \in ℂ$
27		negsub	$⊢ (z \in ℂ \land N \in ℂ) \to z + -N = z - N$
28	26 8 27	syl2anr	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to z + -N = z - N$
29	25 28	fveq12d	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to seq (M + -N) (\underset{˙}{+}, F) (z + -N) = seq (M - N) (\underset{˙}{+}, F) (z - N)$
30		simpr	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to z \in ℤ_{\geq M}$
31		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
32	31	ad2antlr	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to - N \in ℤ$
33		elfzelz	$⊢ y \in (M \dots z) \to y \in ℤ$
34	33	zcnd	$⊢ y \in (M \dots z) \to y \in ℂ$
35	1	shftval	$⊢ (N \in ℂ \land y \in ℂ) \to (F shift N) (y) = F (y - N)$
36		negsub	$⊢ (y \in ℂ \land N \in ℂ) \to y + -N = y - N$
37	36	ancoms	$⊢ (N \in ℂ \land y \in ℂ) \to y + -N = y - N$
38	37	fveq2d	$⊢ (N \in ℂ \land y \in ℂ) \to F (y + -N) = F (y - N)$
39	35 38	eqtr4d	$⊢ (N \in ℂ \land y \in ℂ) \to (F shift N) (y) = F (y + -N)$
40	7 34 39	syl2an	$⊢ (N \in ℤ \land y \in (M \dots z)) \to (F shift N) (y) = F (y + -N)$
41	40	ad4ant24	$⊢ (((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \land y \in (M \dots z)) \to (F shift N) (y) = F (y + -N)$
42	30 32 41	seqshft2	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to seq M (\underset{˙}{+}, (F shift N)) (z) = seq (M + -N) (\underset{˙}{+}, F) (z + -N)$
43	9	shftval	$⊢ (N \in ℂ \land z \in ℂ) \to (seq (M - N) (\underset{˙}{+}, F) shift N) (z) = seq (M - N) (\underset{˙}{+}, F) (z - N)$
44	8 26 43	syl2an	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to (seq (M - N) (\underset{˙}{+}, F) shift N) (z) = seq (M - N) (\underset{˙}{+}, F) (z - N)$
45	29 42 44	3eqtr4d	$⊢ ((M \in ℤ \land N \in ℤ) \land z \in ℤ_{\geq M}) \to seq M (\underset{˙}{+}, (F shift N)) (z) = (seq (M - N) (\underset{˙}{+}, F) shift N) (z)$
46	3 21 45	eqfnfvd	$⊢ (M \in ℤ \land N \in ℤ) \to seq M (\underset{˙}{+}, (F shift N)) = seq (M - N) (\underset{˙}{+}, F) shift N$

Metamath Proof Explorer

Theorem seqshft

Proof