Metamath Proof Explorer


Theorem gamcvg

Description: The pointwise exponential of the series G converges to _G ( A ) x. A . (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Hypotheses lgamcvg.g
|- G = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
lgamcvg.a
|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
Assertion gamcvg
|- ( ph -> ( exp o. seq 1 ( + , G ) ) ~~> ( ( _G ` A ) x. A ) )

Proof

Step Hyp Ref Expression
1 lgamcvg.g
 |-  G = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
2 lgamcvg.a
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
3 nnuz
 |-  NN = ( ZZ>= ` 1 )
4 1zzd
 |-  ( ph -> 1 e. ZZ )
5 efcn
 |-  exp e. ( CC -cn-> CC )
6 5 a1i
 |-  ( ph -> exp e. ( CC -cn-> CC ) )
7 2 eldifad
 |-  ( ph -> A e. CC )
8 7 adantr
 |-  ( ( ph /\ m e. NN ) -> A e. CC )
9 simpr
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
10 9 peano2nnd
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. NN )
11 10 nnrpd
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. RR+ )
12 9 nnrpd
 |-  ( ( ph /\ m e. NN ) -> m e. RR+ )
13 11 12 rpdivcld
 |-  ( ( ph /\ m e. NN ) -> ( ( m + 1 ) / m ) e. RR+ )
14 13 relogcld
 |-  ( ( ph /\ m e. NN ) -> ( log ` ( ( m + 1 ) / m ) ) e. RR )
15 14 recnd
 |-  ( ( ph /\ m e. NN ) -> ( log ` ( ( m + 1 ) / m ) ) e. CC )
16 8 15 mulcld
 |-  ( ( ph /\ m e. NN ) -> ( A x. ( log ` ( ( m + 1 ) / m ) ) ) e. CC )
17 9 nncnd
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
18 9 nnne0d
 |-  ( ( ph /\ m e. NN ) -> m =/= 0 )
19 8 17 18 divcld
 |-  ( ( ph /\ m e. NN ) -> ( A / m ) e. CC )
20 1cnd
 |-  ( ( ph /\ m e. NN ) -> 1 e. CC )
21 19 20 addcld
 |-  ( ( ph /\ m e. NN ) -> ( ( A / m ) + 1 ) e. CC )
22 2 adantr
 |-  ( ( ph /\ m e. NN ) -> A e. ( CC \ ( ZZ \ NN ) ) )
23 22 9 dmgmdivn0
 |-  ( ( ph /\ m e. NN ) -> ( ( A / m ) + 1 ) =/= 0 )
24 21 23 logcld
 |-  ( ( ph /\ m e. NN ) -> ( log ` ( ( A / m ) + 1 ) ) e. CC )
25 16 24 subcld
 |-  ( ( ph /\ m e. NN ) -> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) e. CC )
26 25 1 fmptd
 |-  ( ph -> G : NN --> CC )
27 26 ffvelcdmda
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. CC )
28 3 4 27 serf
 |-  ( ph -> seq 1 ( + , G ) : NN --> CC )
29 1 2 lgamcvg
 |-  ( ph -> seq 1 ( + , G ) ~~> ( ( log_G ` A ) + ( log ` A ) ) )
30 lgamcl
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC )
31 2 30 syl
 |-  ( ph -> ( log_G ` A ) e. CC )
32 2 dmgmn0
 |-  ( ph -> A =/= 0 )
33 7 32 logcld
 |-  ( ph -> ( log ` A ) e. CC )
34 31 33 addcld
 |-  ( ph -> ( ( log_G ` A ) + ( log ` A ) ) e. CC )
35 3 4 6 28 29 34 climcncf
 |-  ( ph -> ( exp o. seq 1 ( + , G ) ) ~~> ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) )
36 efadd
 |-  ( ( ( log_G ` A ) e. CC /\ ( log ` A ) e. CC ) -> ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) = ( ( exp ` ( log_G ` A ) ) x. ( exp ` ( log ` A ) ) ) )
37 31 33 36 syl2anc
 |-  ( ph -> ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) = ( ( exp ` ( log_G ` A ) ) x. ( exp ` ( log ` A ) ) ) )
38 eflgam
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
39 2 38 syl
 |-  ( ph -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
40 eflog
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
41 7 32 40 syl2anc
 |-  ( ph -> ( exp ` ( log ` A ) ) = A )
42 39 41 oveq12d
 |-  ( ph -> ( ( exp ` ( log_G ` A ) ) x. ( exp ` ( log ` A ) ) ) = ( ( _G ` A ) x. A ) )
43 37 42 eqtrd
 |-  ( ph -> ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) = ( ( _G ` A ) x. A ) )
44 35 43 breqtrd
 |-  ( ph -> ( exp o. seq 1 ( + , G ) ) ~~> ( ( _G ` A ) x. A ) )