Metamath Proof Explorer

Theorem relgamcl

Description: The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Assertion relgamcl 
|- ( A e. RR+ -> ( log_G ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 rpdmgm 
 |-  ( A e. RR+ -> A e. ( CC \ ( ZZ \ NN ) ) )
2 lgamcl 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC )
3 1 2 syl 
 |-  ( A e. RR+ -> ( log_G ` A ) e. CC )
4 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
5 4 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
6 3 5 pncand 
 |-  ( A e. RR+ -> ( ( ( log_G ` A ) + ( log ` A ) ) - ( log ` A ) ) = ( log_G ` A ) )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1zzd 
 |-  ( A e. RR+ -> 1 e. ZZ )
9 eqid 
 |-  ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
10 9 1 lgamcvg 
 |-  ( A e. RR+ -> seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) )
11 simpl 
 |-  ( ( A e. RR+ /\ m e. NN ) -> A e. RR+ )
12 11 rpred 
 |-  ( ( A e. RR+ /\ m e. NN ) -> A e. RR )
13 simpr 
 |-  ( ( A e. RR+ /\ m e. NN ) -> m e. NN )
14 13 peano2nnd 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( m + 1 ) e. NN )
15 14 nnrpd 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( m + 1 ) e. RR+ )
16 13 nnrpd 
 |-  ( ( A e. RR+ /\ m e. NN ) -> m e. RR+ )
17 15 16 rpdivcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( ( m + 1 ) / m ) e. RR+ )
18 17 relogcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( log ` ( ( m + 1 ) / m ) ) e. RR )
19 12 18 remulcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( A x. ( log ` ( ( m + 1 ) / m ) ) ) e. RR )
20 11 16 rpdivcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( A / m ) e. RR+ )
21 1rp 
 |-  1 e. RR+
22 21 a1i 
 |-  ( ( A e. RR+ /\ m e. NN ) -> 1 e. RR+ )
23 20 22 rpaddcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( ( A / m ) + 1 ) e. RR+ )
24 23 relogcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( log ` ( ( A / m ) + 1 ) ) e. RR )
25 19 24 resubcld 
 |-  ( ( A e. RR+ /\ m e. NN ) -> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) e. RR )
26 25 fmpttd 
 |-  ( A e. RR+ -> ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) : NN --> RR )
27 26 ffvelcdmda 
 |-  ( ( A e. RR+ /\ n e. NN ) -> ( ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ` n ) e. RR )
28 7 8 27 serfre 
 |-  ( A e. RR+ -> seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) : NN --> RR )
29 28 ffvelcdmda 
 |-  ( ( A e. RR+ /\ n e. NN ) -> ( seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ` n ) e. RR )
30 7 8 10 29 climrecl 
 |-  ( A e. RR+ -> ( ( log_G ` A ) + ( log ` A ) ) e. RR )
31 30 4 resubcld 
 |-  ( A e. RR+ -> ( ( ( log_G ` A ) + ( log ` A ) ) - ( log ` A ) ) e. RR )
32 6 31 eqeltrrd 
 |-  ( A e. RR+ -> ( log_G ` A ) e. RR )