seqshft2

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

	Ref	Expression
Hypotheses	seqshft2.1	$⊢ φ \to N \in ℤ_{\geq M}$
	seqshft2.2	$⊢ φ \to K \in ℤ$
	seqshft2.3	$⊢ (φ \land k \in (M \dots N)) \to F (k) = G (k + K)$
Assertion	seqshft2	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K)$

Proof

Step	Hyp	Ref	Expression
1		seqshft2.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		seqshft2.2	$⊢ φ \to K \in ℤ$
3		seqshft2.3	$⊢ (φ \land k \in (M \dots N)) \to F (k) = G (k + K)$
4		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
5	1 4	syl	$⊢ φ \to N \in (M \dots N)$
6		eleq1	$⊢ x = M \to (x \in (M \dots N) \leftrightarrow M \in (M \dots N))$
7		fveq2	$⊢ x = M \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (M)$
8		fvoveq1	$⊢ x = M \to seq (M + K) (\underset{˙}{+}, G) (x + K) = seq (M + K) (\underset{˙}{+}, G) (M + K)$
9	7 8	eqeq12d	$⊢ x = M \to (seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K) \leftrightarrow seq M (\underset{˙}{+}, F) (M) = seq (M + K) (\underset{˙}{+}, G) (M + K))$
10	6 9	imbi12d	$⊢ x = M \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K)) \leftrightarrow (M \in (M \dots N) \to seq M (\underset{˙}{+}, F) (M) = seq (M + K) (\underset{˙}{+}, G) (M + K)))$
11	10	imbi2d	$⊢ x = M \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K))) \leftrightarrow (φ \to (M \in (M \dots N) \to seq M (\underset{˙}{+}, F) (M) = seq (M + K) (\underset{˙}{+}, G) (M + K))))$
12		eleq1	$⊢ x = n \to (x \in (M \dots N) \leftrightarrow n \in (M \dots N))$
13		fveq2	$⊢ x = n \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n)$
14		fvoveq1	$⊢ x = n \to seq (M + K) (\underset{˙}{+}, G) (x + K) = seq (M + K) (\underset{˙}{+}, G) (n + K)$
15	13 14	eqeq12d	$⊢ x = n \to (seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K) \leftrightarrow seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K))$
16	12 15	imbi12d	$⊢ x = n \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K)) \leftrightarrow (n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K)))$
17	16	imbi2d	$⊢ x = n \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K))) \leftrightarrow (φ \to (n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K))))$
18		eleq1	$⊢ x = n + 1 \to (x \in (M \dots N) \leftrightarrow n + 1 \in (M \dots N))$
19		fveq2	$⊢ x = n + 1 \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n + 1)$
20		fvoveq1	$⊢ x = n + 1 \to seq (M + K) (\underset{˙}{+}, G) (x + K) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K)$
21	19 20	eqeq12d	$⊢ x = n + 1 \to (seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K) \leftrightarrow seq M (\underset{˙}{+}, F) (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K))$
22	18 21	imbi12d	$⊢ x = n + 1 \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K)) \leftrightarrow (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K)))$
23	22	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K))) \leftrightarrow (φ \to (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K))))$
24		eleq1	$⊢ x = N \to (x \in (M \dots N) \leftrightarrow N \in (M \dots N))$
25		fveq2	$⊢ x = N \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (N)$
26		fvoveq1	$⊢ x = N \to seq (M + K) (\underset{˙}{+}, G) (x + K) = seq (M + K) (\underset{˙}{+}, G) (N + K)$
27	25 26	eqeq12d	$⊢ x = N \to (seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K) \leftrightarrow seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K))$
28	24 27	imbi12d	$⊢ x = N \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K)) \leftrightarrow (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K)))$
29	28	imbi2d	$⊢ x = N \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq (M + K) (\underset{˙}{+}, G) (x + K))) \leftrightarrow (φ \to (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K))))$
30		fveq2	$⊢ k = M \to F (k) = F (M)$
31		fvoveq1	$⊢ k = M \to G (k + K) = G (M + K)$
32	30 31	eqeq12d	$⊢ k = M \to (F (k) = G (k + K) \leftrightarrow F (M) = G (M + K))$
33	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) = G (k + K)$
34		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
35	1 34	syl	$⊢ φ \to M \in (M \dots N)$
36	32 33 35	rspcdva	$⊢ φ \to F (M) = G (M + K)$
37		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
38	1 37	syl	$⊢ φ \to M \in ℤ$
39		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
40	38 39	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
41	38 2	zaddcld	$⊢ φ \to M + K \in ℤ$
42		seq1	$⊢ M + K \in ℤ \to seq (M + K) (\underset{˙}{+}, G) (M + K) = G (M + K)$
43	41 42	syl	$⊢ φ \to seq (M + K) (\underset{˙}{+}, G) (M + K) = G (M + K)$
44	36 40 43	3eqtr4d	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) = seq (M + K) (\underset{˙}{+}, G) (M + K)$
45	44	a1i13	$⊢ M \in ℤ \to (φ \to (M \in (M \dots N) \to seq M (\underset{˙}{+}, F) (M) = seq (M + K) (\underset{˙}{+}, G) (M + K)))$
46		peano2fzr	$⊢ (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
47	46	adantl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in (M \dots N)$
48	47	expr	$⊢ (φ \land n \in ℤ_{\geq M}) \to (n + 1 \in (M \dots N) \to n \in (M \dots N))$
49	48	imim1d	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K)) \to (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K)))$
50		oveq1	$⊢ seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K) \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} F (n + 1)$
51		simprl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in ℤ_{\geq M}$
52		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
53	51 52	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
54	2	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to K \in ℤ$
55		eluzadd	$⊢ (n \in ℤ_{\geq M} \land K \in ℤ) \to n + K \in ℤ_{\geq (M + K)}$
56	51 54 55	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + K \in ℤ_{\geq (M + K)}$
57		seqp1	$⊢ n + K \in ℤ_{\geq (M + K)} \to seq (M + K) (\underset{˙}{+}, G) (n + K + 1) = seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} G (n + K + 1)$
58	56 57	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to seq (M + K) (\underset{˙}{+}, G) (n + K + 1) = seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} G (n + K + 1)$
59		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
60	51 59	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in ℤ$
61		zcn	$⊢ n \in ℤ \to n \in ℂ$
62		zcn	$⊢ K \in ℤ \to K \in ℂ$
63		ax-1cn	$⊢ 1 \in ℂ$
64		add32	$⊢ (n \in ℂ \land 1 \in ℂ \land K \in ℂ) \to n + 1 + K = n + K + 1$
65	63 64	mp3an2	$⊢ (n \in ℂ \land K \in ℂ) \to n + 1 + K = n + K + 1$
66	61 62 65	syl2an	$⊢ (n \in ℤ \land K \in ℤ) \to n + 1 + K = n + K + 1$
67	60 54 66	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + 1 + K = n + K + 1$
68	67	fveq2d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to seq (M + K) (\underset{˙}{+}, G) (n + 1 + K) = seq (M + K) (\underset{˙}{+}, G) (n + K + 1)$
69		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
70		fvoveq1	$⊢ k = n + 1 \to G (k + K) = G (n + 1 + K)$
71	69 70	eqeq12d	$⊢ k = n + 1 \to (F (k) = G (k + K) \leftrightarrow F (n + 1) = G (n + 1 + K))$
72	33	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to \forall k \in (M \dots N) F (k) = G (k + K)$
73		simprr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + 1 \in (M \dots N)$
74	71 72 73	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n + 1) = G (n + 1 + K)$
75	67	fveq2d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to G (n + 1 + K) = G (n + K + 1)$
76	74 75	eqtrd	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n + 1) = G (n + K + 1)$
77	76	oveq2d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} F (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} G (n + K + 1)$
78	58 68 77	3eqtr4d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to seq (M + K) (\underset{˙}{+}, G) (n + 1 + K) = seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} F (n + 1)$
79	53 78	eqeq12d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to (seq M (\underset{˙}{+}, F) (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K) \leftrightarrow seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + K) \underset{˙}{+} F (n + 1))$
80	50 79	syl5ibr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to (seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K) \to seq M (\underset{˙}{+}, F) (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K))$
81	49 80	animpimp2impd	$⊢ n \in ℤ_{\geq M} \to ((φ \to (n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq (M + K) (\underset{˙}{+}, G) (n + K))) \to (φ \to (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) = seq (M + K) (\underset{˙}{+}, G) (n + 1 + K))))$
82	11 17 23 29 45 81	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K)))$
83	1 82	mpcom	$⊢ φ \to (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K))$
84	5 83	mpd	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq (M + K) (\underset{˙}{+}, G) (N + K)$

Metamath Proof Explorer

Theorem seqshft2

Proof