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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulm2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulm2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulm2.b ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = 𝐵 )
ulm2.a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = 𝐴 )
ulmi.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
ulmi.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion ulmi ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐶 )

Proof

Step Hyp Ref Expression
1 ulm2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulm2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulm2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
4 ulm2.b ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = 𝐵 )
5 ulm2.a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = 𝐴 )
6 ulmi.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
7 ulmi.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
8 breq2 ⊢ ( 𝑥 = 𝐶 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐶 ) )
9 8 ralbidv ⊢ ( 𝑥 = 𝐶 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐶 ) )
10 9 rexralbidv ⊢ ( 𝑥 = 𝐶 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐶 ) )
11 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
12 6 11 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
13 ulmscl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝑆 ∈ V )
14 6 13 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
15 1 2 3 4 5 12 14 ulm2 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
16 6 15 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 )
17 10 16 7 rspcdva ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐶 )