caushft

Description: A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	caures.1	$⊢ Z = ℤ_{\geq M}$
	caures.3	$⊢ φ \to M \in ℤ$
	caures.4	$⊢ φ \to D \in Met (X)$
	caushft.4	$⊢ W = ℤ_{\geq (M + N)}$
	caushft.5	$⊢ φ \to N \in ℤ$
	caushft.7	$⊢ (φ \land k \in Z) \to F (k) = G (k + N)$
	caushft.8	$⊢ φ \to F \in Cau (D)$
	caushft.9	$⊢ φ \to G : W ⟶ X$
Assertion	caushft	$⊢ φ \to G \in Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		caures.1	$⊢ Z = ℤ_{\geq M}$
2		caures.3	$⊢ φ \to M \in ℤ$
3		caures.4	$⊢ φ \to D \in Met (X)$
4		caushft.4	$⊢ W = ℤ_{\geq (M + N)}$
5		caushft.5	$⊢ φ \to N \in ℤ$
6		caushft.7	$⊢ (φ \land k \in Z) \to F (k) = G (k + N)$
7		caushft.8	$⊢ φ \to F \in Cau (D)$
8		caushft.9	$⊢ φ \to G : W ⟶ X$
9		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
10	3 9	syl	$⊢ φ \to D \in ∞Met (X)$
11	6	ralrimiva	$⊢ φ \to \forall k \in Z F (k) = G (k + N)$
12		fveq2	$⊢ k = j \to F (k) = F (j)$
13		fvoveq1	$⊢ k = j \to G (k + N) = G (j + N)$
14	12 13	eqeq12d	$⊢ k = j \to (F (k) = G (k + N) \leftrightarrow F (j) = G (j + N))$
15	14	rspccva	$⊢ (\forall k \in Z F (k) = G (k + N) \land j \in Z) \to F (j) = G (j + N)$
16	11 15	sylan	$⊢ (φ \land j \in Z) \to F (j) = G (j + N)$
17	1 10 2 6 16	iscau4	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x)))$
18	7 17	mpbid	$⊢ φ \to (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x))$
19	18	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x)$
20	1	eleq2i	$⊢ j \in Z \leftrightarrow j \in ℤ_{\geq M}$
21	20	biimpi	$⊢ j \in Z \to j \in ℤ_{\geq M}$
22		eluzadd	$⊢ (j \in ℤ_{\geq M} \land N \in ℤ) \to j + N \in ℤ_{\geq (M + N)}$
23	21 5 22	syl2anr	$⊢ (φ \land j \in Z) \to j + N \in ℤ_{\geq (M + N)}$
24	23 4	eleqtrrdi	$⊢ (φ \land j \in Z) \to j + N \in W$
25		simplr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to j \in Z$
26	25 1	eleqtrdi	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to j \in ℤ_{\geq M}$
27		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
28	26 27	syl	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to j \in ℤ$
29	5	ad2antrr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to N \in ℤ$
30		simpr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to m \in ℤ_{\geq (j + N)}$
31		eluzsub	$⊢ (j \in ℤ \land N \in ℤ \land m \in ℤ_{\geq (j + N)}) \to m - N \in ℤ_{\geq j}$
32	28 29 30 31	syl3anc	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to m - N \in ℤ_{\geq j}$
33		simp3	$⊢ (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to G (k + N) D G (j + N) < x$
34	33	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to \forall k \in ℤ_{\geq j} G (k + N) D G (j + N) < x$
35		fvoveq1	$⊢ k = m - N \to G (k + N) = G (m - N + N)$
36	35	oveq1d	$⊢ k = m - N \to G (k + N) D G (j + N) = G (m - N + N) D G (j + N)$
37	36	breq1d	$⊢ k = m - N \to (G (k + N) D G (j + N) < x \leftrightarrow G (m - N + N) D G (j + N) < x)$
38	37	rspcv	$⊢ m - N \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} G (k + N) D G (j + N) < x \to G (m - N + N) D G (j + N) < x)$
39	32 34 38	syl2im	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to G (m - N + N) D G (j + N) < x)$
40		eluzelz	$⊢ m \in ℤ_{\geq (j + N)} \to m \in ℤ$
41	40	adantl	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to m \in ℤ$
42	41	zcnd	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to m \in ℂ$
43	5	zcnd	$⊢ φ \to N \in ℂ$
44	43	ad2antrr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to N \in ℂ$
45	42 44	npcand	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to m - N + N = m$
46	45	fveq2d	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G (m - N + N) = G (m)$
47	46	oveq1d	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G (m - N + N) D G (j + N) = G (m) D G (j + N)$
48	3	ad2antrr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to D \in Met (X)$
49	8	ad2antrr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G : W ⟶ X$
50	4	uztrn2	$⊢ (j + N \in W \land m \in ℤ_{\geq (j + N)}) \to m \in W$
51	24 50	sylan	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to m \in W$
52	49 51	ffvelcdmd	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G (m) \in X$
53	8	adantr	$⊢ (φ \land j \in Z) \to G : W ⟶ X$
54	53 24	ffvelcdmd	$⊢ (φ \land j \in Z) \to G (j + N) \in X$
55	54	adantr	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G (j + N) \in X$
56		metsym	$⊢ (D \in Met (X) \land G (m) \in X \land G (j + N) \in X) \to G (m) D G (j + N) = G (j + N) D G (m)$
57	48 52 55 56	syl3anc	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G (m) D G (j + N) = G (j + N) D G (m)$
58	47 57	eqtrd	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to G (m - N + N) D G (j + N) = G (j + N) D G (m)$
59	58	breq1d	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to (G (m - N + N) D G (j + N) < x \leftrightarrow G (j + N) D G (m) < x)$
60	39 59	sylibd	$⊢ ((φ \land j \in Z) \land m \in ℤ_{\geq (j + N)}) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to G (j + N) D G (m) < x)$
61	60	ralrimdva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to \forall m \in ℤ_{\geq (j + N)} G (j + N) D G (m) < x)$
62		fveq2	$⊢ n = j + N \to ℤ_{\geq n} = ℤ_{\geq (j + N)}$
63		fveq2	$⊢ n = j + N \to G (n) = G (j + N)$
64	63	oveq1d	$⊢ n = j + N \to G (n) D G (m) = G (j + N) D G (m)$
65	64	breq1d	$⊢ n = j + N \to (G (n) D G (m) < x \leftrightarrow G (j + N) D G (m) < x)$
66	62 65	raleqbidv	$⊢ n = j + N \to (\forall m \in ℤ_{\geq n} G (n) D G (m) < x \leftrightarrow \forall m \in ℤ_{\geq (j + N)} G (j + N) D G (m) < x)$
67	66	rspcev	$⊢ (j + N \in W \land \forall m \in ℤ_{\geq (j + N)} G (j + N) D G (m) < x) \to \exists n \in W \forall m \in ℤ_{\geq n} G (n) D G (m) < x$
68	24 61 67	syl6an	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to \exists n \in W \forall m \in ℤ_{\geq n} G (n) D G (m) < x)$
69	68	rexlimdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to \exists n \in W \forall m \in ℤ_{\geq n} G (n) D G (m) < x)$
70	69	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land G (k + N) \in X \land G (k + N) D G (j + N) < x) \to \forall x \in ℝ^{+} \exists n \in W \forall m \in ℤ_{\geq n} G (n) D G (m) < x)$
71	19 70	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists n \in W \forall m \in ℤ_{\geq n} G (n) D G (m) < x$
72	2 5	zaddcld	$⊢ φ \to M + N \in ℤ$
73		eqidd	$⊢ (φ \land m \in W) \to G (m) = G (m)$
74		eqidd	$⊢ (φ \land n \in W) \to G (n) = G (n)$
75	4 10 72 73 74 8	iscauf	$⊢ φ \to (G \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists n \in W \forall m \in ℤ_{\geq n} G (n) D G (m) < x)$
76	71 75	mpbird	$⊢ φ \to G \in Cau (D)$

Metamath Proof Explorer

Theorem caushft

Proof