Metamath Proof Explorer

Theorem lgamcvg2

Description: The series G converges to log_G ( A + 1 ) . (Contributed by Mario Carneiro, 9-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 lgamcvg2 
|- ( ph -> seq 1 ( + , G ) ~~> ( log_G ` ( A + 1 ) ) )

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 eqid 
 |-  ( 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 ) ) ) )
6 1nn0 
 |-  1 e. NN0
7 6 a1i 
 |-  ( ph -> 1 e. NN0 )
8 2 7 dmgmaddnn0 
 |-  ( ph -> ( A + 1 ) e. ( CC \ ( ZZ \ NN ) ) )
9 5 8 lgamcvg 
 |-  ( 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 
 |-  seq 1 ( + , G ) e. _V
11 10 a1i 
 |-  ( ph -> seq 1 ( + , G ) e. _V )
12 2 eldifad 
 |-  ( ph -> A e. CC )
13 12 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
14 arch 
 |-  ( ( abs ` A ) e. RR -> E. r e. NN ( abs ` A ) < r )
15 13 14 syl 
 |-  ( ph -> E. r e. NN ( abs ` A ) < r )
16 eqid 
 |-  ( ZZ>= ` r ) = ( ZZ>= ` r )
17 simprl 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> r e. NN )
18 17 nnzd 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> r e. ZZ )
19 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
20 19 logcn 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC )
21 20 a1i 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) )
22 eqid 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
23 22 dvlog2lem 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
24 12 ad2antrr 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> A e. CC )
25 eluznn 
 |-  ( ( r e. NN /\ m e. ( ZZ>= ` r ) ) -> m e. NN )
26 25 ex 
 |-  ( r e. NN -> ( m e. ( ZZ>= ` r ) -> m e. NN ) )
27 26 ad2antrl 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( m e. ( ZZ>= ` r ) -> m e. NN ) )
28 27 imp 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> m e. NN )
29 28 nncnd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> m e. CC )
30 1cnd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> 1 e. CC )
31 29 30 addcld 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( m + 1 ) e. CC )
32 28 peano2nnd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( m + 1 ) e. NN )
33 32 nnne0d 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( m + 1 ) =/= 0 )
34 24 31 33 divcld 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( A / ( m + 1 ) ) e. CC )
35 34 30 addcld 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( A / ( m + 1 ) ) + 1 ) e. CC )
36 ax-1cn 
 |-  1 e. CC
37 eqid 
 |-  ( abs o. - ) = ( abs o. - )
38 37 cnmetdval 
 |-  ( ( ( ( A / ( m + 1 ) ) + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( A / ( m + 1 ) ) + 1 ) ( abs o. - ) 1 ) = ( abs ` ( ( ( A / ( m + 1 ) ) + 1 ) - 1 ) ) )
39 35 36 38 sylancl 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( ( A / ( m + 1 ) ) + 1 ) ( abs o. - ) 1 ) = ( abs ` ( ( ( A / ( m + 1 ) ) + 1 ) - 1 ) ) )
40 34 30 pncand 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( ( A / ( m + 1 ) ) + 1 ) - 1 ) = ( A / ( m + 1 ) ) )
41 40 fveq2d 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` ( ( ( A / ( m + 1 ) ) + 1 ) - 1 ) ) = ( abs ` ( A / ( m + 1 ) ) ) )
42 24 31 33 absdivd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` ( A / ( m + 1 ) ) ) = ( ( abs ` A ) / ( abs ` ( m + 1 ) ) ) )
43 32 nnred 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( m + 1 ) e. RR )
44 32 nnrpd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( m + 1 ) e. RR+ )
45 44 rpge0d 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> 0 <_ ( m + 1 ) )
46 43 45 absidd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` ( m + 1 ) ) = ( m + 1 ) )
47 46 oveq2d 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( abs ` A ) / ( abs ` ( m + 1 ) ) ) = ( ( abs ` A ) / ( m + 1 ) ) )
48 42 47 eqtrd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` ( A / ( m + 1 ) ) ) = ( ( abs ` A ) / ( m + 1 ) ) )
49 39 41 48 3eqtrd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( ( A / ( m + 1 ) ) + 1 ) ( abs o. - ) 1 ) = ( ( abs ` A ) / ( m + 1 ) ) )
50 13 ad2antrr 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` A ) e. RR )
51 17 adantr 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> r e. NN )
52 51 nnred 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> r e. RR )
53 simplrr 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` A ) < r )
54 eluzle 
 |-  ( m e. ( ZZ>= ` r ) -> r <_ m )
