Metamath Proof Explorer

Theorem lgamucov

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, 6-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 ) ) )
lgamucov.j 
|- J = ( TopOpen ` CCfld )
Assertion lgamucov 
|- ( ph -> E. r e. NN A e. ( ( int ` J ) ` 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 lgamucov.j 
 |-  J = ( TopOpen ` CCfld )
4 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
5 difss 
 |-  ( ZZ \ NN ) C_ ZZ
6 3 sszcld 
 |-  ( ( ZZ \ NN ) C_ ZZ -> ( ZZ \ NN ) e. ( Clsd ` J ) )
7 3 cnfldtopon 
 |-  J e. ( TopOn ` CC )
8 7 toponunii 
 |-  CC = U. J
9 8 cldopn 
 |-  ( ( ZZ \ NN ) e. ( Clsd ` J ) -> ( CC \ ( ZZ \ NN ) ) e. J )
10 5 6 9 mp2b 
 |-  ( CC \ ( ZZ \ NN ) ) e. J
11 10 a1i 
 |-  ( ph -> ( CC \ ( ZZ \ NN ) ) e. J )
12 3 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
13 12 mopni2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( CC \ ( ZZ \ NN ) ) e. J /\ A e. ( CC \ ( ZZ \ NN ) ) ) -> E. a e. RR+ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) )
14 4 11 2 13 mp3an2i 
 |-  ( ph -> E. a e. RR+ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) )
15 2 eldifad 
 |-  ( ph -> A e. CC )
16 15 adantr 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> A e. CC )
17 16 abscld 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> ( abs ` A ) e. RR )
18 simprl 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> a e. RR+ )
19 18 rpred 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> a e. RR )
20 17 19 readdcld 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> ( ( abs ` A ) + a ) e. RR )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> 2 e. RR )
23 22 18 rerpdivcld 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> ( 2 / a ) e. RR )
24 20 23 readdcld 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> ( ( ( abs ` A ) + a ) + ( 2 / a ) ) e. RR )
25 arch 
 |-  ( ( ( ( abs ` A ) + a ) + ( 2 / a ) ) e. RR -> E. r e. NN ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r )
26 24 25 syl 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> E. r e. NN ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r )
27 3 cnfldtop 
 |-  J e. Top
28 27 a1i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> J e. Top )
29 1 ssrab3 
 |-  U C_ CC
30 29 a1i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> U C_ CC )
31 16 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> A e. CC )
32 18 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> a e. RR+ )
33 32 rphalfcld 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> ( a / 2 ) e. RR+ )
34 33 rpxrd 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> ( a / 2 ) e. RR* )
35 12 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ ( a / 2 ) e. RR* ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) e. J )
36 4 31 34 35 mp3an2i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) e. J )
37 simplr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> x e. CC )
38 37 abscld 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` x ) e. RR )
39 simp-4r 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> r e. NN )
40 39 nnred 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> r e. RR )
41 24 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( ( abs ` A ) + a ) + ( 2 / a ) ) e. RR )
42 20 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` A ) + a ) e. RR )
43 17 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` A ) e. RR )
44 38 43 resubcld 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` x ) - ( abs ` A ) ) e. RR )
45 19 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> a e. RR )
46 45 rehalfcld 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( a / 2 ) e. RR )
47 31 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> A e. CC )
48 37 47 subcld 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( x - A ) e. CC )
49 48 abscld 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` ( x - A ) ) e. RR )
50 37 47 abs2difd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` x ) - ( abs ` A ) ) <_ ( abs ` ( x - A ) ) )
51 eqid 
 |-  ( abs o. - ) = ( abs o. - )
52 51 cnmetdval 
 |-  ( ( A e. CC /\ x e. CC ) -> ( A ( abs o. - ) x ) = ( abs ` ( A - x ) ) )
