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	$$⊢U=\left\{x\in ℂ|\left(\left|x\right|\le r\wedge \forall k\in {\mathbb{N}}_0\frac{1}{r}\le \left|x+k\right|\right)\right\}$$
	lgamucov.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
Assertion	lgamucov2	$$⊢\phi \to \exists r\in \mathbb{N}A\in U$$

Proof

Step	Hyp	Ref	Expression
1		lgamucov.u	$$⊢U=\left\{x\in ℂ|\left(\left|x\right|\le r\wedge \forall k\in {\mathbb{N}}_0\frac{1}{r}\le \left|x+k\right|\right)\right\}$$
2		lgamucov.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
3		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	1 2 3	lgamucov	$$⊢\phi \to \exists r\in \mathbb{N}A\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(U\right)$$
5	3	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
6	1	ssrab3	$$⊢U\subseteq ℂ$$
7		unicntop	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	7	ntrss2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge U\subseteq ℂ\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(U\right)\subseteq U$$
9	5 6 8	mp2an	$$⊢\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(U\right)\subseteq U$$
10	9	sseli	$$⊢A\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(U\right)\to A\in U$$
11	10	reximi	$$⊢\exists r\in \mathbb{N}A\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(U\right)\to \exists r\in \mathbb{N}A\in U$$
12	4 11	syl	$$⊢\phi \to \exists r\in \mathbb{N}A\in U$$