Metamath Proof Explorer

Theorem cvgcaule

Description: A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025)

Ref Expression
Hypotheses cvgcaule.1 
|- F/_ j F
cvgcaule.2 
|- F/_ k F
cvgcaule.3 
|- ( ph -> M e. Z )
cvgcaule.4 
|- ( ph -> F e. V )
cvgcaule.5 
|- Z = ( ZZ>= ` M )
cvgcaule.6 
|- ( ph -> F e. dom ~~> )
cvgcaule.7 
|- ( ph -> X e. RR+ )
Assertion cvgcaule 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X ) )

Proof

Step Hyp Ref Expression
1 cvgcaule.1 
 |-  F/_ j F
2 cvgcaule.2 
 |-  F/_ k F
3 cvgcaule.3 
 |-  ( ph -> M e. Z )
4 cvgcaule.4 
 |-  ( ph -> F e. V )
5 cvgcaule.5 
 |-  Z = ( ZZ>= ` M )
6 cvgcaule.6 
 |-  ( ph -> F e. dom ~~> )
7 cvgcaule.7 
 |-  ( ph -> X e. RR+ )
8 1 2 3 4 5 6 7 cvgcau 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) )
9 nfv 
 |-  F/ k ( X e. RR+ /\ j e. Z )
10 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X )
11 9 10 nfan 
 |-  F/ k ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) )
12 rspa 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) )
13 12 simpld 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
14 13 adantll 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
15 13 adantll 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
16 5 uzid3 
 |-  ( j e. Z -> j e. ( ZZ>= ` j ) )
17 nfcv 
 |-  F/_ k j
18 2 17 nffv 
 |-  F/_ k ( F ` j )
19 18 nfel1 
 |-  F/ k ( F ` j ) e. CC
20 nfcv 
 |-  F/_ k abs
21 nfcv 
 |-  F/_ k -
22 18 21 18 nfov 
 |-  F/_ k ( ( F ` j ) - ( F ` j ) )
23 20 22 nffv 
 |-  F/_ k ( abs ` ( ( F ` j ) - ( F ` j ) ) )
24 nfcv 
 |-  F/_ k <
25 nfcv 
 |-  F/_ k X
26 23 24 25 nfbr 
 |-  F/ k ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X
27 19 26 nfan 
 |-  F/ k ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X )
28 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
29 28 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) )
30 28 fvoveq1d 
 |-  ( k = j -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) = ( abs ` ( ( F ` j ) - ( F ` j ) ) ) )
31 30 breq1d 
 |-  ( k = j -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X <-> ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X ) )
32 29 31 anbi12d 
 |-  ( k = j -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) <-> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X ) ) )
33 27 32 rspc 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X ) ) )
34 16 33 syl 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X ) ) )
35 34 imp 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - ( F ` j ) ) ) < X ) )
36 35 simpld 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) -> ( F ` j ) e. CC )
37 36 adantr 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. CC )
38 15 37 subcld 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) - ( F ` j ) ) e. CC )
39 38 abscld 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) e. RR )
40 39 adantlll 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) e. RR )
41 simplll 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> X e. RR+ )
42 41 rpred 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> X e. RR )
43 12 adantll 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) )
44 43 simprd 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X )
45 40 42 44 ltled 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X )
46 14 45 jca 
 |-  ( ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X ) )
47 11 46 ralrimia 
 |-  ( ( ( X e. RR+ /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X ) )
48 47 ex 
 |-  ( ( X e. RR+ /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X ) ) )
49 48 reximdva 
 |-  ( X e. RR+ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X ) ) )
50 7 8 49 sylc 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) <_ X ) )