55 54 adantl 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> r <_ m )
56 nnleltp1 
 |-  ( ( r e. NN /\ m e. NN ) -> ( r <_ m <-> r < ( m + 1 ) ) )
57 51 28 56 syl2anc 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( r <_ m <-> r < ( m + 1 ) ) )
58 55 57 mpbid 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> r < ( m + 1 ) )
59 50 52 43 53 58 lttrd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` A ) < ( m + 1 ) )
60 31 mulid1d 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( m + 1 ) x. 1 ) = ( m + 1 ) )
61 59 60 breqtrrd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs ` A ) < ( ( m + 1 ) x. 1 ) )
62 1red 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> 1 e. RR )
63 50 62 44 ltdivmuld 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( ( abs ` A ) / ( m + 1 ) ) < 1 <-> ( abs ` A ) < ( ( m + 1 ) x. 1 ) ) )
64 61 63 mpbird 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( abs ` A ) / ( m + 1 ) ) < 1 )
65 49 64 eqbrtrd 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( ( A / ( m + 1 ) ) + 1 ) ( abs o. - ) 1 ) < 1 )
66 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
67 66 a1i 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
68 1rp 
 |-  1 e. RR+
69 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
70 68 69 mp1i 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> 1 e. RR* )
71 elbl3 
 |-  ( ( ( ( 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 ) )
72 67 70 30 35 71 syl22anc 
 |-  ( ( ( 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 ) )
73 65 72 mpbird 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( A / ( m + 1 ) ) + 1 ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
74 23 73 sselid 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( A / ( m + 1 ) ) + 1 ) e. ( CC \ ( -oo (,] 0 ) ) )
75 74 fmpttd 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( m e. ( ZZ>= ` r ) |-> ( ( A / ( m + 1 ) ) + 1 ) ) : ( ZZ>= ` r ) --> ( CC \ ( -oo (,] 0 ) ) )
76 27 ssrdv 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( ZZ>= ` r ) C_ NN )
77 76 resmptd 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) |` ( ZZ>= ` r ) ) = ( m e. ( ZZ>= ` r ) |-> ( ( A / ( m + 1 ) ) + 1 ) ) )
78 nnex 
 |-  NN e. _V
79 78 mptex 
 |-  ( m e. NN |-> ( A / ( m + 1 ) ) ) e. _V
80 79 a1i 
 |-  ( ph -> ( m e. NN |-> ( A / ( m + 1 ) ) ) e. _V )
81 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
82 81 oveq2d 
 |-  ( m = n -> ( A / ( m + 1 ) ) = ( A / ( n + 1 ) ) )
83 eqid 
 |-  ( m e. NN |-> ( A / ( m + 1 ) ) ) = ( m e. NN |-> ( A / ( m + 1 ) ) )
84 ovex 
 |-  ( A / ( n + 1 ) ) e. _V
85 82 83 84 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( A / ( m + 1 ) ) ) ` n ) = ( A / ( n + 1 ) ) )
86 85 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( A / ( m + 1 ) ) ) ` n ) = ( A / ( n + 1 ) ) )
87 3 4 12 4 80 86 divcnvshft 
 |-  ( ph -> ( m e. NN |-> ( A / ( m + 1 ) ) ) ~~> 0 )
88 1cnd 
 |-  ( ph -> 1 e. CC )
89 78 mptex 
 |-  ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) e. _V
90 89 a1i 
 |-  ( ph -> ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) e. _V )
91 12 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. CC )
92 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
93 92 nncnd 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
94 1cnd 
 |-  ( ( ph /\ n e. NN ) -> 1 e. CC )
95 93 94 addcld 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. CC )
96 92 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
97 96 nnne0d 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) =/= 0 )
98 91 95 97 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( n + 1 ) ) e. CC )
99 86 98 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( A / ( m + 1 ) ) ) ` n ) e. CC )
100 82 oveq1d 
 |-  ( m = n -> ( ( A / ( m + 1 ) ) + 1 ) = ( ( A / ( n + 1 ) ) + 1 ) )
