Metamath Proof Explorer

Theorem caures

Description: The restriction of a Cauchy sequence to an upper set of integers 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 ) )
caures.5 
|- ( ph -> F e. ( X ^pm CC ) )
Assertion caures 
|- ( ph -> ( F e. ( Cau ` D ) <-> ( F |` Z ) 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 caures.5 
 |-  ( ph -> F e. ( X ^pm CC ) )
5 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
6 5 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
7 6 biantrurd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( k e. dom F <-> ( k e. Z /\ k e. dom F ) ) )
8 dmres 
 |-  dom ( F |` Z ) = ( Z i^i dom F )
9 8 elin2 
 |-  ( k e. dom ( F |` Z ) <-> ( k e. Z /\ k e. dom F ) )
10 7 9 bitr4di 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( k e. dom F <-> k e. dom ( F |` Z ) ) )
11 10 3anbi1d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
12 11 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
13 12 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
14 13 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
15 4 biantrurd 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
16 elfvdm 
 |-  ( D e. ( Met ` X ) -> X e. dom Met )
17 3 16 syl 
 |-  ( ph -> X e. dom Met )
18 cnex 
 |-  CC e. _V
19 ssid 
 |-  X C_ X
20 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
21 zsscn 
 |-  ZZ C_ CC
22 20 21 sstri 
 |-  ( ZZ>= ` M ) C_ CC
23 1 22 eqsstri 
 |-  Z C_ CC
24 pmss12g 
 |-  ( ( ( X C_ X /\ Z C_ CC ) /\ ( X e. dom Met /\ CC e. _V ) ) -> ( X ^pm Z ) C_ ( X ^pm CC ) )
25 19 23 24 mpanl12 
 |-  ( ( X e. dom Met /\ CC e. _V ) -> ( X ^pm Z ) C_ ( X ^pm CC ) )
26 17 18 25 sylancl 
 |-  ( ph -> ( X ^pm Z ) C_ ( X ^pm CC ) )
27 1 fvexi 
 |-  Z e. _V
28 pmresg 
 |-  ( ( Z e. _V /\ F e. ( X ^pm CC ) ) -> ( F |` Z ) e. ( X ^pm Z ) )
29 27 4 28 sylancr 
 |-  ( ph -> ( F |` Z ) e. ( X ^pm Z ) )
30 26 29 sseldd 
 |-  ( ph -> ( F |` Z ) e. ( X ^pm CC ) )
31 30 biantrurd 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( ( F |` Z ) e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
32 14 15 31 3bitr3d 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) <-> ( ( F |` Z ) e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
33 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
34 3 33 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
35 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
36 eqidd 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) = ( F ` j ) )
37 1 34 2 35 36 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 /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
38 fvres 
 |-  ( k e. Z -> ( ( F |` Z ) ` k ) = ( F ` k ) )
39 38 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( F |` Z ) ` k ) = ( F ` k ) )
40 fvres 
 |-  ( j e. Z -> ( ( F |` Z ) ` j ) = ( F ` j ) )
41 40 adantl 
 |-  ( ( ph /\ j e. Z ) -> ( ( F |` Z ) ` j ) = ( F ` j ) )
42 1 34 2 39 41 iscau4 
 |-  ( ph -> ( ( F |` Z ) e. ( Cau ` D ) <-> ( ( F |` Z ) e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` Z ) /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
43 32 37 42 3bitr4d 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F |` Z ) e. ( Cau ` D ) ) )