Metamath Proof Explorer

Theorem iprodfac

Description: An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion iprodfac 
|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1zzd 
 |-  ( A e. NN0 -> 1 e. ZZ )
3 facne0 
 |-  ( A e. NN0 -> ( ! ` A ) =/= 0 )
4 eqid 
 |-  ( x e. NN |-> ( ( ( 1 + ( 1 / x ) ) ^ A ) / ( 1 + ( A / x ) ) ) ) = ( x e. NN |-> ( ( ( 1 + ( 1 / x ) ) ^ A ) / ( 1 + ( A / x ) ) ) )
5 4 faclim 
 |-  ( A e. NN0 -> seq 1 ( x. , ( x e. NN |-> ( ( ( 1 + ( 1 / x ) ) ^ A ) / ( 1 + ( A / x ) ) ) ) ) ~~> ( ! ` A ) )
6 oveq2 
 |-  ( x = k -> ( 1 / x ) = ( 1 / k ) )
7 6 oveq2d 
 |-  ( x = k -> ( 1 + ( 1 / x ) ) = ( 1 + ( 1 / k ) ) )
8 7 oveq1d 
 |-  ( x = k -> ( ( 1 + ( 1 / x ) ) ^ A ) = ( ( 1 + ( 1 / k ) ) ^ A ) )
9 oveq2 
 |-  ( x = k -> ( A / x ) = ( A / k ) )
10 9 oveq2d 
 |-  ( x = k -> ( 1 + ( A / x ) ) = ( 1 + ( A / k ) ) )
11 8 10 oveq12d 
 |-  ( x = k -> ( ( ( 1 + ( 1 / x ) ) ^ A ) / ( 1 + ( A / x ) ) ) = ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) )
12 ovex 
 |-  ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) e. _V
13 11 4 12 fvmpt 
 |-  ( k e. NN -> ( ( x e. NN |-> ( ( ( 1 + ( 1 / x ) ) ^ A ) / ( 1 + ( A / x ) ) ) ) ` k ) = ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) )
14 13 adantl 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( ( x e. NN |-> ( ( ( 1 + ( 1 / x ) ) ^ A ) / ( 1 + ( A / x ) ) ) ) ` k ) = ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) )
15 1rp 
 |-  1 e. RR+
16 15 a1i 
 |-  ( ( A e. NN0 /\ k e. NN ) -> 1 e. RR+ )
17 simpr 
 |-  ( ( A e. NN0 /\ k e. NN ) -> k e. NN )
18 17 nnrpd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> k e. RR+ )
19 18 rpreccld 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( 1 / k ) e. RR+ )
20 16 19 rpaddcld 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( 1 + ( 1 / k ) ) e. RR+ )
21 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
22 21 adantr 
 |-  ( ( A e. NN0 /\ k e. NN ) -> A e. ZZ )
23 20 22 rpexpcld 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( ( 1 + ( 1 / k ) ) ^ A ) e. RR+ )
24 1cnd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> 1 e. CC )
25 nn0nndivcl 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( A / k ) e. RR )
26 25 recnd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( A / k ) e. CC )
27 24 26 addcomd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( 1 + ( A / k ) ) = ( ( A / k ) + 1 ) )
28 nn0ge0div 
 |-  ( ( A e. NN0 /\ k e. NN ) -> 0 <_ ( A / k ) )
29 25 28 ge0p1rpd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( ( A / k ) + 1 ) e. RR+ )
30 27 29 eqeltrd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( 1 + ( A / k ) ) e. RR+ )
31 23 30 rpdivcld 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) e. RR+ )
32 31 rpcnd 
 |-  ( ( A e. NN0 /\ k e. NN ) -> ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) e. CC )
33 1 2 3 5 14 32 iprodn0 
 |-  ( A e. NN0 -> prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) = ( ! ` A ) )
34 33 eqcomd 
 |-  ( A e. NN0 -> ( ! ` A ) = prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) )