Metamath Proof Explorer

Theorem gamcvg2lem

Description: Lemma for gamcvg2 . (Contributed by Mario Carneiro, 10-Jul-2017)

Ref Expression
Hypotheses gamcvg2.f 
|- F = ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) )
gamcvg2.a 
|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
gamcvg2.g 
|- G = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
Assertion gamcvg2lem 
|- ( ph -> ( exp o. seq 1 ( + , G ) ) = seq 1 ( x. , F ) )

Proof

Step Hyp Ref Expression
1 gamcvg2.f 
 |-  F = ( m e. NN |-> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) )
2 gamcvg2.a 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
3 gamcvg2.g 
 |-  G = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
4 addcl 
 |-  ( ( n e. CC /\ x e. CC ) -> ( n + x ) e. CC )
5 4 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. CC /\ x e. CC ) ) -> ( n + x ) e. CC )
6 simpll 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ph )
7 elfznn 
 |-  ( n e. ( 1 ... k ) -> n e. NN )
8 7 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n e. NN )
9 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
10 id 
 |-  ( m = n -> m = n )
11 9 10 oveq12d 
 |-  ( m = n -> ( ( m + 1 ) / m ) = ( ( n + 1 ) / n ) )
12 11 fveq2d 
 |-  ( m = n -> ( log ` ( ( m + 1 ) / m ) ) = ( log ` ( ( n + 1 ) / n ) ) )
13 12 oveq2d 
 |-  ( m = n -> ( A x. ( log ` ( ( m + 1 ) / m ) ) ) = ( A x. ( log ` ( ( n + 1 ) / n ) ) ) )
14 oveq2 
 |-  ( m = n -> ( A / m ) = ( A / n ) )
15 14 oveq1d 
 |-  ( m = n -> ( ( A / m ) + 1 ) = ( ( A / n ) + 1 ) )
16 15 fveq2d 
 |-  ( m = n -> ( log ` ( ( A / m ) + 1 ) ) = ( log ` ( ( A / n ) + 1 ) ) )
17 13 16 oveq12d 
 |-  ( m = n -> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) = ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) )
18 ovex 
 |-  ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) e. _V
19 17 3 18 fvmpt 
 |-  ( n e. NN -> ( G ` n ) = ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) )
20 19 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) )
21 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. ( CC \ ( ZZ \ NN ) ) )
22 21 eldifad 
 |-  ( ( ph /\ n e. NN ) -> A e. CC )
23 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
24 23 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
25 24 nnrpd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. RR+ )
26 23 nnrpd 
 |-  ( ( ph /\ n e. NN ) -> n e. RR+ )
27 25 26 rpdivcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( n + 1 ) / n ) e. RR+ )
28 27 relogcld 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( n + 1 ) / n ) ) e. RR )
29 28 recnd 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( n + 1 ) / n ) ) e. CC )
30 22 29 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( A x. ( log ` ( ( n + 1 ) / n ) ) ) e. CC )
31 23 nncnd 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
32 23 nnne0d 
 |-  ( ( ph /\ n e. NN ) -> n =/= 0 )
33 22 31 32 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( A / n ) e. CC )
34 1cnd 
 |-  ( ( ph /\ n e. NN ) -> 1 e. CC )
35 33 34 addcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A / n ) + 1 ) e. CC )
36 21 23 dmgmdivn0 
 |-  ( ( ph /\ n e. NN ) -> ( ( A / n ) + 1 ) =/= 0 )
37 35 36 logcld 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( A / n ) + 1 ) ) e. CC )
38 30 37 subcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) e. CC )
39 20 38 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. CC )
40 6 8 39 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( G ` n ) e. CC )
41 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
42 nnuz 
 |-  NN = ( ZZ>= ` 1 )
43 41 42 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
44 efadd 
 |-  ( ( n e. CC /\ x e. CC ) -> ( exp ` ( n + x ) ) = ( ( exp ` n ) x. ( exp ` x ) ) )
45 44 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. CC /\ x e. CC ) ) -> ( exp ` ( n + x ) ) = ( ( exp ` n ) x. ( exp ` x ) ) )
46 efsub 
 |-  ( ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) e. CC /\ ( log ` ( ( A / n ) + 1 ) ) e. CC ) -> ( exp ` ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) ) = ( ( exp ` ( A x. ( log ` ( ( n + 1 ) / n ) ) ) ) / ( exp ` ( log ` ( ( A / n ) + 1 ) ) ) ) )
