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