Metamath Proof Explorer

Theorem cvgcau

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

Ref Expression
Hypotheses cvgcau.1 
|- F/_ j F
cvgcau.2 
|- F/_ k F
cvgcau.3 
|- ( ph -> M e. Z )
cvgcau.4 
|- ( ph -> F e. V )
cvgcau.5 
|- Z = ( ZZ>= ` M )
cvgcau.6 
|- ( ph -> F e. dom ~~> )
cvgcau.7 
|- ( ph -> X e. RR+ )
Assertion cvgcau 
|- ( 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 cvgcau.1 
 |-  F/_ j F
2 cvgcau.2 
 |-  F/_ k F
3 cvgcau.3 
 |-  ( ph -> M e. Z )
4 cvgcau.4 
 |-  ( ph -> F e. V )
5 cvgcau.5 
 |-  Z = ( ZZ>= ` M )
6 cvgcau.6 
 |-  ( ph -> F e. dom ~~> )
7 cvgcau.7 
 |-  ( ph -> X e. RR+ )
8 breq2 
 |-  ( x = X -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) )
9 8 anbi2d 
 |-  ( x = X -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) ) )
10 9 rexralbidv 
 |-  ( x = X -> ( 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 ) ) )
11 5 3 eluzelz2d 
 |-  ( ph -> M e. ZZ )
12 1 2 5 caucvgbf 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
13 11 4 12 syl2anc 
 |-  ( ph -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
14 6 13 mpbid 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
15 10 14 7 rspcdva 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < X ) )