Metamath Proof Explorer

Theorem regamcl

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

Ref Expression
Assertion regamcl 
|- ( A e. ( RR \ ( ZZ \ NN ) ) -> ( _G ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> A e. RR )
2 1 recnd 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> A e. CC )
3 eldifn 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> -. A e. ( ZZ \ NN ) )
4 2 3 eldifd 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
5 gamcl 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) e. CC )
6 4 5 syl 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> ( _G ` A ) e. CC )
7 4 dmgmn0 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> A =/= 0 )
8 6 2 7 divcan4d 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> ( ( ( _G ` A ) x. A ) / A ) = ( _G ` A ) )
9 nnuz 
 |-  NN = ( ZZ>= ` 1 )
10 1zzd 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> 1 e. ZZ )
11 eqid 
 |-  ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) ) = ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) )
12 11 4 gamcvg2 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> seq 1 ( x. , ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) ) ) ~~> ( ( _G ` A ) x. A ) )
13 simpr 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> m e. NN )
14 13 peano2nnd 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( m + 1 ) e. NN )
15 14 nnrpd 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( m + 1 ) e. RR+ )
16 13 nnrpd 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> m e. RR+ )
17 15 16 rpdivcld 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( ( m + 1 ) / m ) e. RR+ )
18 17 rpred 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( ( m + 1 ) / m ) e. RR )
19 17 rpge0d 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> 0 <_ ( ( m + 1 ) / m ) )
20 1 adantr 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> A e. RR )
21 18 19 20 recxpcld 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( ( ( m + 1 ) / m ) ^c A ) e. RR )
22 20 13 nndivred 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( A / m ) e. RR )
23 1red 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> 1 e. RR )
24 22 23 readdcld 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( ( A / m ) + 1 ) e. RR )
25 4 adantr 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> A e. ( CC \ ( ZZ \ NN ) ) )
26 25 13 dmgmdivn0 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( ( A / m ) + 1 ) =/= 0 )
27 21 24 26 redivcld 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ m e. NN ) -> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) e. RR )
28 27 fmpttd 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) ) : NN --> RR )
29 28 ffvelrnda 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) ) ` n ) e. RR )
30 remulcl 
 |-  ( ( n e. RR /\ x e. RR ) -> ( n x. x ) e. RR )
31 30 adantl 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ ( n e. RR /\ x e. RR ) ) -> ( n x. x ) e. RR )
32 9 10 29 31 seqf 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> seq 1 ( x. , ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) ) ) : NN --> RR )
33 32 ffvelrnda 
 |-  ( ( A e. ( RR \ ( ZZ \ NN ) ) /\ n e. NN ) -> ( seq 1 ( x. , ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) ) ) ` n ) e. RR )
34 9 10 12 33 climrecl 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> ( ( _G ` A ) x. A ) e. RR )
35 34 1 7 redivcld 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> ( ( ( _G ` A ) x. A ) / A ) e. RR )
36 8 35 eqeltrrd 
 |-  ( A e. ( RR \ ( ZZ \ NN ) ) -> ( _G ` A ) e. RR )