101 eqid 
 |-  ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) = ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) )
102 ovex 
 |-  ( ( A / ( n + 1 ) ) + 1 ) e. _V
103 100 101 102 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) ` n ) = ( ( A / ( n + 1 ) ) + 1 ) )
104 103 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) ` n ) = ( ( A / ( n + 1 ) ) + 1 ) )
105 86 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( m e. NN |-> ( A / ( m + 1 ) ) ) ` n ) + 1 ) = ( ( A / ( n + 1 ) ) + 1 ) )
106 104 105 eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) ` n ) = ( ( ( m e. NN |-> ( A / ( m + 1 ) ) ) ` n ) + 1 ) )
107 3 4 87 88 90 99 106 climaddc1 
 |-  ( ph -> ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) ~~> ( 0 + 1 ) )
108 0p1e1 
 |-  ( 0 + 1 ) = 1
109 107 108 breqtrdi 
 |-  ( ph -> ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) ~~> 1 )
110 109 adantr 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) ~~> 1 )
111 climres 
 |-  ( ( 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 ) )
112 18 89 111 sylancl 
 |-  ( ( 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 ) )
113 110 112 mpbird 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( ( m e. NN |-> ( ( A / ( m + 1 ) ) + 1 ) ) |` ( ZZ>= ` r ) ) ~~> 1 )
114 77 113 eqbrtrrd 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( m e. ( ZZ>= ` r ) |-> ( ( A / ( m + 1 ) ) + 1 ) ) ~~> 1 )
115 68 a1i 
 |-  ( 1 e. RR -> 1 e. RR+ )
116 19 ellogdm 
 |-  ( 1 e. ( CC \ ( -oo (,] 0 ) ) <-> ( 1 e. CC /\ ( 1 e. RR -> 1 e. RR+ ) ) )
117 36 115 116 mpbir2an 
 |-  1 e. ( CC \ ( -oo (,] 0 ) )
118 117 a1i 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> 1 e. ( CC \ ( -oo (,] 0 ) ) )
119 16 18 21 75 114 118 climcncf 
 |-  ( ( 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 ) )
120 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
121 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
122 120 121 mp1i 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> log : ( CC \ { 0 } ) --> ran log )
123 19 logdmss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
124 123 74 sselid 
 |-  ( ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) /\ m e. ( ZZ>= ` r ) ) -> ( ( A / ( m + 1 ) ) + 1 ) e. ( CC \ { 0 } ) )
125 122 124 cofmpt 
 |-  ( ( 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 ) ) ) )
126 frn 
 |-  ( ( 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 ) ) )
127 cores 
 |-  ( 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 ) ) ) )
128 75 126 127 3syl 
 |-  ( ( 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 ) ) ) )
129 76 resmptd 
 |-  ( ( 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 ) ) ) )
130 125 128 129 3eqtr4d 
 |-  ( ( 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 ) ) )
131 fvres 
 |-  ( 1 e. ( CC \ ( -oo (,] 0 ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` 1 ) = ( log ` 1 ) )
132 117 131 mp1i 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` 1 ) = ( log ` 1 ) )
133 log1 
 |-  ( log ` 1 ) = 0
134 132 133 eqtrdi 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` 1 ) = 0 )
135 119 130 134 3brtr3d 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) |` ( ZZ>= ` r ) ) ~~> 0 )
136 78 mptex 
 |-  ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) e. _V
137 climres 
 |-  ( ( 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 ) )
138 18 136 137 sylancl 
 |-  ( ( 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 ) )
139 135 138 mpbid 
 |-  ( ( ph /\ ( r e. NN /\ ( abs ` A ) < r ) ) -> ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ~~> 0 )
