Theorem lgamcvg

Description: The series G converges to log_G ( A ) + log ( A ) . (Contributed by Mario Carneiro, 6-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		lgamcvg.g	|- G = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
2		lgamcvg.a	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
3		eqid	|- { x e. CC | ( ( abs ` x ) <_ y /\ A. k e. NN0 ( 1 / y ) <_ ( abs ` ( x + k ) ) ) } = { x e. CC | ( ( abs ` x ) <_ y /\ A. k e. NN0 ( 1 / y ) <_ ( abs ` ( x + k ) ) ) }
4	3 2 1	lgamcvglem	|- ( ph -> ( ( log_G ` A ) e. CC /\ seq 1 ( + , G ) ~~> ( ( log_G ` A ) + ( log ` A ) ) ) )
5	4	simprd	|- ( ph -> seq 1 ( + , G ) ~~> ( ( log_G ` A ) + ( log ` A ) ) )