Metamath Proof Explorer

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 = { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) }
lgamucov.a 
|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
Assertion lgamucov2 
|- ( ph -> E. r e. NN A e. U )

Proof

Step Hyp Ref Expression
1 lgamucov.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) }
2 lgamucov.a 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 1 2 3 lgamucov 
 |-  ( ph -> E. r e. NN A e. ( ( int ` ( TopOpen ` CCfld ) ) ` U ) )
5 3 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
6 1 ssrab3 
 |-  U C_ CC
7 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
8 7 ntrss2 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ U C_ CC ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` U ) C_ U )
9 5 6 8 mp2an 
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` U ) C_ U
10 9 sseli 
 |-  ( A e. ( ( int ` ( TopOpen ` CCfld ) ) ` U ) -> A e. U )
11 10 reximi 
 |-  ( E. r e. NN A e. ( ( int ` ( TopOpen ` CCfld ) ) ` U ) -> E. r e. NN A e. U )
12 4 11 syl 
 |-  ( ph -> E. r e. NN A e. U )