140 15 139 rexlimddv 
 |-  ( ph -> ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ~~> 0 )
141 12 88 addcld 
 |-  ( ph -> ( A + 1 ) e. CC )
142 8 dmgmn0 
 |-  ( ph -> ( A + 1 ) =/= 0 )
143 141 142 logcld 
 |-  ( ph -> ( log ` ( A + 1 ) ) e. CC )
144 78 mptex 
 |-  ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) e. _V
145 144 a1i 
 |-  ( ph -> ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) e. _V )
146 82 fvoveq1d 
 |-  ( m = n -> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) = ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) )
147 eqid 
 |-  ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) = ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) )
148 fvex 
 |-  ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) e. _V
149 146 147 148 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ` n ) = ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) )
150 149 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ` n ) = ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) )
151 98 94 addcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A / ( n + 1 ) ) + 1 ) e. CC )
152 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. ( CC \ ( ZZ \ NN ) ) )
153 152 96 dmgmdivn0 
 |-  ( ( ph /\ n e. NN ) -> ( ( A / ( n + 1 ) ) + 1 ) =/= 0 )
154 151 153 logcld 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) e. CC )
155 150 154 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ` n ) e. CC )
156 146 oveq2d 
 |-  ( m = n -> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) = ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) )
157 eqid 
 |-  ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) = ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) )
158 ovex 
 |-  ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) e. _V
159 156 157 158 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ` n ) = ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) )
160 159 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ` n ) = ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) )
161 150 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( log ` ( A + 1 ) ) - ( ( m e. NN |-> ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ` n ) ) = ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) )
162 160 161 eqtr4d 
 |-  ( ( 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 ) ) )
163 3 4 140 143 145 155 162 climsubc2 
 |-  ( ph -> ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ~~> ( ( log ` ( A + 1 ) ) - 0 ) )
164 143 subid1d 
 |-  ( ph -> ( ( log ` ( A + 1 ) ) - 0 ) = ( log ` ( A + 1 ) ) )
165 163 164 breqtrd 
 |-  ( ph -> ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ~~> ( log ` ( A + 1 ) ) )
166 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
167 166 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
168 oveq1 
 |-  ( m = k -> ( m + 1 ) = ( k + 1 ) )
169 id 
 |-  ( m = k -> m = k )
170 168 169 oveq12d 
 |-  ( m = k -> ( ( m + 1 ) / m ) = ( ( k + 1 ) / k ) )
171 170 fveq2d 
 |-  ( m = k -> ( log ` ( ( m + 1 ) / m ) ) = ( log ` ( ( k + 1 ) / k ) ) )
172 171 oveq2d 
 |-  ( m = k -> ( ( A + 1 ) x. ( log ` ( ( m + 1 ) / m ) ) ) = ( ( A + 1 ) x. ( log ` ( ( k + 1 ) / k ) ) ) )
173 oveq2 
 |-  ( m = k -> ( ( A + 1 ) / m ) = ( ( A + 1 ) / k ) )
174 173 fvoveq1d 
 |-  ( m = k -> ( log ` ( ( ( A + 1 ) / m ) + 1 ) ) = ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) )
175 172 174 oveq12d 
 |-  ( 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 ) ) ) )
176 ovex 
 |-  ( ( ( A + 1 ) x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) ) e. _V
177 175 5 176 fvmpt 
 |-  ( 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 ) ) ) )
178 167 177 syl 
 |-  ( ( ( 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 ) ) ) )
179 92 3 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
180 12 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. CC )
181 1cnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> 1 e. CC )
182 180 181 addcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( A + 1 ) e. CC )
183 167 peano2nnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k + 1 ) e. NN )
184 183 nnrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k + 1 ) e. RR+ )
185 167 nnrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. RR+ )
186 184 185 rpdivcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( k + 1 ) / k ) e. RR+ )
187 186 relogcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( k + 1 ) / k ) ) e. RR )
188 187 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( k + 1 ) / k ) ) e. CC )
189 182 188 mulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + 1 ) x. ( log ` ( ( k + 1 ) / k ) ) ) e. CC )
190 167 nncnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. CC )
191 167 nnne0d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k =/= 0 )
192 182 190 191 divcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + 1 ) / k ) e. CC )
193 192 181 addcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) / k ) + 1 ) e. CC )
194 8 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( A + 1 ) e. ( CC \ ( ZZ \ NN ) ) )
195 194 167 dmgmdivn0 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) / k ) + 1 ) =/= 0 )
196 193 195 logcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) e. CC )
197 189 196 subcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) ) e. CC )
198 178 179 197 fsumser 
 |-  ( ( 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 ) )
