Metamath Proof Explorer

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 ⊢ φ → R ∈ ℕ
lgamgulm.u ⊢ U = x ∈ ℂ | x ≤ R ∧ ∀ k ∈ ℕ 0 1 R ≤ x + k
lgamgulm.g ⊢ G = m ∈ ℕ ⟼ z ∈ U ⟼ z ⁢ log ⁡ m + 1 m − log ⁡ z m + 1
Assertion lgamgulm ⊢ φ → seq 1 ∘ f ⁡ + G ∈ dom ⁡ ⇝u ⁡ U

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢ φ → R ∈ ℕ
2 lgamgulm.u ⊢ U = x ∈ ℂ | x ≤ R ∧ ∀ k ∈ ℕ 0 1 R ≤ x + k
3 lgamgulm.g ⊢ G = m ∈ ℕ ⟼ z ∈ U ⟼ z ⁢ log ⁡ m + 1 m − log ⁡ z m + 1
4 eqid ⊢ m ∈ ℕ ⟼ if 2 ⁢ R ≤ m R ⁢ 2 ⁢ R + 1 m 2 R ⁢ log ⁡ m + 1 m + log ⁡ R + 1 ⁢ m + π = m ∈ ℕ ⟼ if 2 ⁢ R ≤ m R ⁢ 2 ⁢ R + 1 m 2 R ⁢ log ⁡ m + 1 m + log ⁡ R + 1 ⁢ m + π
5 1 2 3 4 lgamgulmlem6 ⊢ φ → seq 1 ∘ f ⁡ + G ∈ dom ⁡ ⇝u ⁡ U ∧ seq 1 ∘ f ⁡ + G ⇝u ⁡ U z ∈ U ⟼ 1 → ∃ r ∈ ℝ ∀ z ∈ U 1 ≤ r
6 5 simpld ⊢ φ → seq 1 ∘ f ⁡ + G ∈ dom ⁡ ⇝u ⁡ U