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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 )