199 fzfid 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. Fin )
200 199 197 fsumcl 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) ( ( ( A + 1 ) x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) ) e. CC )
201 198 200 eqeltrrd 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( m e. NN |-> ( ( ( A + 1 ) x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( ( A + 1 ) / m ) + 1 ) ) ) ) ) ` n ) e. CC )
202 143 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( A + 1 ) ) e. CC )
203 202 154 subcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) e. CC )
204 160 203 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ` n ) e. CC )
205 180 188 mulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( A x. ( log ` ( ( k + 1 ) / k ) ) ) e. CC )
206 180 190 191 divcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( A / k ) e. CC )
207 206 181 addcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A / k ) + 1 ) e. CC )
208 2 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
209 208 167 dmgmdivn0 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A / k ) + 1 ) =/= 0 )
210 207 209 logcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( A / k ) + 1 ) ) e. CC )
211 205 210 subcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. CC )
212 199 211 fsumcl 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. CC )
213 200 212 nncand 
 |-  ( ( 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 ) ) ) )
214 189 196 205 210 sub4d 
 |-  ( ( ( 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 ) ) ) ) )
215 180 181 pncan2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + 1 ) - A ) = 1 )
216 215 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) - A ) x. ( log ` ( ( k + 1 ) / k ) ) ) = ( 1 x. ( log ` ( ( k + 1 ) / k ) ) ) )
217 182 180 188 subdird 
 |-  ( ( ( 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 ) ) ) ) )
218 188 mulid2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( 1 x. ( log ` ( ( k + 1 ) / k ) ) ) = ( log ` ( ( k + 1 ) / k ) ) )
219 216 217 218 3eqtr3d 
 |-  ( ( ( 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 ) ) )
220 219 oveq1d 
 |-  ( ( ( 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 ) ) ) ) )
221 188 196 210 subsubd 
 |-  ( ( ( 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 ) ) ) )
222 188 196 subcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( log ` ( ( k + 1 ) / k ) ) - ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) ) e. CC )
223 222 210 addcomd 
 |-  ( ( ( 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 ) ) ) ) )
224 210 196 188 subsub2d 
 |-  ( ( ( 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 ) ) ) ) )
225 183 nncnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k + 1 ) e. CC )
226 180 225 addcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( A + ( k + 1 ) ) e. CC )
227 183 nnnn0d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k + 1 ) e. NN0 )
228 dmgmaddn0 
 |-  ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ ( k + 1 ) e. NN0 ) -> ( A + ( k + 1 ) ) =/= 0 )
229 208 227 228 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( A + ( k + 1 ) ) =/= 0 )
230 226 229 logcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( A + ( k + 1 ) ) ) e. CC )
231 184 relogcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( k + 1 ) ) e. RR )
232 231 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( k + 1 ) ) e. CC )
233 185 relogcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` k ) e. RR )
234 233 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` k ) e. CC )
235 230 232 234 nnncan2d 
 |-  ( ( ( 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 ) ) ) )
236 182 190 190 191 divdird 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) + k ) / k ) = ( ( ( A + 1 ) / k ) + ( k / k ) ) )
237 180 190 181 add32d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + k ) + 1 ) = ( ( A + 1 ) + k ) )
238 180 190 181 addassd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + k ) + 1 ) = ( A + ( k + 1 ) ) )
239 237 238 eqtr3d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + 1 ) + k ) = ( A + ( k + 1 ) ) )
240 239 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) + k ) / k ) = ( ( A + ( k + 1 ) ) / k ) )
241 190 191 dividd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k / k ) = 1 )
242 241 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) / k ) + ( k / k ) ) = ( ( ( A + 1 ) / k ) + 1 ) )
243 236 240 242 3eqtr3rd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A + 1 ) / k ) + 1 ) = ( ( A + ( k + 1 ) ) / k ) )
244 243 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) = ( log ` ( ( A + ( k + 1 ) ) / k ) ) )
245 logdiv2 
 |-  ( ( ( A + ( k + 1 ) ) e. CC /\ ( A + ( k + 1 ) ) =/= 0 /\ k e. RR+ ) -> ( log ` ( ( A + ( k + 1 ) ) / k ) ) = ( ( log ` ( A + ( k + 1 ) ) ) - ( log ` k ) ) )
246 226 229 185 245 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( A + ( k + 1 ) ) / k ) ) = ( ( log ` ( A + ( k + 1 ) ) ) - ( log ` k ) ) )
247 244 246 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) = ( ( log ` ( A + ( k + 1 ) ) ) - ( log ` k ) ) )
248 184 185 relogdivd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( k + 1 ) / k ) ) = ( ( log ` ( k + 1 ) ) - ( log ` k ) ) )
249 247 248 oveq12d 
 |-  ( ( ( 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 ) ) ) )
250 183 nnne0d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k + 1 ) =/= 0 )
251 180 225 225 250 divdird 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A + ( k + 1 ) ) / ( k + 1 ) ) = ( ( A / ( k + 1 ) ) + ( ( k + 1 ) / ( k + 1 ) ) ) )
252 225 250 dividd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( k + 1 ) / ( k + 1 ) ) = 1 )
253 252 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A / ( k + 1 ) ) + ( ( k + 1 ) / ( k + 1 ) ) ) = ( ( A / ( k + 1 ) ) + 1 ) )
254 251 253 eqtr2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( A / ( k + 1 ) ) + 1 ) = ( ( A + ( k + 1 ) ) / ( k + 1 ) ) )
255 254 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( A / ( k + 1 ) ) + 1 ) ) = ( log ` ( ( A + ( k + 1 ) ) / ( k + 1 ) ) ) )
256 logdiv2 
 |-  ( ( ( 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 ) ) ) )
257 226 229 184 256 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( A + ( k + 1 ) ) / ( k + 1 ) ) ) = ( ( log ` ( A + ( k + 1 ) ) ) - ( log ` ( k + 1 ) ) ) )
258 255 257 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( log ` ( ( A / ( k + 1 ) ) + 1 ) ) = ( ( log ` ( A + ( k + 1 ) ) ) - ( log ` ( k + 1 ) ) ) )
259 235 249 258 3eqtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( log ` ( ( ( A + 1 ) / k ) + 1 ) ) - ( log ` ( ( k + 1 ) / k ) ) ) = ( log ` ( ( A / ( k + 1 ) ) + 1 ) ) )
260 259 oveq2d 
 |-  ( ( ( 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 ) ) ) )
261 224 260 eqtr3d 
 |-  ( ( ( 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 ) ) ) )
262 221 223 261 3eqtrd 
 |-  ( ( ( 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 ) ) ) )
263 214 220 262 3eqtrd 
 |-  ( ( ( 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 ) ) ) )
264 263 sumeq2dv 
 |-  ( ( 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 ) ) ) )
265 199 197 211 fsumsub 
 |-  ( ( 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 ) ) ) ) )
266 oveq2 
 |-  ( x = k -> ( A / x ) = ( A / k ) )
267 266 fvoveq1d 
 |-  ( x = k -> ( log ` ( ( A / x ) + 1 ) ) = ( log ` ( ( A / k ) + 1 ) ) )
268 oveq2 
 |-  ( x = ( k + 1 ) -> ( A / x ) = ( A / ( k + 1 ) ) )
269 268 fvoveq1d 
 |-  ( x = ( k + 1 ) -> ( log ` ( ( A / x ) + 1 ) ) = ( log ` ( ( A / ( k + 1 ) ) + 1 ) ) )
270 oveq2 
 |-  ( x = 1 -> ( A / x ) = ( A / 1 ) )
271 270 fvoveq1d 
 |-  ( x = 1 -> ( log ` ( ( A / x ) + 1 ) ) = ( log ` ( ( A / 1 ) + 1 ) ) )
272 oveq2 
 |-  ( x = ( n + 1 ) -> ( A / x ) = ( A / ( n + 1 ) ) )
273 272 fvoveq1d 
 |-  ( x = ( n + 1 ) -> ( log ` ( ( A / x ) + 1 ) ) = ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) )
