ulmcau2

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k , m the functions F ( k ) and F ( m ) are uniformly within x of each other on S . (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	ulmcau.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	ulmcau.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	ulmcau.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	ulmcau.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑_m 𝑆 ) )
Assertion	ulmcau2	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ⇝_𝑢 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ulmcau.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		ulmcau.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		ulmcau.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		ulmcau.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑_m 𝑆 ) )
5	1 2 3 4	ulmcau	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ⇝_𝑢 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
6	1 2 3 4	ulmcaulem	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
7	5 6	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ⇝_𝑢 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )

Metamath Proof Explorer

Theorem ulmcau2

Proof