This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmi

Description: The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015)

Ref Expression
Hypotheses ulm2.z 
|- Z = ( ZZ>= ` M )
ulm2.m 
|- ( ph -> M e. ZZ )
ulm2.f 
|- ( ph -> F : Z --> ( CC ^m S ) )
ulm2.b 
|- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = B )
ulm2.a 
|- ( ( ph /\ z e. S ) -> ( G ` z ) = A )
ulmi.u 
|- ( ph -> F ( ~~>u ` S ) G )
ulmi.c 
|- ( ph -> C e. RR+ )
Assertion ulmi 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < C )

Proof

Step Hyp Ref Expression
1 ulm2.z 
 |-  Z = ( ZZ>= ` M )
2 ulm2.m 
 |-  ( ph -> M e. ZZ )
3 ulm2.f 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
4 ulm2.b 
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = B )
5 ulm2.a 
 |-  ( ( ph /\ z e. S ) -> ( G ` z ) = A )
6 ulmi.u 
 |-  ( ph -> F ( ~~>u ` S ) G )
7 ulmi.c 
 |-  ( ph -> C e. RR+ )
8 breq2 
 |-  ( x = C -> ( ( abs ` ( B - A ) ) < x <-> ( abs ` ( B - A ) ) < C ) )
9 8 ralbidv 
 |-  ( x = C -> ( A. z e. S ( abs ` ( B - A ) ) < x <-> A. z e. S ( abs ` ( B - A ) ) < C ) )
10 9 rexralbidv 
 |-  ( x = C -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < C ) )
11 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
12 6 11 syl 
 |-  ( ph -> G : S --> CC )
13 ulmscl 
 |-  ( F ( ~~>u ` S ) G -> S e. _V )
14 6 13 syl 
 |-  ( ph -> S e. _V )
15 1 2 3 4 5 12 14 ulm2 
 |-  ( ph -> ( F ( ~~>u ` S ) G <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
16 6 15 mpbid 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x )
17 10 16 7 rspcdva 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < C )