Metamath Proof Explorer


Theorem ulmcau2

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k , m the functions F ( k ) and F ( m ) are uniformly within x of each other on S . (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses ulmcau.z
|- Z = ( ZZ>= ` M )
ulmcau.m
|- ( ph -> M e. ZZ )
ulmcau.s
|- ( ph -> S e. V )
ulmcau.f
|- ( ph -> F : Z --> ( CC ^m S ) )
Assertion ulmcau2
|- ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 ulmcau.z
 |-  Z = ( ZZ>= ` M )
2 ulmcau.m
 |-  ( ph -> M e. ZZ )
3 ulmcau.s
 |-  ( ph -> S e. V )
4 ulmcau.f
 |-  ( ph -> F : Z --> ( CC ^m S ) )
5 1 2 3 4 ulmcau
 |-  ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
6 1 2 3 4 ulmcaulem
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
7 5 6 bitrd
 |-  ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )