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 ) )