53 47 37 52 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( A ( abs o. - ) x ) = ( abs ` ( A - x ) ) )
54 47 37 abssubd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` ( A - x ) ) = ( abs ` ( x - A ) ) )
55 53 54 eqtrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( A ( abs o. - ) x ) = ( abs ` ( x - A ) ) )
56 simpr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( A ( abs o. - ) x ) < ( a / 2 ) )
57 55 56 eqbrtrrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` ( x - A ) ) < ( a / 2 ) )
58 44 49 46 50 57 lelttrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` x ) - ( abs ` A ) ) < ( a / 2 ) )
59 32 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> a e. RR+ )
60 rphalflt 
 |-  ( a e. RR+ -> ( a / 2 ) < a )
61 59 60 syl 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( a / 2 ) < a )
62 44 46 45 58 61 lttrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` x ) - ( abs ` A ) ) < a )
63 38 43 45 ltsubadd2d 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( ( abs ` x ) - ( abs ` A ) ) < a <-> ( abs ` x ) < ( ( abs ` A ) + a ) ) )
64 62 63 mpbid 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` x ) < ( ( abs ` A ) + a ) )
65 2rp 
 |-  2 e. RR+
66 65 a1i 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> 2 e. RR+ )
67 66 59 rpdivcld 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( 2 / a ) e. RR+ )
68 42 67 ltaddrpd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` A ) + a ) < ( ( ( abs ` A ) + a ) + ( 2 / a ) ) )
69 38 42 41 64 68 lttrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` x ) < ( ( ( abs ` A ) + a ) + ( 2 / a ) ) )
70 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r )
71 38 41 40 69 70 lttrd 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` x ) < r )
72 38 40 71 ltled 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( abs ` x ) <_ r )
73 39 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> r e. NN )
74 73 nnrecred 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 1 / r ) e. RR )
75 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> x e. CC )
76 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> k e. NN0 )
77 76 nn0cnd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> k e. CC )
78 75 77 addcld 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( x + k ) e. CC )
79 78 abscld 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( abs ` ( x + k ) ) e. RR )
80 46 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( a / 2 ) e. RR )
81 23 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 2 / a ) e. RR )
82 41 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( ( ( abs ` A ) + a ) + ( 2 / a ) ) e. RR )
83 40 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> r e. RR )
84 47 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> A e. CC )
85 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> A e. ( CC \ ( ZZ \ NN ) ) )
86 85 dmgmn0 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> A =/= 0 )
87 84 86 absrpcld 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( abs ` A ) e. RR+ )
88 59 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> a e. RR+ )
89 87 88 rpaddcld 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( ( abs ` A ) + a ) e. RR+ )
90 81 89 ltaddrp2d 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 2 / a ) < ( ( ( abs ` A ) + a ) + ( 2 / a ) ) )
91 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r )
92 81 82 83 90 91 lttrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 2 / a ) < r )
93 67 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 2 / a ) e. RR+ )
94 73 nnrpd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> r e. RR+ )
95 93 94 ltrecd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( ( 2 / a ) < r <-> ( 1 / r ) < ( 1 / ( 2 / a ) ) ) )
96 92 95 mpbid 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 1 / r ) < ( 1 / ( 2 / a ) ) )
97 2cnd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> 2 e. CC )
98 88 rpcnd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> a e. CC )
99 2ne0 
 |-  2 =/= 0
100 99 a1i 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> 2 =/= 0 )
101 88 rpne0d 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> a =/= 0 )
102 97 98 100 101 recdivd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 1 / ( 2 / a ) ) = ( a / 2 ) )
103 96 102 breqtrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 1 / r ) < ( a / 2 ) )
104 eldmgm 
 |-  ( -u k e. ( CC \ ( ZZ \ NN ) ) <-> ( -u k e. CC /\ -. -u -u k e. NN0 ) )
105 104 simprbi 
 |-  ( -u k e. ( CC \ ( ZZ \ NN ) ) -> -. -u -u k e. NN0 )
106 77 negnegd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> -u -u k = k )
107 106 76 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> -u -u k e. NN0 )
108 105 107 nsyl3 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> -. -u k e. ( CC \ ( ZZ \ NN ) ) )
109 4 a1i 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( abs o. - ) e. ( *Met ` CC ) )
110 34 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( a / 2 ) e. RR* )
111 77 negcld 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> -u k e. CC )
112 elbl2 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( a / 2 ) e. RR* ) /\ ( x e. CC /\ -u k e. CC ) ) -> ( -u k e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) <-> ( x ( abs o. - ) -u k ) < ( a / 2 ) ) )
113 109 110 75 111 112 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( -u k e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) <-> ( x ( abs o. - ) -u k ) < ( a / 2 ) ) )
114 51 cnmetdval 
 |-  ( ( x e. CC /\ -u k e. CC ) -> ( x ( abs o. - ) -u k ) = ( abs ` ( x - -u k ) ) )