274 92 nnzd 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
275 96 3 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. ( ZZ>= ` 1 ) )
276 12 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> A e. CC )
277 elfznn 
 |-  ( x e. ( 1 ... ( n + 1 ) ) -> x e. NN )
278 277 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> x e. NN )
279 278 nncnd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> x e. CC )
280 278 nnne0d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> x =/= 0 )
281 276 279 280 divcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> ( A / x ) e. CC )
282 1cnd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> 1 e. CC )
283 281 282 addcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> ( ( A / x ) + 1 ) e. CC )
284 2 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
285 284 278 dmgmdivn0 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> ( ( A / x ) + 1 ) =/= 0 )
286 283 285 logcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... ( n + 1 ) ) ) -> ( log ` ( ( A / x ) + 1 ) ) e. CC )
287 267 269 271 273 274 275 286 telfsum 
 |-  ( ( 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 ) ) ) )
288 91 div1d 
 |-  ( ( ph /\ n e. NN ) -> ( A / 1 ) = A )
289 288 fvoveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( A / 1 ) + 1 ) ) = ( log ` ( A + 1 ) ) )
290 289 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( log ` ( ( A / 1 ) + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) = ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) )
291 287 290 eqtrd 
 |-  ( ( 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 ) ) ) )
292 264 265 291 3eqtr3d 
 |-  ( ( 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 ) ) ) )
293 292 oveq2d 
 |-  ( ( 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 ) ) ) ) )
294 213 293 eqtr3d 
 |-  ( ( 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 ) ) ) ) )
295 171 oveq2d 
 |-  ( m = k -> ( A x. ( log ` ( ( m + 1 ) / m ) ) ) = ( A x. ( log ` ( ( k + 1 ) / k ) ) ) )
296 oveq2 
 |-  ( m = k -> ( A / m ) = ( A / k ) )
297 296 fvoveq1d 
 |-  ( m = k -> ( log ` ( ( A / m ) + 1 ) ) = ( log ` ( ( A / k ) + 1 ) ) )
298 295 297 oveq12d 
 |-  ( m = k -> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
299 ovex 
 |-  ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. _V
300 298 1 299 fvmpt 
 |-  ( k e. NN -> ( G ` k ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
301 167 300 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( G ` k ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
302 301 179 211 fsumser 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) = ( seq 1 ( + , G ) ` n ) )
303 160 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( n + 1 ) ) + 1 ) ) ) = ( ( m e. NN |-> ( ( log ` ( A + 1 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ` n ) )
304 198 303 oveq12d 
 |-  ( ( 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 ) ) )
305 294 302 304 3eqtr3d 
 |-  ( ( 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 ) ) - ( log ` ( ( A / ( m + 1 ) ) + 1 ) ) ) ) ` n ) ) )
306 3 4 9 11 165 201 204 305 climsub 
 |-  ( ph -> seq 1 ( + , G ) ~~> ( ( ( log_G ` ( A + 1 ) ) + ( log ` ( A + 1 ) ) ) - ( log ` ( A + 1 ) ) ) )
307 lgamcl 
 |-  ( ( A + 1 ) e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` ( A + 1 ) ) e. CC )
308 8 307 syl 
 |-  ( ph -> ( log_G ` ( A + 1 ) ) e. CC )
309 308 143 pncand 
 |-  ( ph -> ( ( ( log_G ` ( A + 1 ) ) + ( log ` ( A + 1 ) ) ) - ( log ` ( A + 1 ) ) ) = ( log_G ` ( A + 1 ) ) )
310 306 309 breqtrd 
 |-  ( ph -> seq 1 ( + , G ) ~~> ( log_G ` ( A + 1 ) ) )