# Metamath Proof Explorer

## Theorem ulmi

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

Ref Expression
Hypotheses ulm2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
ulm2.m ${⊢}{\phi }\to {M}\in ℤ$
ulm2.f ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
ulm2.b ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge {z}\in {S}\right)\right)\to {F}\left({k}\right)\left({z}\right)={B}$
ulm2.a ${⊢}\left({\phi }\wedge {z}\in {S}\right)\to {G}\left({z}\right)={A}$
ulmi.u
ulmi.c ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
Assertion ulmi ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}$

### Proof

Step Hyp Ref Expression
1 ulm2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
2 ulm2.m ${⊢}{\phi }\to {M}\in ℤ$
3 ulm2.f ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
4 ulm2.b ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge {z}\in {S}\right)\right)\to {F}\left({k}\right)\left({z}\right)={B}$
5 ulm2.a ${⊢}\left({\phi }\wedge {z}\in {S}\right)\to {G}\left({z}\right)={A}$
6 ulmi.u
7 ulmi.c ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
8 breq2 ${⊢}{x}={C}\to \left(\left|{B}-{A}\right|<{x}↔\left|{B}-{A}\right|<{C}\right)$
9 8 ralbidv ${⊢}{x}={C}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{x}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}\right)$
10 9 rexralbidv ${⊢}{x}={C}\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{x}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}\right)$
11 ulmcl
12 6 11 syl ${⊢}{\phi }\to {G}:{S}⟶ℂ$
13 ulmscl
14 6 13 syl ${⊢}{\phi }\to {S}\in \mathrm{V}$
15 1 2 3 4 5 12 14 ulm2
16 6 15 mpbid ${⊢}{\phi }\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{x}$
17 10 16 7 rspcdva ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}$