Theorem lgamgulm

Description: The series G is uniformly convergent on the compact region U , which describes a circle of radius R with holes of size 1 / R around the poles of the gamma function. (Contributed by Mario Carneiro, 3-Jul-2017)

	Ref	Expression
Hypotheses	lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
	lgamgulm.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
Assertion	lgamgulm	⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) ∈ dom ( ⇝𝑢 ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2		lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3		lgamgulm.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
4		eqid	⊢ ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) ) = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
5	1 2 3 4	lgamgulmlem6	⊢ ( 𝜑 → ( seq 1 ( ∘f + , 𝐺 ) ∈ dom ( ⇝𝑢 ‘ 𝑈 ) ∧ ( seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 1 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 1 ) ≤ 𝑟 ) ) )
6	5	simpld	⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) ∈ dom ( ⇝𝑢 ‘ 𝑈 ) )