Theorem lgamucov2

Description: The U regions used in the proof of lgamgulm have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017)

	Ref	Expression
Hypotheses	lgamucov.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
	lgamucov.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
Assertion	lgamucov2	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lgamucov.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
2		lgamucov.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4	1 2 3	lgamucov	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑈 ) )
5	3	cnfldtop	⊢ ( TopOpen ‘ ℂfld ) ∈ Top
6	1	ssrab3	⊢ 𝑈 ⊆ ℂ
7		unicntop	⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
8	7	ntrss2	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑈 ⊆ ℂ ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑈 ) ⊆ 𝑈 )
9	5 6 8	mp2an	⊢ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑈 ) ⊆ 𝑈
10	9	sseli	⊢ ( 𝐴 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑈 ) → 𝐴 ∈ 𝑈 )
11	10	reximi	⊢ ( ∃ 𝑟 ∈ ℕ 𝐴 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑈 ) → ∃ 𝑟 ∈ ℕ 𝐴 ∈ 𝑈 )
12	4 11	syl	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ 𝑈 )