47 30 37 46 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( exp ` ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) ) = ( ( exp ` ( A x. ( log ` ( ( n + 1 ) / n ) ) ) ) / ( exp ` ( log ` ( ( A / n ) + 1 ) ) ) ) )
48 31 34 addcld 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. CC )
49 48 31 32 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( n + 1 ) / n ) e. CC )
50 24 nnne0d 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) =/= 0 )
51 48 31 50 32 divne0d 
 |-  ( ( ph /\ n e. NN ) -> ( ( n + 1 ) / n ) =/= 0 )
52 49 51 22 cxpefd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( n + 1 ) / n ) ^c A ) = ( exp ` ( A x. ( log ` ( ( n + 1 ) / n ) ) ) ) )
53 52 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( exp ` ( A x. ( log ` ( ( n + 1 ) / n ) ) ) ) = ( ( ( n + 1 ) / n ) ^c A ) )
54 eflog 
 |-  ( ( ( ( A / n ) + 1 ) e. CC /\ ( ( A / n ) + 1 ) =/= 0 ) -> ( exp ` ( log ` ( ( A / n ) + 1 ) ) ) = ( ( A / n ) + 1 ) )
55 35 36 54 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( exp ` ( log ` ( ( A / n ) + 1 ) ) ) = ( ( A / n ) + 1 ) )
56 53 55 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( exp ` ( A x. ( log ` ( ( n + 1 ) / n ) ) ) ) / ( exp ` ( log ` ( ( A / n ) + 1 ) ) ) ) = ( ( ( ( n + 1 ) / n ) ^c A ) / ( ( A / n ) + 1 ) ) )
57 47 56 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( exp ` ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) ) = ( ( ( ( n + 1 ) / n ) ^c A ) / ( ( A / n ) + 1 ) ) )
58 20 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( exp ` ( G ` n ) ) = ( exp ` ( ( A x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( A / n ) + 1 ) ) ) ) )
59 11 oveq1d 
 |-  ( m = n -> ( ( ( m + 1 ) / m ) ^c A ) = ( ( ( n + 1 ) / n ) ^c A ) )
60 59 15 oveq12d 
 |-  ( m = n -> ( ( ( ( m + 1 ) / m ) ^c A ) / ( ( A / m ) + 1 ) ) = ( ( ( ( n + 1 ) / n ) ^c A ) / ( ( A / n ) + 1 ) ) )
61 ovex 
 |-  ( ( ( ( n + 1 ) / n ) ^c A ) / ( ( A / n ) + 1 ) ) e. _V
62 60 1 61 fvmpt 
 |-  ( n e. NN -> ( F ` n ) = ( ( ( ( n + 1 ) / n ) ^c A ) / ( ( A / n ) + 1 ) ) )
63 62 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( ( ( n + 1 ) / n ) ^c A ) / ( ( A / n ) + 1 ) ) )
64 57 58 63 3eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( exp ` ( G ` n ) ) = ( F ` n ) )
65 6 8 64 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( exp ` ( G ` n ) ) = ( F ` n ) )
66 5 40 43 45 65 seqhomo 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( seq 1 ( + , G ) ` k ) ) = ( seq 1 ( x. , F ) ` k ) )
67 66 mpteq2dva 
 |-  ( ph -> ( k e. NN |-> ( exp ` ( seq 1 ( + , G ) ` k ) ) ) = ( k e. NN |-> ( seq 1 ( x. , F ) ` k ) ) )
68 eff 
 |-  exp : CC --> CC
69 68 a1i 
 |-  ( ph -> exp : CC --> CC )
70 1z 
 |-  1 e. ZZ
71 70 a1i 
 |-  ( ph -> 1 e. ZZ )
72 42 71 39 serf 
 |-  ( ph -> seq 1 ( + , G ) : NN --> CC )
73 fcompt 
 |-  ( ( exp : CC --> CC /\ seq 1 ( + , G ) : NN --> CC ) -> ( exp o. seq 1 ( + , G ) ) = ( k e. NN |-> ( exp ` ( seq 1 ( + , G ) ` k ) ) ) )
74 69 72 73 syl2anc 
 |-  ( ph -> ( exp o. seq 1 ( + , G ) ) = ( k e. NN |-> ( exp ` ( seq 1 ( + , G ) ` k ) ) ) )
75 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( x. , F ) Fn ( ZZ>= ` 1 ) )
76 70 75 mp1i 
 |-  ( ph -> seq 1 ( x. , F ) Fn ( ZZ>= ` 1 ) )
77 42 fneq2i 
 |-  ( seq 1 ( x. , F ) Fn NN <-> seq 1 ( x. , F ) Fn ( ZZ>= ` 1 ) )
78 76 77 sylibr 
 |-  ( ph -> seq 1 ( x. , F ) Fn NN )
79 dffn5 
 |-  ( seq 1 ( x. , F ) Fn NN <-> seq 1 ( x. , F ) = ( k e. NN |-> ( seq 1 ( x. , F ) ` k ) ) )
80 78 79 sylib 
 |-  ( ph -> seq 1 ( x. , F ) = ( k e. NN |-> ( seq 1 ( x. , F ) ` k ) ) )
81 67 74 80 3eqtr4d 
 |-  ( ph -> ( exp o. seq 1 ( + , G ) ) = seq 1 ( x. , F ) )