Metamath Proof Explorer

Theorem ulmi

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

Ref Expression
Hypotheses ulm2.z ⊢ Z = ℤ ≥ M
ulm2.m ⊢ φ → M ∈ ℤ
ulm2.f ⊢ φ → F : Z ⟶ ℂ S
ulm2.b ⊢ φ ∧ k ∈ Z ∧ z ∈ S → F ⁡ k ⁡ z = B
ulm2.a ⊢ φ ∧ z ∈ S → G ⁡ z = A
ulmi.u ⊢ φ → F ⇝u ⁡ S G
ulmi.c ⊢ φ → C ∈ ℝ +
Assertion ulmi ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ z ∈ S B − A < C

Proof

Step Hyp Ref Expression
1 ulm2.z ⊢ Z = ℤ ≥ M
2 ulm2.m ⊢ φ → M ∈ ℤ
3 ulm2.f ⊢ φ → F : Z ⟶ ℂ S
4 ulm2.b ⊢ φ ∧ k ∈ Z ∧ z ∈ S → F ⁡ k ⁡ z = B
5 ulm2.a ⊢ φ ∧ z ∈ S → G ⁡ z = A
6 ulmi.u ⊢ φ → F ⇝u ⁡ S G
7 ulmi.c ⊢ φ → C ∈ ℝ +
8 breq2 ⊢ x = C → B − A < x ↔ B − A < C
9 8 ralbidv ⊢ x = C → ∀ z ∈ S B − A < x ↔ ∀ z ∈ S B − A < C
10 9 rexralbidv ⊢ x = C → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ z ∈ S B − A < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ z ∈ S B − A < C
11 ulmcl ⊢ F ⇝u ⁡ S G → G : S ⟶ ℂ
12 6 11 syl ⊢ φ → G : S ⟶ ℂ
13 ulmscl ⊢ F ⇝u ⁡ S G → S ∈ V
14 6 13 syl ⊢ φ → S ∈ V
15 1 2 3 4 5 12 14 ulm2 ⊢ φ → F ⇝u ⁡ S G ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ z ∈ S B − A < x
16 6 15 mpbid ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ z ∈ S B − A < x
17 10 16 7 rspcdva ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ z ∈ S B − A < C