Metamath Proof Explorer

Theorem lgam1

Description: The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Assertion lgam1 
|- ( log_G ` 1 ) = 0

Proof

Step Hyp Ref Expression
1 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
2 1 nnrpd 
 |-  ( m e. NN -> ( m + 1 ) e. RR+ )
3 nnrp 
 |-  ( m e. NN -> m e. RR+ )
4 2 3 rpdivcld 
 |-  ( m e. NN -> ( ( m + 1 ) / m ) e. RR+ )
5 4 relogcld 
 |-  ( m e. NN -> ( log ` ( ( m + 1 ) / m ) ) e. RR )
6 5 recnd 
 |-  ( m e. NN -> ( log ` ( ( m + 1 ) / m ) ) e. CC )
7 6 mullidd 
 |-  ( m e. NN -> ( 1 x. ( log ` ( ( m + 1 ) / m ) ) ) = ( log ` ( ( m + 1 ) / m ) ) )
8 nncn 
 |-  ( m e. NN -> m e. CC )
9 nnne0 
 |-  ( m e. NN -> m =/= 0 )
10 8 9 dividd 
 |-  ( m e. NN -> ( m / m ) = 1 )
11 10 oveq1d 
 |-  ( m e. NN -> ( ( m / m ) + ( 1 / m ) ) = ( 1 + ( 1 / m ) ) )
12 1cnd 
 |-  ( m e. NN -> 1 e. CC )
13 8 12 8 9 divdird 
 |-  ( m e. NN -> ( ( m + 1 ) / m ) = ( ( m / m ) + ( 1 / m ) ) )
14 8 9 reccld 
 |-  ( m e. NN -> ( 1 / m ) e. CC )
15 14 12 addcomd 
 |-  ( m e. NN -> ( ( 1 / m ) + 1 ) = ( 1 + ( 1 / m ) ) )
16 11 13 15 3eqtr4rd 
 |-  ( m e. NN -> ( ( 1 / m ) + 1 ) = ( ( m + 1 ) / m ) )
17 16 fveq2d 
 |-  ( m e. NN -> ( log ` ( ( 1 / m ) + 1 ) ) = ( log ` ( ( m + 1 ) / m ) ) )
18 7 17 oveq12d 
 |-  ( m e. NN -> ( ( 1 x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( 1 / m ) + 1 ) ) ) = ( ( log ` ( ( m + 1 ) / m ) ) - ( log ` ( ( m + 1 ) / m ) ) ) )
19 6 subidd 
 |-  ( m e. NN -> ( ( log ` ( ( m + 1 ) / m ) ) - ( log ` ( ( m + 1 ) / m ) ) ) = 0 )
20 18 19 eqtrd 
 |-  ( m e. NN -> ( ( 1 x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( 1 / m ) + 1 ) ) ) = 0 )
21 20 mpteq2ia 
 |-  ( m e. NN |-> ( ( 1 x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( 1 / m ) + 1 ) ) ) ) = ( m e. NN |-> 0 )
22 fconstmpt 
 |-  ( NN X. { 0 } ) = ( m e. NN |-> 0 )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 23 xpeq1i 
 |-  ( NN X. { 0 } ) = ( ( ZZ>= ` 1 ) X. { 0 } )
25 21 22 24 3eqtr2ri 
 |-  ( ( ZZ>= ` 1 ) X. { 0 } ) = ( m e. NN |-> ( ( 1 x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( 1 / m ) + 1 ) ) ) )
26 ax-1cn 
 |-  1 e. CC
27 1nn 
 |-  1 e. NN
28 eldifn 
 |-  ( 1 e. ( ZZ \ NN ) -> -. 1 e. NN )
29 27 28 mt2 
 |-  -. 1 e. ( ZZ \ NN )
30 eldif 
 |-  ( 1 e. ( CC \ ( ZZ \ NN ) ) <-> ( 1 e. CC /\ -. 1 e. ( ZZ \ NN ) ) )
31 26 29 30 mpbir2an 
 |-  1 e. ( CC \ ( ZZ \ NN ) )
32 31 a1i 
 |-  ( T. -> 1 e. ( CC \ ( ZZ \ NN ) ) )
33 25 32 lgamcvg 
 |-  ( T. -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> ( ( log_G ` 1 ) + ( log ` 1 ) ) )
34 33 mptru 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> ( ( log_G ` 1 ) + ( log ` 1 ) )
35 log1 
 |-  ( log ` 1 ) = 0
36 35 oveq2i 
 |-  ( ( log_G ` 1 ) + ( log ` 1 ) ) = ( ( log_G ` 1 ) + 0 )
37 lgamcl 
 |-  ( 1 e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` 1 ) e. CC )
38 31 37 ax-mp 
 |-  ( log_G ` 1 ) e. CC
39 38 addridi 
 |-  ( ( log_G ` 1 ) + 0 ) = ( log_G ` 1 )
40 36 39 eqtri 
 |-  ( ( log_G ` 1 ) + ( log ` 1 ) ) = ( log_G ` 1 )
41 34 40 breqtri 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> ( log_G ` 1 )
42 1z 
 |-  1 e. ZZ
43 serclim0 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 )
44 42 43 ax-mp 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0
45 climuni 
 |-  ( ( seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> ( log_G ` 1 ) /\ seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 ) -> ( log_G ` 1 ) = 0 )
46 41 44 45 mp2an 
 |-  ( log_G ` 1 ) = 0