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