Database
BASIC REAL AND COMPLEX FUNCTIONS
Sequences and series
Uniform convergence
ulmpm
Next ⟩
ulmf2
Metamath Proof Explorer
Ascii
Unicode
Theorem
ulmpm
Description:
Closure of a uniform limit of functions.
(Contributed by
Mario Carneiro
, 26-Feb-2015)
Ref
Expression
Assertion
ulmpm
⊢
F
⇝
u
⁡
S
G
→
F
∈
ℂ
S
↑
𝑝𝑚
ℤ
Proof
Step
Hyp
Ref
Expression
1
ulmf
⊢
F
⇝
u
⁡
S
G
→
∃
n
∈
ℤ
F
:
ℤ
≥
n
⟶
ℂ
S
2
uzssz
⊢
ℤ
≥
n
⊆
ℤ
3
ovex
⊢
ℂ
S
∈
V
4
zex
⊢
ℤ
∈
V
5
elpm2r
⊢
ℂ
S
∈
V
∧
ℤ
∈
V
∧
F
:
ℤ
≥
n
⟶
ℂ
S
∧
ℤ
≥
n
⊆
ℤ
→
F
∈
ℂ
S
↑
𝑝𝑚
ℤ
6
3
4
5
mpanl12
⊢
F
:
ℤ
≥
n
⟶
ℂ
S
∧
ℤ
≥
n
⊆
ℤ
→
F
∈
ℂ
S
↑
𝑝𝑚
ℤ
7
2
6
mpan2
⊢
F
:
ℤ
≥
n
⟶
ℂ
S
→
F
∈
ℂ
S
↑
𝑝𝑚
ℤ
8
7
rexlimivw
⊢
∃
n
∈
ℤ
F
:
ℤ
≥
n
⟶
ℂ
S
→
F
∈
ℂ
S
↑
𝑝𝑚
ℤ
9
1
8
syl
⊢
F
⇝
u
⁡
S
G
→
F
∈
ℂ
S
↑
𝑝𝑚
ℤ