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 )