Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lgamcvg2 Unicode version

Theorem lgamcvg2 24792
Description: The series  G converges to  log  _G ( A  +  1
). (Contributed by Mario Carneiro, 9-Jul-2017.)
Hypotheses
Ref Expression
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
Ref Expression
lgamcvg2  |-  ( ph  ->  seq  1 (  +  ,  G )  ~~>  ( log  _G `  ( A  + 
1 ) ) )
Distinct variable groups:    A, m    ph, m
Allowed substitution hint:    G( m)

Proof of Theorem lgamcvg2
Dummy variables  k  n  r  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10477 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 10267 . . . 4  |-  1  e.  ZZ
32a1i 11 . . 3  |-  ( ph  ->  1  e.  ZZ )
4 eqid 2404 . . . 4  |-  ( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  ( ( m  + 
1 )  /  m
) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) )  =  ( m  e.  NN  |->  ( ( ( A  + 
1 )  x.  ( log `  ( ( m  +  1 )  /  m ) ) )  -  ( log `  (
( ( A  + 
1 )  /  m
)  +  1 ) ) ) )
5 lgamcvg.a . . . . 5  |-  ( ph  ->  A  e.  ( CC 
\  ( ZZ  \  NN ) ) )
6 1nn0 10193 . . . . . 6  |-  1  e.  NN0
76a1i 11 . . . . 5  |-  ( ph  ->  1  e.  NN0 )
85, 7dmgmaddnn0 24764 . . . 4  |-  ( ph  ->  ( A  +  1 )  e.  ( CC 
\  ( ZZ  \  NN ) ) )
94, 8lgamcvg 24791 . . 3  |-  ( ph  ->  seq  1 (  +  ,  ( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) ) )  ~~>  ( ( log  _G `  ( A  +  1 ) )  +  ( log `  ( A  +  1 ) ) ) )
10 seqex 11280 . . . 4  |-  seq  1
(  +  ,  G
)  e.  _V
1110a1i 11 . . 3  |-  ( ph  ->  seq  1 (  +  ,  G )  e. 
_V )
125eldifad 3292 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
1312abscld 12193 . . . . . . 7  |-  ( ph  ->  ( abs `  A
)  e.  RR )
14 arch 10174 . . . . . . 7  |-  ( ( abs `  A )  e.  RR  ->  E. r  e.  NN  ( abs `  A
)  <  r )
1513, 14syl 16 . . . . . 6  |-  ( ph  ->  E. r  e.  NN  ( abs `  A )  <  r )
16 eqid 2404 . . . . . . . . 9  |-  ( ZZ>= `  r )  =  (
ZZ>= `  r )
17 simprl 733 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  r  e.  NN )
1817nnzd 10330 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  r  e.  ZZ )
19 eqid 2404 . . . . . . . . . . 11  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
2019logcn 20491 . . . . . . . . . 10  |-  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  e.  ( ( CC  \  (  -oo (,] 0 ) ) -cn-> CC )
2120a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  ( log  |`  ( CC  \ 
(  -oo (,] 0 ) ) )  e.  ( ( CC  \  (  -oo (,] 0 ) )
-cn-> CC ) )
22 eqid 2404 . . . . . . . . . . . 12  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
2322dvlog2lem 20496 . . . . . . . . . . 11  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  (  -oo (,] 0 ) )
2412ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  A  e.  CC )
251uztrn2 10459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  NN  /\  m  e.  ( ZZ>= `  r ) )  ->  m  e.  NN )
2625ex 424 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  e.  NN  ->  (
m  e.  ( ZZ>= `  r )  ->  m  e.  NN ) )
2726ad2antrl 709 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
m  e.  ( ZZ>= `  r )  ->  m  e.  NN ) )
2827imp 419 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  m  e.  NN )
2928nncnd 9972 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  m  e.  CC )
30 ax-1cn 9004 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
3130a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  1  e.  CC )
3229, 31addcld 9063 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( m  + 
1 )  e.  CC )
3328peano2nnd 9973 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( m  + 
1 )  e.  NN )
3433nnne0d 10000 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( m  + 
1 )  =/=  0
)
3524, 32, 34divcld 9746 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( A  / 
( m  +  1 ) )  e.  CC )
3635, 31addcld 9063 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( A  /  ( m  + 
1 ) )  +  1 )  e.  CC )
37 eqid 2404 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3837cnmetdval 18758 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  / 
( m  +  1 ) )  +  1 )  e.  CC  /\  1  e.  CC )  ->  ( ( ( A  /  ( m  + 
1 ) )  +  1 ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( ( ( A  /  ( m  + 
1 ) )  +  1 )  -  1 ) ) )
3936, 30, 38sylancl 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( ( A  /  ( m  +  1 ) )  +  1 ) ( abs  o.  -  )
1 )  =  ( abs `  ( ( ( A  /  (
m  +  1 ) )  +  1 )  -  1 ) ) )
4035, 31pncand 9368 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( ( A  /  ( m  +  1 ) )  +  1 )  - 
1 )  =  ( A  /  ( m  +  1 ) ) )
4140fveq2d 5691 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  (
( ( A  / 
( m  +  1 ) )  +  1 )  -  1 ) )  =  ( abs `  ( A  /  (
m  +  1 ) ) ) )
4224, 32, 34absdivd 12212 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  ( A  /  ( m  + 
1 ) ) )  =  ( ( abs `  A )  /  ( abs `  ( m  + 
1 ) ) ) )
4333nnred 9971 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( m  + 
1 )  e.  RR )
4433nnrpd 10603 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( m  + 
1 )  e.  RR+ )
4544rpge0d 10608 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  0  <_  (
m  +  1 ) )
4643, 45absidd 12180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  (
m  +  1 ) )  =  ( m  +  1 ) )
4746oveq2d 6056 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( abs `  A )  /  ( abs `  ( m  + 
1 ) ) )  =  ( ( abs `  A )  /  (
m  +  1 ) ) )
4842, 47eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  ( A  /  ( m  + 
1 ) ) )  =  ( ( abs `  A )  /  (
m  +  1 ) ) )
4939, 41, 483eqtrd 2440 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( ( A  /  ( m  +  1 ) )  +  1 ) ( abs  o.  -  )
1 )  =  ( ( abs `  A
)  /  ( m  +  1 ) ) )
5013ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  A
)  e.  RR )
5117adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  r  e.  NN )
5251nnred 9971 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  r  e.  RR )
53 simplrr 738 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  A
)  <  r )
54 eluzle 10454 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  r
)  ->  r  <_  m )
5554adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  r  <_  m
)
56 nnleltp1 10285 . . . . . . . . . . . . . . . . . 18  |-  ( ( r  e.  NN  /\  m  e.  NN )  ->  ( r  <_  m  <->  r  <  ( m  + 
1 ) ) )
5751, 28, 56syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( r  <_  m 
<->  r  <  ( m  +  1 ) ) )
5855, 57mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  r  <  (
m  +  1 ) )
5950, 52, 43, 53, 58lttrd 9187 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  A
)  <  ( m  +  1 ) )
6032mulid1d 9061 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( m  +  1 )  x.  1 )  =  ( m  +  1 ) )
6159, 60breqtrrd 4198 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs `  A
)  <  ( (
m  +  1 )  x.  1 ) )
62 1re 9046 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
6362a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  1  e.  RR )
6450, 63, 44ltdivmuld 10651 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( ( abs `  A )  /  ( m  + 
1 ) )  <  1  <->  ( abs `  A
)  <  ( (
m  +  1 )  x.  1 ) ) )
6561, 64mpbird 224 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( abs `  A )  /  (
m  +  1 ) )  <  1 )
6649, 65eqbrtrd 4192 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( ( A  /  ( m  +  1 ) )  +  1 ) ( abs  o.  -  )
1 )  <  1
)
67 cnxmet 18760 . . . . . . . . . . . . . 14  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
6867a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
69 1rp 10572 . . . . . . . . . . . . . 14  |-  1  e.  RR+
70 rpxr 10575 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
7169, 70mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  1  e.  RR* )
72 elbl3 18375 . . . . . . . . . . . . 13  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  1  e.  RR* )  /\  ( 1  e.  CC  /\  ( ( A  /  ( m  +  1 ) )  +  1 )  e.  CC ) )  -> 
( ( ( A  /  ( m  + 
1 ) )  +  1 )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( (
( A  /  (
m  +  1 ) )  +  1 ) ( abs  o.  -  ) 1 )  <  1 ) )
7368, 71, 31, 36, 72syl22anc 1185 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( ( A  /  ( m  +  1 ) )  +  1 )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <-> 
( ( ( A  /  ( m  + 
1 ) )  +  1 ) ( abs 
o.  -  ) 1 )  <  1 ) )
7466, 73mpbird 224 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( A  /  ( m  + 
1 ) )  +  1 )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
7523, 74sseldi 3306 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( A  /  ( m  + 
1 ) )  +  1 )  e.  ( CC  \  (  -oo (,] 0 ) ) )
76 eqid 2404 . . . . . . . . . 10  |-  ( m  e.  ( ZZ>= `  r
)  |->  ( ( A  /  ( m  + 
1 ) )  +  1 ) )  =  ( m  e.  (
ZZ>= `  r )  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) )
7775, 76fmptd 5852 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
m  e.  ( ZZ>= `  r )  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) ) : ( ZZ>= `  r
) --> ( CC  \ 
(  -oo (,] 0 ) ) )
7827ssrdv 3314 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  ( ZZ>=
`  r )  C_  NN )
79 resmpt 5150 . . . . . . . . . . 11  |-  ( (
ZZ>= `  r )  C_  NN  ->  ( ( m  e.  NN  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) )  |`  ( ZZ>= `  r )
)  =  ( m  e.  ( ZZ>= `  r
)  |->  ( ( A  /  ( m  + 
1 ) )  +  1 ) ) )
8078, 79syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) )  |`  ( ZZ>=
`  r ) )  =  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )
8113recnd 9070 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( abs `  A
)  e.  CC )
82 divcnv 12588 . . . . . . . . . . . . . . . . 17  |-  ( ( abs `  A )  e.  CC  ->  (
m  e.  NN  |->  ( ( abs `  A
)  /  m ) )  ~~>  0 )
8381, 82syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( m  e.  NN  |->  ( ( abs `  A
)  /  m ) )  ~~>  0 )
84 nnex 9962 . . . . . . . . . . . . . . . . . 18  |-  NN  e.  _V
8584mptex 5925 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN  |->  ( abs `  ( A  /  (
m  +  1 ) ) ) )  e. 
_V
8685a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) )  e.  _V )
87 oveq2 6048 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  (
( abs `  A
)  /  m )  =  ( ( abs `  A )  /  n
) )
88 eqid 2404 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  |->  ( ( abs `  A )  /  m ) )  =  ( m  e.  NN  |->  ( ( abs `  A )  /  m
) )
89 ovex 6065 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs `  A )  /  n )  e. 
_V
9087, 88, 89fvmpt 5765 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( ( abs `  A
)  /  m ) ) `  n )  =  ( ( abs `  A )  /  n
) )
9190adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( abs `  A
)  /  m ) ) `  n )  =  ( ( abs `  A )  /  n
) )
9212adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  A  e.  CC )
9392abscld 12193 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  A )  e.  RR )
94 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
9593, 94nndivred 10004 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( abs `  A )  /  n )  e.  RR )
9691, 95eqeltrd 2478 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( abs `  A
)  /  m ) ) `  n )  e.  RR )
97 oveq1 6047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
m  +  1 )  =  ( n  + 
1 ) )
9897oveq2d 6056 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  ( A  /  ( m  + 
1 ) )  =  ( A  /  (
n  +  1 ) ) )
9998fveq2d 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  ( abs `  ( A  / 
( m  +  1 ) ) )  =  ( abs `  ( A  /  ( n  + 
1 ) ) ) )
100 eqid 2404 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  |->  ( abs `  ( A  /  (
m  +  1 ) ) ) )  =  ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) )
101 fvex 5701 . . . . . . . . . . . . . . . . . . 19  |-  ( abs `  ( A  /  (
n  +  1 ) ) )  e.  _V
10299, 100, 101fvmpt 5765 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) ) `  n )  =  ( abs `  ( A  /  ( n  + 
1 ) ) ) )
103102adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) ) `  n )  =  ( abs `  ( A  /  ( n  + 
1 ) ) ) )
10494nncnd 9972 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  CC )
10530a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  1  e.  CC )
106104, 105addcld 9063 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( n  +  1 )  e.  CC )
10794peano2nnd 9973 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  ( n  +  1 )  e.  NN )
108107nnne0d 10000 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( n  +  1 )  =/=  0 )
10992, 106, 108divcld 9746 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( A  /  ( n  + 
1 ) )  e.  CC )
110109abscld 12193 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  ( A  /  (
n  +  1 ) ) )  e.  RR )
111103, 110eqeltrd 2478 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) ) `  n )  e.  RR )
11292, 106, 108absdivd 12212 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  ( A  /  (
n  +  1 ) ) )  =  ( ( abs `  A
)  /  ( abs `  ( n  +  1 ) ) ) )
113107nnred 9971 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( n  +  1 )  e.  RR )
114107nnrpd 10603 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  n  e.  NN )  ->  ( n  +  1 )  e.  RR+ )
115114rpge0d 10608 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( n  +  1 ) )
116113, 115absidd 12180 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  ( n  +  1 ) )  =  ( n  +  1 ) )
117116oveq2d 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( abs `  A )  /  ( abs `  (
n  +  1 ) ) )  =  ( ( abs `  A
)  /  ( n  +  1 ) ) )
118112, 117eqtrd 2436 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  ( A  /  (
n  +  1 ) ) )  =  ( ( abs `  A
)  /  ( n  +  1 ) ) )
11994nnrpd 10603 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  RR+ )
12092absge0d 12201 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( abs `  A
) )
12194nnred 9971 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  RR )
122121lep1d 9898 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  n  <_ 
( n  +  1 ) )
123119, 114, 93, 120, 122lediv2ad 10626 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( abs `  A )  /  ( n  + 
1 ) )  <_ 
( ( abs `  A
)  /  n ) )
124118, 123eqbrtrd 4192 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  ( A  /  (
n  +  1 ) ) )  <_  (
( abs `  A
)  /  n ) )
125124, 103, 913brtr4d 4202 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) ) `  n )  <_  ( ( m  e.  NN  |->  ( ( abs `  A )  /  m ) ) `
 n ) )
126109absge0d 12201 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( abs `  ( A  /  ( n  + 
1 ) ) ) )
127126, 103breqtrrd 4198 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) ) `  n ) )
1281, 3, 83, 86, 96, 111, 125, 127climsqz2 12390 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) )  ~~>  0 )
12984mptex 5925 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN  |->  ( A  /  ( m  + 
1 ) ) )  e.  _V
130129a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( m  e.  NN  |->  ( A  /  (
m  +  1 ) ) )  e.  _V )
131 eqid 2404 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  |->  ( A  /  ( m  + 
1 ) ) )  =  ( m  e.  NN  |->  ( A  / 
( m  +  1 ) ) )
132 ovex 6065 . . . . . . . . . . . . . . . . . . 19  |-  ( A  /  ( n  + 
1 ) )  e. 
_V
13398, 131, 132fvmpt 5765 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( A  /  (
m  +  1 ) ) ) `  n
)  =  ( A  /  ( n  + 
1 ) ) )
134133adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( A  /  ( m  +  1 ) ) ) `  n )  =  ( A  / 
( n  +  1 ) ) )
135134, 109eqeltrd 2478 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( A  /  ( m  +  1 ) ) ) `  n )  e.  CC )
136134fveq2d 5691 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( abs `  ( ( m  e.  NN  |->  ( A  / 
( m  +  1 ) ) ) `  n ) )  =  ( abs `  ( A  /  ( n  + 
1 ) ) ) )
137103, 136eqtr4d 2439 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) ) `  n )  =  ( abs `  (
( m  e.  NN  |->  ( A  /  (
m  +  1 ) ) ) `  n
) ) )
1381, 3, 130, 86, 135, 137climabs0 12334 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( m  e.  NN  |->  ( A  / 
( m  +  1 ) ) )  ~~>  0  <->  (
m  e.  NN  |->  ( abs `  ( A  /  ( m  + 
1 ) ) ) )  ~~>  0 ) )
139128, 138mpbird 224 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  e.  NN  |->  ( A  /  (
m  +  1 ) ) )  ~~>  0 )
14030a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  CC )
14184mptex 5925 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) )  e.  _V
142141a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) )  e.  _V )
14398oveq1d 6055 . . . . . . . . . . . . . . . . 17  |-  ( m  =  n  ->  (
( A  /  (
m  +  1 ) )  +  1 )  =  ( ( A  /  ( n  + 
1 ) )  +  1 ) )
144 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) )  =  ( m  e.  NN  |->  ( ( A  /  ( m  + 
1 ) )  +  1 ) )
145 ovex 6065 . . . . . . . . . . . . . . . . 17  |-  ( ( A  /  ( n  +  1 ) )  +  1 )  e. 
_V
146143, 144, 145fvmpt 5765 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) `  n
)  =  ( ( A  /  ( n  +  1 ) )  +  1 ) )
147146adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) ) `  n )  =  ( ( A  /  ( n  + 
1 ) )  +  1 ) )
148134oveq1d 6055 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( m  e.  NN  |->  ( A  /  (
m  +  1 ) ) ) `  n
)  +  1 )  =  ( ( A  /  ( n  + 
1 ) )  +  1 ) )
149147, 148eqtr4d 2439 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) ) `  n )  =  ( ( ( m  e.  NN  |->  ( A  /  ( m  +  1 ) ) ) `  n )  +  1 ) )
1501, 3, 139, 140, 142, 135, 149climaddc1 12383 . . . . . . . . . . . . 13  |-  ( ph  ->  ( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) )  ~~>  ( 0  +  1 ) )
151 0p1e1 10049 . . . . . . . . . . . . 13  |-  ( 0  +  1 )  =  1
152150, 151syl6breq 4211 . . . . . . . . . . . 12  |-  ( ph  ->  ( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) )  ~~>  1 )
153152adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
m  e.  NN  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) )  ~~>  1 )
154 climres 12324 . . . . . . . . . . . 12  |-  ( ( r  e.  ZZ  /\  ( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) )  e.  _V )  ->  ( ( ( m  e.  NN  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) )  |`  ( ZZ>= `  r ) )  ~~>  1  <->  (
m  e.  NN  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) )  ~~>  1 ) )
15518, 141, 154sylancl 644 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( ( m  e.  NN  |->  ( ( A  /  ( m  + 
1 ) )  +  1 ) )  |`  ( ZZ>= `  r )
)  ~~>  1  <->  ( m  e.  NN  |->  ( ( A  /  ( m  + 
1 ) )  +  1 ) )  ~~>  1 ) )
156153, 155mpbird 224 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( m  e.  NN  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) )  |`  ( ZZ>=
`  r ) )  ~~>  1 )
15780, 156eqbrtrrd 4194 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
m  e.  ( ZZ>= `  r )  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) )  ~~>  1 )
15869a1i 11 . . . . . . . . . . 11  |-  ( 1  e.  RR  ->  1  e.  RR+ )
15919ellogdm 20483 . . . . . . . . . . 11  |-  ( 1  e.  ( CC  \ 
(  -oo (,] 0 ) )  <->  ( 1  e.  CC  /\  ( 1  e.  RR  ->  1  e.  RR+ ) ) )
16030, 158, 159mpbir2an 887 . . . . . . . . . 10  |-  1  e.  ( CC  \  (  -oo (,] 0 ) )
161160a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  1  e.  ( CC  \  (  -oo (,] 0 ) ) )
16216, 18, 21, 77, 157, 161climcncf 18883 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) )  o.  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  ~~>  ( ( log  |`  ( CC  \  (  -oo (,] 0
) ) ) ` 
1 ) )
16319logdmss 20486 . . . . . . . . . . 11  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
164163, 75sseldi 3306 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
r  e.  NN  /\  ( abs `  A )  <  r ) )  /\  m  e.  (
ZZ>= `  r ) )  ->  ( ( A  /  ( m  + 
1 ) )  +  1 )  e.  ( CC  \  { 0 } ) )
165 eqidd 2405 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
m  e.  ( ZZ>= `  r )  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) )  =  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )
166 logf1o 20415 . . . . . . . . . . . 12  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
167 f1of 5633 . . . . . . . . . . . 12  |-  ( log
: ( CC  \  { 0 } ) -1-1-onto-> ran 
log  ->  log : ( CC 
\  { 0 } ) --> ran  log )
168166, 167mp1i 12 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  log : ( CC  \  {
0 } ) --> ran 
log )
169168feqmptd 5738 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  log  =  ( x  e.  ( CC  \  {
0 } )  |->  ( log `  x ) ) )
170 fveq2 5687 . . . . . . . . . 10  |-  ( x  =  ( ( A  /  ( m  + 
1 ) )  +  1 )  ->  ( log `  x )  =  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) )
171164, 165, 169, 170fmptco 5860 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  ( log  o.  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  =  ( m  e.  (
ZZ>= `  r )  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) )
172 frn 5556 . . . . . . . . . 10  |-  ( ( m  e.  ( ZZ>= `  r )  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) ) : ( ZZ>= `  r
) --> ( CC  \ 
(  -oo (,] 0 ) )  ->  ran  ( m  e.  ( ZZ>= `  r
)  |->  ( ( A  /  ( m  + 
1 ) )  +  1 ) )  C_  ( CC  \  (  -oo (,] 0 ) ) )
173 cores 5332 . . . . . . . . . 10  |-  ( ran  ( m  e.  (
ZZ>= `  r )  |->  ( ( A  /  (
m  +  1 ) )  +  1 ) )  C_  ( CC  \  (  -oo (,] 0
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) )  o.  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  =  ( log  o.  (
m  e.  ( ZZ>= `  r )  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) )
17477, 172, 1733syl 19 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) )  o.  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  =  ( log  o.  (
m  e.  ( ZZ>= `  r )  |->  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) )
175 resmpt 5150 . . . . . . . . . 10  |-  ( (
ZZ>= `  r )  C_  NN  ->  ( ( m  e.  NN  |->  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  |`  ( ZZ>= `  r )
)  =  ( m  e.  ( ZZ>= `  r
)  |->  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) ) )
17678, 175syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) )  |`  ( ZZ>= `  r ) )  =  ( m  e.  (
ZZ>= `  r )  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) )
177171, 174, 1763eqtr4d 2446 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) )  o.  ( m  e.  ( ZZ>= `  r )  |->  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  =  ( ( m  e.  NN  |->  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) )  |`  ( ZZ>=
`  r ) ) )
178 fvres 5704 . . . . . . . . . 10  |-  ( 1  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  ( ( log  |`  ( CC  \ 
(  -oo (,] 0 ) ) ) `  1
)  =  ( log `  1 ) )
179160, 178mp1i 12 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) ) `
 1 )  =  ( log `  1
) )
180 log1 20433 . . . . . . . . 9  |-  ( log `  1 )  =  0
181179, 180syl6eq 2452 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) ) `
 1 )  =  0 )
182162, 177, 1813brtr3d 4201 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) )  |`  ( ZZ>= `  r ) )  ~~>  0 )
18384mptex 5925 . . . . . . . 8  |-  ( m  e.  NN  |->  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  e. 
_V
184 climres 12324 . . . . . . . 8  |-  ( ( r  e.  ZZ  /\  ( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) )  e.  _V )  ->  ( ( ( m  e.  NN  |->  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  |`  ( ZZ>= `  r )
)  ~~>  0  <->  ( m  e.  NN  |->  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) )  ~~>  0 ) )
18518, 183, 184sylancl 644 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
( ( m  e.  NN  |->  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) )  |`  ( ZZ>=
`  r ) )  ~~>  0  <->  ( m  e.  NN  |->  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) )  ~~>  0 ) )
186182, 185mpbid 202 . . . . . 6  |-  ( (
ph  /\  ( r  e.  NN  /\  ( abs `  A )  <  r
) )  ->  (
m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) )  ~~>  0 )
18715, 186rexlimddv 2794 . . . . 5  |-  ( ph  ->  ( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) )  ~~>  0 )
18812, 140addcld 9063 . . . . . 6  |-  ( ph  ->  ( A  +  1 )  e.  CC )
1898dmgmn0 24763 . . . . . 6  |-  ( ph  ->  ( A  +  1 )  =/=  0 )
190188, 189logcld 20421 . . . . 5  |-  ( ph  ->  ( log `  ( A  +  1 ) )  e.  CC )
19184mptex 5925 . . . . . 6  |-  ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) ) )  e. 
_V
192191a1i 11 . . . . 5  |-  ( ph  ->  ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) )  e.  _V )
193143fveq2d 5691 . . . . . . . 8  |-  ( m  =  n  ->  ( log `  ( ( A  /  ( m  + 
1 ) )  +  1 ) )  =  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )
194 eqid 2404 . . . . . . . 8  |-  ( m  e.  NN  |->  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  =  ( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) )
195 fvex 5701 . . . . . . . 8  |-  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) )  e.  _V
196193, 194, 195fvmpt 5765 . . . . . . 7  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) `  n )  =  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )
197196adantl 453 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) `  n )  =  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )
198109, 105addcld 9063 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( A  /  ( n  +  1 ) )  +  1 )  e.  CC )
1995adantr 452 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  A  e.  ( CC  \  ( ZZ  \  NN ) ) )
200199, 107dmgmdivn0 24765 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( A  /  ( n  +  1 ) )  +  1 )  =/=  0 )
201198, 200logcld 20421 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) )  e.  CC )
202197, 201eqeltrd 2478 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) `  n )  e.  CC )
203193oveq2d 6056 . . . . . . . 8  |-  ( m  =  n  ->  (
( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )
204 eqid 2404 . . . . . . . 8  |-  ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  (
( A  /  (
m  +  1 ) )  +  1 ) ) ) )  =  ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) )
205 ovex 6065 . . . . . . . 8  |-  ( ( log `  ( A  +  1 ) )  -  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )  e.  _V
206203, 204, 205fvmpt 5765 . . . . . . 7  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) ) `
 n )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )
207206adantl 453 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) ) `
 n )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )
208197oveq2d 6056 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( log `  ( A  +  1 ) )  -  ( ( m  e.  NN  |->  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) `  n ) )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )
209207, 208eqtr4d 2439 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) ) `
 n )  =  ( ( log `  ( A  +  1 ) )  -  ( ( m  e.  NN  |->  ( log `  ( ( A  /  ( m  +  1 ) )  +  1 ) ) ) `  n ) ) )
2101, 3, 187, 190, 192, 202, 209climsubc2 12387 . . . 4  |-  ( ph  ->  ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) )  ~~>  ( ( log `  ( A  +  1 ) )  -  0 ) )
211190subid1d 9356 . . . 4  |-  ( ph  ->  ( ( log `  ( A  +  1 ) )  -  0 )  =  ( log `  ( A  +  1 ) ) )
212210, 211breqtrd 4196 . . 3  |-  ( ph  ->  ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) )  ~~>  ( log `  ( A  +  1 ) ) )
213 elfznn 11036 . . . . . . 7  |-  ( k  e.  ( 1 ... n )  ->  k  e.  NN )
214213adantl 453 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
215 oveq1 6047 . . . . . . . . . . 11  |-  ( m  =  k  ->  (
m  +  1 )  =  ( k  +  1 ) )
216 id 20 . . . . . . . . . . 11  |-  ( m  =  k  ->  m  =  k )
217215, 216oveq12d 6058 . . . . . . . . . 10  |-  ( m  =  k  ->  (
( m  +  1 )  /  m )  =  ( ( k  +  1 )  / 
k ) )
218217fveq2d 5691 . . . . . . . . 9  |-  ( m  =  k  ->  ( log `  ( ( m  +  1 )  /  m ) )  =  ( log `  (
( k  +  1 )  /  k ) ) )
219218oveq2d 6056 . . . . . . . 8  |-  ( m  =  k  ->  (
( A  +  1 )  x.  ( log `  ( ( m  + 
1 )  /  m
) ) )  =  ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) ) )
220 oveq2 6048 . . . . . . . . . 10  |-  ( m  =  k  ->  (
( A  +  1 )  /  m )  =  ( ( A  +  1 )  / 
k ) )
221220oveq1d 6055 . . . . . . . . 9  |-  ( m  =  k  ->  (
( ( A  + 
1 )  /  m
)  +  1 )  =  ( ( ( A  +  1 )  /  k )  +  1 ) )
222221fveq2d 5691 . . . . . . . 8  |-  ( m  =  k  ->  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) )  =  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )
223219, 222oveq12d 6058 . . . . . . 7  |-  ( m  =  k  ->  (
( ( A  + 
1 )  x.  ( log `  ( ( m  +  1 )  /  m ) ) )  -  ( log `  (
( ( A  + 
1 )  /  m
)  +  1 ) ) )  =  ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) ) )
224 ovex 6065 . . . . . . 7  |-  ( ( ( A  +  1 )  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  e.  _V
225223, 4, 224fvmpt 5765 . . . . . 6  |-  ( k  e.  NN  ->  (
( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) ) `  k )  =  ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) ) )
226214, 225syl 16 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) ) `  k )  =  ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) ) )
22794, 1syl6eleq 2494 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  ( ZZ>= `  1 )
)
22812ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  CC )
22930a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  1  e.  CC )
230228, 229addcld 9063 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( A  +  1 )  e.  CC )
231214peano2nnd 9973 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
k  +  1 )  e.  NN )
232231nnrpd 10603 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
k  +  1 )  e.  RR+ )
233214nnrpd 10603 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  RR+ )
234232, 233rpdivcld 10621 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( k  +  1 )  /  k )  e.  RR+ )
235234relogcld 20471 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( k  +  1 )  / 
k ) )  e.  RR )
236235recnd 9070 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( k  +  1 )  / 
k ) )  e.  CC )
237230, 236mulcld 9064 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  1 )  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  e.  CC )
238214nncnd 9972 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  CC )
239214nnne0d 10000 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  =/=  0 )
240230, 238, 239divcld 9746 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  1 )  /  k )  e.  CC )
241240, 229addcld 9063 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  /  k
)  +  1 )  e.  CC )
2428ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( A  +  1 )  e.  ( CC  \ 
( ZZ  \  NN ) ) )
243242, 214dmgmdivn0 24765 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  /  k
)  +  1 )  =/=  0 )
244241, 243logcld 20421 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  e.  CC )
245237, 244subcld 9367 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  e.  CC )
246226, 227, 245fsumser 12479 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  =  (  seq  1
(  +  ,  ( m  e.  NN  |->  ( ( ( A  + 
1 )  x.  ( log `  ( ( m  +  1 )  /  m ) ) )  -  ( log `  (
( ( A  + 
1 )  /  m
)  +  1 ) ) ) ) ) `
 n ) )
247 fzfid 11267 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1 ... n )  e. 
Fin )
248247, 245fsumcl 12482 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  e.  CC )
249246, 248eqeltrrd 2479 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  (  seq  1 (  +  , 
( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) ) ) `  n
)  e.  CC )
250190adantr 452 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( log `  ( A  +  1 ) )  e.  CC )
251250, 201subcld 9367 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( log `  ( A  +  1 ) )  -  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )  e.  CC )
252207, 251eqeltrd 2478 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) ) `
 n )  e.  CC )
253228, 236mulcld 9064 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( A  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  e.  CC )
254228, 238, 239divcld 9746 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( A  /  k )  e.  CC )
255254, 229addcld 9063 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  /  k
)  +  1 )  e.  CC )
2565ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( CC  \  ( ZZ  \  NN ) ) )
257256, 214dmgmdivn0 24765 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  /  k
)  +  1 )  =/=  0 )
258255, 257logcld 20421 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( A  /  k )  +  1 ) )  e.  CC )
259253, 258subcld 9367 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) )  e.  CC )
260247, 259fsumcl 12482 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) )  e.  CC )
261248, 260nncand 9372 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( sum_ k  e.  ( 1 ... n ) ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  -  ( sum_ k  e.  ( 1 ... n ) ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  -  sum_ k  e.  ( 1 ... n ) ( ( A  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) ) ) )  =  sum_ k  e.  ( 1 ... n ) ( ( A  x.  ( log `  ( ( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  / 
k )  +  1 ) ) ) )
262237, 244, 253, 258sub4d 9416 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )  =  ( ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( A  x.  ( log `  ( ( k  +  1 )  /  k ) ) ) )  -  (
( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) )  -  ( log `  ( ( A  / 
k )  +  1 ) ) ) ) )
263228, 229pncan2d 9369 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  1 )  -  A )  =  1 )
264263oveq1d 6055 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  -  A
)  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  =  ( 1  x.  ( log `  ( ( k  +  1 )  / 
k ) ) ) )
265230, 228, 236subdird 9446 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  -  A
)  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  =  ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( A  x.  ( log `  ( ( k  +  1 )  /  k
) ) ) ) )
266236mulid2d 9062 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
1  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  =  ( log `  (
( k  +  1 )  /  k ) ) )
267264, 265, 2663eqtr3d 2444 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( A  x.  ( log `  ( ( k  +  1 )  /  k ) ) ) )  =  ( log `  ( ( k  +  1 )  /  k ) ) )
268267oveq1d 6055 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( A  x.  ( log `  ( ( k  +  1 )  /  k
) ) ) )  -  ( ( log `  ( ( ( A  +  1 )  / 
k )  +  1 ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )  =  ( ( log `  ( ( k  +  1 )  /  k ) )  -  ( ( log `  ( ( ( A  +  1 )  / 
k )  +  1 ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) ) )
269236, 244, 258subsubd 9395 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( k  +  1 )  /  k ) )  -  ( ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) ) )  =  ( ( ( log `  ( ( k  +  1 )  /  k
) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  +  ( log `  (
( A  /  k
)  +  1 ) ) ) )
270236, 244subcld 9367 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( k  +  1 )  /  k ) )  -  ( log `  ( ( ( A  +  1 )  / 
k )  +  1 ) ) )  e.  CC )
271270, 258addcomd 9224 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( log `  (
( k  +  1 )  /  k ) )  -  ( log `  ( ( ( A  +  1 )  / 
k )  +  1 ) ) )  +  ( log `  (
( A  /  k
)  +  1 ) ) )  =  ( ( log `  (
( A  /  k
)  +  1 ) )  +  ( ( log `  ( ( k  +  1 )  /  k ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) ) ) )
272258, 244, 236subsub2d 9396 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( A  /  k
)  +  1 ) )  -  ( ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  -  ( log `  (
( k  +  1 )  /  k ) ) ) )  =  ( ( log `  (
( A  /  k
)  +  1 ) )  +  ( ( log `  ( ( k  +  1 )  /  k ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) ) ) )
273231nncnd 9972 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
k  +  1 )  e.  CC )
274228, 273addcld 9063 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( A  +  ( k  +  1 ) )  e.  CC )
275231nnnn0d 10230 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
k  +  1 )  e.  NN0 )
276 dmgmaddn0 24760 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( CC 
\  ( ZZ  \  NN ) )  /\  (
k  +  1 )  e.  NN0 )  -> 
( A  +  ( k  +  1 ) )  =/=  0 )
277256, 275, 276syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( A  +  ( k  +  1 ) )  =/=  0 )
278274, 277logcld 20421 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( A  +  ( k  +  1 ) ) )  e.  CC )
279232relogcld 20471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( k  +  1 ) )  e.  RR )
280279recnd 9070 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( k  +  1 ) )  e.  CC )
281233relogcld 20471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  k )  e.  RR )
282281recnd 9070 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  k )  e.  CC )
283278, 280, 282nnncan2d 9402 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  k ) )  -  ( ( log `  (
k  +  1 ) )  -  ( log `  k ) ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  ( k  +  1 ) ) ) )
284230, 238, 238, 239divdird 9784 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  +  k )  /  k )  =  ( ( ( A  +  1 )  /  k )  +  ( k  /  k
) ) )
285228, 238, 229add32d 9244 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  k )  +  1 )  =  ( ( A  +  1 )  +  k ) )
286228, 238, 229addassd 9066 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  k )  +  1 )  =  ( A  +  ( k  +  1 ) ) )
287285, 286eqtr3d 2438 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  1 )  +  k )  =  ( A  +  ( k  +  1 ) ) )
288287oveq1d 6055 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  +  k )  /  k )  =  ( ( A  +  ( k  +  1 ) )  / 
k ) )
289238, 239dividd 9744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
k  /  k )  =  1 )
290289oveq2d 6056 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  /  k
)  +  ( k  /  k ) )  =  ( ( ( A  +  1 )  /  k )  +  1 ) )
291284, 288, 2903eqtr3rd 2445 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( A  + 
1 )  /  k
)  +  1 )  =  ( ( A  +  ( k  +  1 ) )  / 
k ) )
292291fveq2d 5691 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  =  ( log `  (
( A  +  ( k  +  1 ) )  /  k ) ) )
293 logdiv2 20465 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  +  ( k  +  1 ) )  e.  CC  /\  ( A  +  (
k  +  1 ) )  =/=  0  /\  k  e.  RR+ )  ->  ( log `  (
( A  +  ( k  +  1 ) )  /  k ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  k
) ) )
294274, 277, 233, 293syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( A  +  ( k  +  1 ) )  / 
k ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  k ) ) )
295292, 294eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  k ) ) )
296232, 233relogdivd 20474 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( k  +  1 )  / 
k ) )  =  ( ( log `  (
k  +  1 ) )  -  ( log `  k ) ) )
297295, 296oveq12d 6058 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) )  -  ( log `  ( ( k  +  1 )  /  k
) ) )  =  ( ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  k ) )  -  ( ( log `  ( k  +  1 ) )  -  ( log `  k ) ) ) )
298231nnne0d 10000 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
k  +  1 )  =/=  0 )
299228, 273, 273, 298divdird 9784 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  +  ( k  +  1 ) )  /  ( k  +  1 ) )  =  ( ( A  /  ( k  +  1 ) )  +  ( ( k  +  1 )  /  (
k  +  1 ) ) ) )
300273, 298dividd 9744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( k  +  1 )  /  ( k  +  1 ) )  =  1 )
301300oveq2d 6056 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  /  (
k  +  1 ) )  +  ( ( k  +  1 )  /  ( k  +  1 ) ) )  =  ( ( A  /  ( k  +  1 ) )  +  1 ) )
302299, 301eqtr2d 2437 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( A  /  (
k  +  1 ) )  +  1 )  =  ( ( A  +  ( k  +  1 ) )  / 
( k  +  1 ) ) )
303302fveq2d 5691 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( A  /  ( k  +  1 ) )  +  1 ) )  =  ( log `  (
( A  +  ( k  +  1 ) )  /  ( k  +  1 ) ) ) )
304 logdiv2 20465 . . . . . . . . . . . . . . 15  |-  ( ( ( A  +  ( k  +  1 ) )  e.  CC  /\  ( A  +  (
k  +  1 ) )  =/=  0  /\  ( k  +  1 )  e.  RR+ )  ->  ( log `  (
( A  +  ( k  +  1 ) )  /  ( k  +  1 ) ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  (
k  +  1 ) ) ) )
305274, 277, 232, 304syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( A  +  ( k  +  1 ) )  / 
( k  +  1 ) ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  ( k  +  1 ) ) ) )
306303, 305eqtrd 2436 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( log `  ( ( A  /  ( k  +  1 ) )  +  1 ) )  =  ( ( log `  ( A  +  ( k  +  1 ) ) )  -  ( log `  ( k  +  1 ) ) ) )
307283, 297, 3063eqtr4d 2446 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) )  -  ( log `  ( ( k  +  1 )  /  k
) ) )  =  ( log `  (
( A  /  (
k  +  1 ) )  +  1 ) ) )
308307oveq2d 6056 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( A  /  k
)  +  1 ) )  -  ( ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  -  ( log `  (
( k  +  1 )  /  k ) ) ) )  =  ( ( log `  (
( A  /  k
)  +  1 ) )  -  ( log `  ( ( A  / 
( k  +  1 ) )  +  1 ) ) ) )
309272, 308eqtr3d 2438 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( A  /  k
)  +  1 ) )  +  ( ( log `  ( ( k  +  1 )  /  k ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) ) )  =  ( ( log `  (
( A  /  k
)  +  1 ) )  -  ( log `  ( ( A  / 
( k  +  1 ) )  +  1 ) ) ) )
310269, 271, 3093eqtrd 2440 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( log `  (
( k  +  1 )  /  k ) )  -  ( ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) ) )  =  ( ( log `  (
( A  /  k
)  +  1 ) )  -  ( log `  ( ( A  / 
( k  +  1 ) )  +  1 ) ) ) )
311262, 268, 3103eqtrd 2440 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )  =  ( ( log `  ( ( A  /  k )  +  1 ) )  -  ( log `  (
( A  /  (
k  +  1 ) )  +  1 ) ) ) )
312311sumeq2dv 12452 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( ( ( A  +  1 )  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  ( ( A  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )  =  sum_ k  e.  ( 1 ... n ) ( ( log `  (
( A  /  k
)  +  1 ) )  -  ( log `  ( ( A  / 
( k  +  1 ) )  +  1 ) ) ) )
313247, 245, 259fsumsub 12526 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( ( ( A  +  1 )  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  ( ( A  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )  =  (
sum_ k  e.  ( 1 ... n ) ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  sum_ k  e.  ( 1 ... n ) ( ( A  x.  ( log `  ( ( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  / 
k )  +  1 ) ) ) ) )
314 oveq2 6048 . . . . . . . . . . 11  |-  ( x  =  k  ->  ( A  /  x )  =  ( A  /  k
) )
315314oveq1d 6055 . . . . . . . . . 10  |-  ( x  =  k  ->  (
( A  /  x
)  +  1 )  =  ( ( A  /  k )  +  1 ) )
316315fveq2d 5691 . . . . . . . . 9  |-  ( x  =  k  ->  ( log `  ( ( A  /  x )  +  1 ) )  =  ( log `  (
( A  /  k
)  +  1 ) ) )
317 oveq2 6048 . . . . . . . . . . 11  |-  ( x  =  ( k  +  1 )  ->  ( A  /  x )  =  ( A  /  (
k  +  1 ) ) )
318317oveq1d 6055 . . . . . . . . . 10  |-  ( x  =  ( k  +  1 )  ->  (
( A  /  x
)  +  1 )  =  ( ( A  /  ( k  +  1 ) )  +  1 ) )
319318fveq2d 5691 . . . . . . . . 9  |-  ( x  =  ( k  +  1 )  ->  ( log `  ( ( A  /  x )  +  1 ) )  =  ( log `  (
( A  /  (
k  +  1 ) )  +  1 ) ) )
320 oveq2 6048 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( A  /  x )  =  ( A  /  1
) )
321320oveq1d 6055 . . . . . . . . . 10  |-  ( x  =  1  ->  (
( A  /  x
)  +  1 )  =  ( ( A  /  1 )  +  1 ) )
322321fveq2d 5691 . . . . . . . . 9  |-  ( x  =  1  ->  ( log `  ( ( A  /  x )  +  1 ) )  =  ( log `  (
( A  /  1
)  +  1 ) ) )
323 oveq2 6048 . . . . . . . . . . 11  |-  ( x  =  ( n  + 
1 )  ->  ( A  /  x )  =  ( A  /  (
n  +  1 ) ) )
324323oveq1d 6055 . . . . . . . . . 10  |-  ( x  =  ( n  + 
1 )  ->  (
( A  /  x
)  +  1 )  =  ( ( A  /  ( n  + 
1 ) )  +  1 ) )
325324fveq2d 5691 . . . . . . . . 9  |-  ( x  =  ( n  + 
1 )  ->  ( log `  ( ( A  /  x )  +  1 ) )  =  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )
32694nnzd 10330 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  ZZ )
327107, 1syl6eleq 2494 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( n  +  1 )  e.  ( ZZ>= `  1 )
)
32812ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  A  e.  CC )
329 elfznn 11036 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... ( n  +  1 ) )  ->  x  e.  NN )
330329adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  x  e.  NN )
331330nncnd 9972 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  x  e.  CC )
332330nnne0d 10000 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  x  =/=  0 )
333328, 331, 332divcld 9746 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  ( A  /  x )  e.  CC )
33430a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  1  e.  CC )
335333, 334addcld 9063 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  (
( A  /  x
)  +  1 )  e.  CC )
3365ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  A  e.  ( CC  \  ( ZZ  \  NN ) ) )
337336, 330dmgmdivn0 24765 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  (
( A  /  x
)  +  1 )  =/=  0 )
338335, 337logcld 20421 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... (
n  +  1 ) ) )  ->  ( log `  ( ( A  /  x )  +  1 ) )  e.  CC )
339316, 319, 322, 325, 326, 327, 338fsumtscop 12538 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( log `  ( ( A  / 
k )  +  1 ) )  -  ( log `  ( ( A  /  ( k  +  1 ) )  +  1 ) ) )  =  ( ( log `  ( ( A  / 
1 )  +  1 ) )  -  ( log `  ( ( A  /  ( n  + 
1 ) )  +  1 ) ) ) )
34092div1d 9738 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( A  /  1 )  =  A )
341340oveq1d 6055 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( A  /  1 )  +  1 )  =  ( A  +  1 ) )
342341fveq2d 5691 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( log `  ( ( A  / 
1 )  +  1 ) )  =  ( log `  ( A  +  1 ) ) )
343342oveq1d 6055 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( log `  ( ( A  /  1 )  +  1 ) )  -  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )
344339, 343eqtrd 2436 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( log `  ( ( A  / 
k )  +  1 ) )  -  ( log `  ( ( A  /  ( k  +  1 ) )  +  1 ) ) )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  /  ( n  + 
1 ) )  +  1 ) ) ) )
345312, 313, 3443eqtr3d 2444 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( sum_ k  e.  ( 1 ... n ) ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  -  sum_ k  e.  ( 1 ... n ) ( ( A  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) ) )  =  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )
346345oveq2d 6056 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( sum_ k  e.  ( 1 ... n ) ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  -  ( sum_ k  e.  ( 1 ... n ) ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  -  sum_ k  e.  ( 1 ... n ) ( ( A  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) ) ) )  =  ( sum_ k  e.  ( 1 ... n
) ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  /  ( n  + 
1 ) )  +  1 ) ) ) ) )
347261, 346eqtr3d 2438 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) )  =  ( sum_ k  e.  ( 1 ... n
) ( ( ( A  +  1 )  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( ( A  +  1 )  /  k )  +  1 ) ) )  -  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  /  ( n  + 
1 ) )  +  1 ) ) ) ) )
348218oveq2d 6056 . . . . . . . 8  |-  ( m  =  k  ->  ( A  x.  ( log `  ( ( m  + 
1 )  /  m
) ) )  =  ( A  x.  ( log `  ( ( k  +  1 )  / 
k ) ) ) )
349 oveq2 6048 . . . . . . . . . 10  |-  ( m  =  k  ->  ( A  /  m )  =  ( A  /  k
) )
350349oveq1d 6055 . . . . . . . . 9  |-  ( m  =  k  ->  (
( A  /  m
)  +  1 )  =  ( ( A  /  k )  +  1 ) )
351350fveq2d 5691 . . . . . . . 8  |-  ( m  =  k  ->  ( log `  ( ( A  /  m )  +  1 ) )  =  ( log `  (
( A  /  k
)  +  1 ) ) )
352348, 351oveq12d 6058 . . . . . . 7  |-  ( m  =  k  ->  (
( A  x.  ( log `  ( ( m  +  1 )  /  m ) ) )  -  ( log `  (
( A  /  m
)  +  1 ) ) )  =  ( ( A  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( A  /  k
)  +  1 ) ) ) )
353 lgamcvg.g . . . . . . 7  |-  G  =  ( m  e.  NN  |->  ( ( A  x.  ( log `  ( ( m  +  1 )  /  m ) ) )  -  ( log `  ( ( A  /  m )  +  1 ) ) ) )
354 ovex 6065 . . . . . . 7  |-  ( ( A  x.  ( log `  ( ( k  +  1 )  /  k
) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) )  e.  _V
355352, 353, 354fvmpt 5765 . . . . . 6  |-  ( k  e.  NN  ->  ( G `  k )  =  ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )
356214, 355syl 16 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ( G `  k )  =  ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) ) )
357356, 227, 259fsumser 12479 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) ( ( A  x.  ( log `  (
( k  +  1 )  /  k ) ) )  -  ( log `  ( ( A  /  k )  +  1 ) ) )  =  (  seq  1
(  +  ,  G
) `  n )
)
358207eqcomd 2409 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( log `  ( A  +  1 ) )  -  ( log `  (
( A  /  (
n  +  1 ) )  +  1 ) ) )  =  ( ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) ) `
 n ) )
359246, 358oveq12d 6058 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ( sum_ k  e.  ( 1 ... n ) ( ( ( A  + 
1 )  x.  ( log `  ( ( k  +  1 )  / 
k ) ) )  -  ( log `  (
( ( A  + 
1 )  /  k
)  +  1 ) ) )  -  (
( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( n  +  1 ) )  +  1 ) ) ) )  =  ( (  seq  1 (  +  , 
( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) ) ) `  n
)  -  ( ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )  -  ( log `  ( ( A  / 
( m  +  1 ) )  +  1 ) ) ) ) `
 n ) ) )
360347, 357, 3593eqtr3d 2444 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  (  seq  1 (  +  ,  G ) `  n
)  =  ( (  seq  1 (  +  ,  ( m  e.  NN  |->  ( ( ( A  +  1 )  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( ( A  +  1 )  /  m )  +  1 ) ) ) ) ) `  n
)  -  ( ( m  e.  NN  |->  ( ( log `  ( A  +  1 ) )