ulmshft

Description: A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015)

	Ref	Expression
Hypotheses	ulmshft.z	$⊢ Z = ℤ_{\geq M}$
	ulmshft.w	$⊢ W = ℤ_{\geq (M + K)}$
	ulmshft.m	$⊢ φ \to M \in ℤ$
	ulmshft.k	$⊢ φ \to K \in ℤ$
	ulmshft.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
	ulmshft.h	$⊢ φ \to H = (n \in W ⟼ F (n - K))$
Assertion	ulmshft	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow H \underset{u}{⇝} (S) G)$

Proof

Step	Hyp	Ref	Expression
1		ulmshft.z	$⊢ Z = ℤ_{\geq M}$
2		ulmshft.w	$⊢ W = ℤ_{\geq (M + K)}$
3		ulmshft.m	$⊢ φ \to M \in ℤ$
4		ulmshft.k	$⊢ φ \to K \in ℤ$
5		ulmshft.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
6		ulmshft.h	$⊢ φ \to H = (n \in W ⟼ F (n - K))$
7	1 2 3 4 5 6	ulmshftlem	$⊢ φ \to (F \underset{u}{⇝} (S) G \to H \underset{u}{⇝} (S) G)$
8		eqid	$⊢ ℤ_{\geq (M + K + (- K))} = ℤ_{\geq (M + K + (- K))}$
9	3 4	zaddcld	$⊢ φ \to M + K \in ℤ$
10	4	znegcld	$⊢ φ \to - K \in ℤ$
11	5	adantr	$⊢ (φ \land n \in W) \to F : Z ⟶ ℂ^{S}$
12	3	adantr	$⊢ (φ \land n \in W) \to M \in ℤ$
13	4	adantr	$⊢ (φ \land n \in W) \to K \in ℤ$
14		simpr	$⊢ (φ \land n \in W) \to n \in W$
15	14 2	eleqtrdi	$⊢ (φ \land n \in W) \to n \in ℤ_{\geq (M + K)}$
16		eluzsub	$⊢ (M \in ℤ \land K \in ℤ \land n \in ℤ_{\geq (M + K)}) \to n - K \in ℤ_{\geq M}$
17	12 13 15 16	syl3anc	$⊢ (φ \land n \in W) \to n - K \in ℤ_{\geq M}$
18	17 1	eleqtrrdi	$⊢ (φ \land n \in W) \to n - K \in Z$
19	11 18	ffvelcdmd	$⊢ (φ \land n \in W) \to F (n - K) \in (ℂ^{S})$
20	6 19	fmpt3d	$⊢ φ \to H : W ⟶ ℂ^{S}$
21		simpr	$⊢ (φ \land m \in Z) \to m \in Z$
22	21 1	eleqtrdi	$⊢ (φ \land m \in Z) \to m \in ℤ_{\geq M}$
23		eluzelz	$⊢ m \in ℤ_{\geq M} \to m \in ℤ$
24	22 23	syl	$⊢ (φ \land m \in Z) \to m \in ℤ$
25	24	zcnd	$⊢ (φ \land m \in Z) \to m \in ℂ$
26	4	zcnd	$⊢ φ \to K \in ℂ$
27	26	adantr	$⊢ (φ \land m \in Z) \to K \in ℂ$
28	25 27	subnegd	$⊢ (φ \land m \in Z) \to m - (- K) = m + K$
29	28	fveq2d	$⊢ (φ \land m \in Z) \to H (m - (- K)) = H (m + K)$
30	6	adantr	$⊢ (φ \land m \in Z) \to H = (n \in W ⟼ F (n - K))$
31	30	fveq1d	$⊢ (φ \land m \in Z) \to H (m + K) = (n \in W ⟼ F (n - K)) (m + K)$
32	4	adantr	$⊢ (φ \land m \in Z) \to K \in ℤ$
33		eluzadd	$⊢ (m \in ℤ_{\geq M} \land K \in ℤ) \to m + K \in ℤ_{\geq (M + K)}$
34	22 32 33	syl2anc	$⊢ (φ \land m \in Z) \to m + K \in ℤ_{\geq (M + K)}$
35	34 2	eleqtrrdi	$⊢ (φ \land m \in Z) \to m + K \in W$
36		fvoveq1	$⊢ n = m + K \to F (n - K) = F (m + K - K)$
37		eqid	$⊢ (n \in W ⟼ F (n - K)) = (n \in W ⟼ F (n - K))$
38		fvex	$⊢ F (m + K - K) \in V$
39	36 37 38	fvmpt	$⊢ m + K \in W \to (n \in W ⟼ F (n - K)) (m + K) = F (m + K - K)$
40	35 39	syl	$⊢ (φ \land m \in Z) \to (n \in W ⟼ F (n - K)) (m + K) = F (m + K - K)$
41	25 27	pncand	$⊢ (φ \land m \in Z) \to m + K - K = m$
42	41	fveq2d	$⊢ (φ \land m \in Z) \to F (m + K - K) = F (m)$
43	40 42	eqtrd	$⊢ (φ \land m \in Z) \to (n \in W ⟼ F (n - K)) (m + K) = F (m)$
44	29 31 43	3eqtrd	$⊢ (φ \land m \in Z) \to H (m - (- K)) = F (m)$
45	44	mpteq2dva	$⊢ φ \to (m \in Z ⟼ H (m - (- K))) = (m \in Z ⟼ F (m))$
46	3	zcnd	$⊢ φ \to M \in ℂ$
47	10	zcnd	$⊢ φ \to - K \in ℂ$
48	46 26 47	addassd	$⊢ φ \to M + K + (- K) = M + K + (- K)$
49	26	negidd	$⊢ φ \to K + (- K) = 0$
50	49	oveq2d	$⊢ φ \to M + K + (- K) = M + 0$
51	46	addridd	$⊢ φ \to M + 0 = M$
52	48 50 51	3eqtrd	$⊢ φ \to M + K + (- K) = M$
53	52	fveq2d	$⊢ φ \to ℤ_{\geq (M + K + (- K))} = ℤ_{\geq M}$
54	53 1	eqtr4di	$⊢ φ \to ℤ_{\geq (M + K + (- K))} = Z$
55	54	mpteq1d	$⊢ φ \to (m \in ℤ_{\geq (M + K + (- K))} ⟼ H (m - (- K))) = (m \in Z ⟼ H (m - (- K)))$
56	5	feqmptd	$⊢ φ \to F = (m \in Z ⟼ F (m))$
57	45 55 56	3eqtr4rd	$⊢ φ \to F = (m \in ℤ_{\geq (M + K + (- K))} ⟼ H (m - (- K)))$
58	2 8 9 10 20 57	ulmshftlem	$⊢ φ \to (H \underset{u}{⇝} (S) G \to F \underset{u}{⇝} (S) G)$
59	7 58	impbid	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow H \underset{u}{⇝} (S) G)$

Metamath Proof Explorer

Theorem ulmshft

Proof