115 75 111 114 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( x ( abs o. - ) -u k ) = ( abs ` ( x - -u k ) ) )
116 75 77 subnegd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( x - -u k ) = ( x + k ) )
117 116 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( abs ` ( x - -u k ) ) = ( abs ` ( x + k ) ) )
118 115 117 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( x ( abs o. - ) -u k ) = ( abs ` ( x + k ) ) )
119 118 breq1d 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( ( x ( abs o. - ) -u k ) < ( a / 2 ) <-> ( abs ` ( x + k ) ) < ( a / 2 ) ) )
120 79 80 ltnled 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( ( abs ` ( x + k ) ) < ( a / 2 ) <-> -. ( a / 2 ) <_ ( abs ` ( x + k ) ) ) )
121 113 119 120 3bitrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( -u k e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) <-> -. ( a / 2 ) <_ ( abs ` ( x + k ) ) ) )
122 45 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> a e. RR )
123 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( A ( abs o. - ) x ) < ( a / 2 ) )
124 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( a / 2 ) e. RR* ) /\ ( x e. CC /\ A e. CC ) ) -> ( A e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) <-> ( A ( abs o. - ) x ) < ( a / 2 ) ) )
125 109 110 75 84 124 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( A e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) <-> ( A ( abs o. - ) x ) < ( a / 2 ) ) )
126 123 125 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> A e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) )
127 blhalf 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ x e. CC ) /\ ( a e. RR /\ A e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) ) ) -> ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ ( A ( ball ` ( abs o. - ) ) a ) )
128 109 75 122 126 127 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ ( A ( ball ` ( abs o. - ) ) a ) )
129 simprr 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) )
130 129 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) )
131 128 130 sstrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ ( CC \ ( ZZ \ NN ) ) )
132 131 sseld 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( -u k e. ( x ( ball ` ( abs o. - ) ) ( a / 2 ) ) -> -u k e. ( CC \ ( ZZ \ NN ) ) ) )
133 121 132 sylbird 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( -. ( a / 2 ) <_ ( abs ` ( x + k ) ) -> -u k e. ( CC \ ( ZZ \ NN ) ) ) )
134 108 133 mt3d 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( a / 2 ) <_ ( abs ` ( x + k ) ) )
135 74 80 79 103 134 ltletrd 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 1 / r ) < ( abs ` ( x + k ) ) )
136 74 79 135 ltled 
 |-  ( ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) /\ k e. NN0 ) -> ( 1 / r ) <_ ( abs ` ( x + k ) ) )
137 136 ralrimiva 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) )
138 72 137 jca 
 |-  ( ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) /\ ( A ( abs o. - ) x ) < ( a / 2 ) ) -> ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) )
139 138 ex 
 |-  ( ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) /\ x e. CC ) -> ( ( A ( abs o. - ) x ) < ( a / 2 ) -> ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) ) )
140 139 ss2rabdv 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> { x e. CC | ( A ( abs o. - ) x ) < ( a / 2 ) } C_ { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) } )
141 blval 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ ( a / 2 ) e. RR* ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) = { x e. CC | ( A ( abs o. - ) x ) < ( a / 2 ) } )
142 4 31 34 141 mp3an2i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) = { x e. CC | ( A ( abs o. - ) x ) < ( a / 2 ) } )
143 1 a1i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> U = { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) } )
144 140 142 143 3sstr4d 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ U )
145 8 ssntr 
 |-  ( ( ( J e. Top /\ U C_ CC ) /\ ( ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) e. J /\ ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ U ) ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ ( ( int ` J ) ` U ) )
146 28 30 36 144 145 syl22anc 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) C_ ( ( int ` J ) ` U ) )
147 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ ( a / 2 ) e. RR+ ) -> A e. ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) )
148 4 31 33 147 mp3an2i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> A e. ( A ( ball ` ( abs o. - ) ) ( a / 2 ) ) )
149 146 148 sseldd 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) /\ ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r ) -> A e. ( ( int ` J ) ` U ) )
150 149 ex 
 |-  ( ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) /\ r e. NN ) -> ( ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r -> A e. ( ( int ` J ) ` U ) ) )
151 150 reximdva 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> ( E. r e. NN ( ( ( abs ` A ) + a ) + ( 2 / a ) ) < r -> E. r e. NN A e. ( ( int ` J ) ` U ) ) )
152 26 151 mpd 
 |-  ( ( ph /\ ( a e. RR+ /\ ( A ( ball ` ( abs o. - ) ) a ) C_ ( CC \ ( ZZ \ NN ) ) ) ) -> E. r e. NN A e. ( ( int ` J ) ` U ) )
153 14 152 rexlimddv 
 |-  ( ph -> E. r e. NN A e. ( ( int ` J ) ` U ) )