Metamath Proof Explorer


Theorem 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 = M
caures.3 φ M
caures.4 φ D Met X
caushft.4 W = M + N
caushft.5 φ N
caushft.7 φ k Z F k = G k + N
caushft.8 φ F Cau D
caushft.9 φ G : W X
Assertion caushft φ G Cau D

Proof

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