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