Metamath Proof Explorer

Theorem lgambdd

Description: The log-Gamma function is bounded on the region U . (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r 
|- ( ph -> R e. NN )
lgamgulm.u 
|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
lgamgulm.g 
|- G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
Assertion lgambdd 
|- ( ph -> E. r e. RR A. z e. U ( abs ` ( log_G ` z ) ) <_ r )

Proof

Step Hyp Ref Expression
1 lgamgulm.r 
 |-  ( ph -> R e. NN )
2 lgamgulm.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3 lgamgulm.g 
 |-  G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
4 1 2 3 lgamgulm2 
 |-  ( ph -> ( A. z e. U ( log_G ` z ) e. CC /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ) )
5 4 simprd 
 |-  ( ph -> seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) )
6 eqid 
 |-  ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) ) = ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) )
7 1 2 3 6 lgamgulmlem6 
 |-  ( ph -> ( seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) /\ ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) -> E. y e. RR A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) ) )
8 7 simprd 
 |-  ( ph -> ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) -> E. y e. RR A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) )
9 5 8 mpd 
 |-  ( ph -> E. y e. RR A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y )
10 1 nnrpd 
 |-  ( ph -> R e. RR+ )
11 10 adantr 
 |-  ( ( ph /\ y e. RR ) -> R e. RR+ )
12 11 relogcld 
 |-  ( ( ph /\ y e. RR ) -> ( log ` R ) e. RR )
13 pire 
 |-  _pi e. RR
14 13 a1i 
 |-  ( ( ph /\ y e. RR ) -> _pi e. RR )
15 12 14 readdcld 
 |-  ( ( ph /\ y e. RR ) -> ( ( log ` R ) + _pi ) e. RR )
16 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
17 15 16 readdcld 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( log ` R ) + _pi ) + y ) e. RR )
18 17 adantrr 
 |-  ( ( ph /\ ( y e. RR /\ A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) ) -> ( ( ( log ` R ) + _pi ) + y ) e. RR )
19 4 simpld 
 |-  ( ph -> A. z e. U ( log_G ` z ) e. CC )
20 19 adantr 
 |-  ( ( ph /\ y e. RR ) -> A. z e. U ( log_G ` z ) e. CC )
21 20 r19.21bi 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log_G ` z ) e. CC )
22 21 abscld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log_G ` z ) ) e. RR )
23 22 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( abs ` ( log_G ` z ) ) e. RR )
24 11 adantr 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> R e. RR+ )
25 24 relogcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` R ) e. RR )
26 13 a1i 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> _pi e. RR )
27 25 26 readdcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( log ` R ) + _pi ) e. RR )
28 1 2 lgamgulmlem1 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )
29 28 adantr 
 |-  ( ( ph /\ y e. RR ) -> U C_ ( CC \ ( ZZ \ NN ) ) )
30 29 sselda 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> z e. ( CC \ ( ZZ \ NN ) ) )
31 30 eldifad 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> z e. CC )
32 30 dmgmn0 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> z =/= 0 )
33 31 32 logcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` z ) e. CC )
34 21 33 addcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( log_G ` z ) + ( log ` z ) ) e. CC )
35 34 abscld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) e. RR )
36 27 35 readdcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( ( log ` R ) + _pi ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) e. RR )
37 36 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( ( ( log ` R ) + _pi ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) e. RR )
38 17 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( ( ( log ` R ) + _pi ) + y ) e. RR )
39 33 abscld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log ` z ) ) e. RR )
40 39 35 readdcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log ` z ) ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) e. RR )
41 33 negcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> -u ( log ` z ) e. CC )
42 21 41 abs2difd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log_G ` z ) ) - ( abs ` -u ( log ` z ) ) ) <_ ( abs ` ( ( log_G ` z ) - -u ( log ` z ) ) ) )
43 33 absnegd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` -u ( log ` z ) ) = ( abs ` ( log ` z ) ) )
44 43 oveq2d 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log_G ` z ) ) - ( abs ` -u ( log ` z ) ) ) = ( ( abs ` ( log_G ` z ) ) - ( abs ` ( log ` z ) ) ) )
45 21 33 subnegd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( log_G ` z ) - -u ( log ` z ) ) = ( ( log_G ` z ) + ( log ` z ) ) )
46 45 fveq2d 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( ( log_G ` z ) - -u ( log ` z ) ) ) = ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) )
47 42 44 46 3brtr3d 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log_G ` z ) ) - ( abs ` ( log ` z ) ) ) <_ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) )
48 22 39 35 lesubadd2d 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( ( abs ` ( log_G ` z ) ) - ( abs ` ( log ` z ) ) ) <_ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <-> ( abs ` ( log_G ` z ) ) <_ ( ( abs ` ( log ` z ) ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) ) )
49 47 48 mpbid 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log_G ` z ) ) <_ ( ( abs ` ( log ` z ) ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) )
50 31 32 absrpcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` z ) e. RR+ )
51 50 relogcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` ( abs ` z ) ) e. RR )
52 51 recnd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` ( abs ` z ) ) e. CC )
53 52 abscld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log ` ( abs ` z ) ) ) e. RR )
54 53 26 readdcld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log ` ( abs ` z ) ) ) + _pi ) e. RR )
55 abslogle 
 |-  ( ( z e. CC /\ z =/= 0 ) -> ( abs ` ( log ` z ) ) <_ ( ( abs ` ( log ` ( abs ` z ) ) ) + _pi ) )
56 31 32 55 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log ` z ) ) <_ ( ( abs ` ( log ` ( abs ` z ) ) ) + _pi ) )
57 df-neg 
 |-  -u ( log ` R ) = ( 0 - ( log ` R ) )
58 log1 
 |-  ( log ` 1 ) = 0
59 58 oveq1i 
 |-  ( ( log ` 1 ) - ( log ` R ) ) = ( 0 - ( log ` R ) )
60 57 59 eqtr4i 
 |-  -u ( log ` R ) = ( ( log ` 1 ) - ( log ` R ) )
61 1rp 
 |-  1 e. RR+
62 relogdiv 
 |-  ( ( 1 e. RR+ /\ R e. RR+ ) -> ( log ` ( 1 / R ) ) = ( ( log ` 1 ) - ( log ` R ) ) )
63 61 24 62 sylancr 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` ( 1 / R ) ) = ( ( log ` 1 ) - ( log ` R ) ) )
64 60 63 eqtr4id 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> -u ( log ` R ) = ( log ` ( 1 / R ) ) )
65 oveq2 
 |-  ( k = 0 -> ( z + k ) = ( z + 0 ) )
66 65 fveq2d 
 |-  ( k = 0 -> ( abs ` ( z + k ) ) = ( abs ` ( z + 0 ) ) )
67 66 breq2d 
 |-  ( k = 0 -> ( ( 1 / R ) <_ ( abs ` ( z + k ) ) <-> ( 1 / R ) <_ ( abs ` ( z + 0 ) ) ) )
68 fveq2 
 |-  ( x = z -> ( abs ` x ) = ( abs ` z ) )
69 68 breq1d 
 |-  ( x = z -> ( ( abs ` x ) <_ R <-> ( abs ` z ) <_ R ) )
70 fvoveq1 
 |-  ( x = z -> ( abs ` ( x + k ) ) = ( abs ` ( z + k ) ) )
71 70 breq2d 
 |-  ( x = z -> ( ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> ( 1 / R ) <_ ( abs ` ( z + k ) ) ) )
72 71 ralbidv 
 |-  ( x = z -> ( A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( z + k ) ) ) )
73 69 72 anbi12d 
 |-  ( x = z -> ( ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) <-> ( ( abs ` z ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( z + k ) ) ) ) )
74 73 2 elrab2 
 |-  ( z e. U <-> ( z e. CC /\ ( ( abs ` z ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( z + k ) ) ) ) )
75 74 simprbi 
 |-  ( z e. U -> ( ( abs ` z ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( z + k ) ) ) )
76 75 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` z ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( z + k ) ) ) )
77 76 simprd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( z + k ) ) )
78 0nn0 
 |-  0 e. NN0
79 78 a1i 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> 0 e. NN0 )
80 67 77 79 rspcdva 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( 1 / R ) <_ ( abs ` ( z + 0 ) ) )
81 31 addridd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( z + 0 ) = z )
82 81 fveq2d 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( z + 0 ) ) = ( abs ` z ) )
83 80 82 breqtrd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( 1 / R ) <_ ( abs ` z ) )
84 24 rpreccld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( 1 / R ) e. RR+ )
85 84 50 logled 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( 1 / R ) <_ ( abs ` z ) <-> ( log ` ( 1 / R ) ) <_ ( log ` ( abs ` z ) ) ) )
86 83 85 mpbid 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` ( 1 / R ) ) <_ ( log ` ( abs ` z ) ) )
87 64 86 eqbrtrd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> -u ( log ` R ) <_ ( log ` ( abs ` z ) ) )
88 76 simpld 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` z ) <_ R )
89 50 24 logled 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` z ) <_ R <-> ( log ` ( abs ` z ) ) <_ ( log ` R ) ) )
90 88 89 mpbid 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( log ` ( abs ` z ) ) <_ ( log ` R ) )
91 51 25 absled 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log ` ( abs ` z ) ) ) <_ ( log ` R ) <-> ( -u ( log ` R ) <_ ( log ` ( abs ` z ) ) /\ ( log ` ( abs ` z ) ) <_ ( log ` R ) ) ) )
92 87 90 91 mpbir2and 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log ` ( abs ` z ) ) ) <_ ( log ` R ) )
93 53 25 26 92 leadd1dd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log ` ( abs ` z ) ) ) + _pi ) <_ ( ( log ` R ) + _pi ) )
94 39 54 27 56 93 letrd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log ` z ) ) <_ ( ( log ` R ) + _pi ) )
95 39 27 35 94 leadd1dd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( log ` z ) ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) <_ ( ( ( log ` R ) + _pi ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) )
96 22 40 36 49 95 letrd 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) )
97 96 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) )
98 35 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) e. RR )
99 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> y e. RR )
100 27 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( ( log ` R ) + _pi ) e. RR )
101 simpr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y )
102 98 99 100 101 leadd2dd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( ( ( log ` R ) + _pi ) + ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) ) <_ ( ( ( log ` R ) + _pi ) + y ) )
103 23 37 38 97 102 letrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. U ) /\ ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) -> ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + y ) )
104 103 ex 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. U ) -> ( ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y -> ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + y ) ) )
105 104 ralimdva 
 |-  ( ( ph /\ y e. RR ) -> ( A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y -> A. z e. U ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + y ) ) )
106 105 impr 
 |-  ( ( ph /\ ( y e. RR /\ A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) ) -> A. z e. U ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + y ) )
107 brralrspcev 
 |-  ( ( ( ( ( log ` R ) + _pi ) + y ) e. RR /\ A. z e. U ( abs ` ( log_G ` z ) ) <_ ( ( ( log ` R ) + _pi ) + y ) ) -> E. r e. RR A. z e. U ( abs ` ( log_G ` z ) ) <_ r )
108 18 106 107 syl2anc 
 |-  ( ( ph /\ ( y e. RR /\ A. z e. U ( abs ` ( ( log_G ` z ) + ( log ` z ) ) ) <_ y ) ) -> E. r e. RR A. z e. U ( abs ` ( log_G ` z ) ) <_ r )
109 9 108 rexlimddv 
 |-  ( ph -> E. r e. RR A. z e. U ( abs ` ( log_G ` z ) ) <_ r )