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 = ( ZZ>= ` M )
caures.3 
|- ( ph -> M e. ZZ )
caures.4 
|- ( ph -> D e. ( Met ` X ) )
caushft.4 
|- W = ( ZZ>= ` ( M + N ) )
caushft.5 
|- ( ph -> N e. ZZ )
caushft.7 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` ( k + N ) ) )
caushft.8 
|- ( ph -> F e. ( Cau ` D ) )
caushft.9 
|- ( ph -> G : W --> X )
Assertion caushft 
|- ( ph -> G e. ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 caures.1 
 |-  Z = ( ZZ>= ` M )
2 caures.3 
 |-  ( ph -> M e. ZZ )
3 caures.4 
 |-  ( ph -> D e. ( Met ` X ) )
4 caushft.4 
 |-  W = ( ZZ>= ` ( M + N ) )
5 caushft.5 
 |-  ( ph -> N e. ZZ )
6 caushft.7 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` ( k + N ) ) )
7 caushft.8 
 |-  ( ph -> F e. ( Cau ` D ) )
8 caushft.9 
 |-  ( ph -> G : W --> X )
9 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
10 3 9 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
11 6 ralrimiva 
 |-  ( ph -> A. k e. 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 
 |-  ( ( A. k e. Z ( F ` k ) = ( G ` ( k + N ) ) /\ j e. Z ) -> ( F ` j ) = ( G ` ( j + N ) ) )
16 11 15 sylan 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` ( j + N ) ) )
17 1 10 2 6 16 iscau4 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) ) ) )
18 7 17 mpbid 
 |-  ( ph -> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) ) )
19 18 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) )
20 1 eleq2i 
 |-  ( j e. Z <-> j e. ( ZZ>= ` M ) )
21 20 biimpi 
 |-  ( j e. Z -> j e. ( ZZ>= ` M ) )
22 eluzadd 
 |-  ( ( j e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( j + N ) e. ( ZZ>= ` ( M + N ) ) )
23 21 5 22 syl2anr 
 |-  ( ( ph /\ j e. Z ) -> ( j + N ) e. ( ZZ>= ` ( M + N ) ) )
24 23 4 eleqtrrdi 
 |-  ( ( ph /\ j e. Z ) -> ( j + N ) e. W )
25 simplr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> j e. Z )
26 25 1 eleqtrdi 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> j e. ( ZZ>= ` M ) )
27 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
28 26 27 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> j e. ZZ )
29 5 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> N e. ZZ )
30 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. ( ZZ>= ` ( j + N ) ) )
31 eluzsub 
 |-  ( ( j e. ZZ /\ N e. ZZ /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( m - N ) e. ( ZZ>= ` j ) )
32 28 29 30 31 syl3anc 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( m - N ) e. ( ZZ>= ` j ) )
33 simp3 
 |-  ( ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x )
34 33 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> A. k e. ( ZZ>= ` 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 ) e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x ) )
39 32 34 38 syl2im 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x ) )
40 eluzelz 
 |-  ( m e. ( ZZ>= ` ( j + N ) ) -> m e. ZZ )
41 40 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. ZZ )
42 41 zcnd 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. CC )
43 5 zcnd 
 |-  ( ph -> N e. CC )
44 43 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> N e. CC )
45 42 44 npcand 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( m - N ) + N ) = m )
46 45 fveq2d 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( G ` ( ( m - N ) + N ) ) = ( G ` m ) )
47 46 oveq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) = ( ( G ` m ) D ( G ` ( j + N ) ) ) )
48 3 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> D e. ( Met ` X ) )
49 8 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> G : W --> X )
50 4 uztrn2 
 |-  ( ( ( j + N ) e. W /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. W )
51 24 50 sylan 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. W )
52 49 51 ffvelrnd 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( G ` m ) e. X )
53 8 adantr 
 |-  ( ( ph /\ j e. Z ) -> G : W --> X )
54 53 24 ffvelrnd 
 |-  ( ( ph /\ j e. Z ) -> ( G ` ( j + N ) ) e. X )
55 54 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( G ` ( j + N ) ) e. X )
56 metsym 
 |-  ( ( D e. ( Met ` X ) /\ ( G ` m ) e. X /\ ( G ` ( j + N ) ) e. X ) -> ( ( G ` m ) D ( G ` ( j + N ) ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) )
57 48 52 55 56 syl3anc 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( G ` m ) D ( G ` ( j + N ) ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) )
58 47 57 eqtrd 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) )
59 58 breq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x <-> ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) )
60 39 59 sylibd 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) )
61 60 ralrimdva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> A. m e. ( ZZ>= ` ( j + N ) ) ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) )
62 fveq2 
 |-  ( n = ( j + N ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( 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 ) -> ( A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x <-> A. m e. ( ZZ>= ` ( j + N ) ) ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) )
67 66 rspcev 
 |-  ( ( ( j + N ) e. W /\ A. m e. ( ZZ>= ` ( j + N ) ) ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) -> E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x )
68 24 61 67 syl6an 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) )
69 68 rexlimdva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) )
70 69 ralimdv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> A. x e. RR+ E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) )
71 19 70 mpd 
 |-  ( ph -> A. x e. RR+ E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x )
72 2 5 zaddcld 
 |-  ( ph -> ( M + N ) e. ZZ )
73 eqidd 
 |-  ( ( ph /\ m e. W ) -> ( G ` m ) = ( G ` m ) )
74 eqidd 
 |-  ( ( ph /\ n e. W ) -> ( G ` n ) = ( G ` n ) )
75 4 10 72 73 74 8 iscauf 
 |-  ( ph -> ( G e. ( Cau ` D ) <-> A. x e. RR+ E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) )
76 71 75 mpbird 
 |-  ( ph -> G e. ( Cau ` D ) )