Theorem stirlinglem9

Description: ( ( BN ) - ( B( N + 1 ) ) ) is expressed as a limit of a series. This result will be used both to prove that B is decreasing and to prove that B is bounded (below). It will follow that B converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem9.1	|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
	stirlinglem9.2	|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
	stirlinglem9.3	|- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
	stirlinglem9.4	|- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
Assertion	stirlinglem9	|- ( N e. NN -> seq 1 ( + , K ) ~~> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stirlinglem9.1	|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2		stirlinglem9.2	|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3		stirlinglem9.3	|- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
4		stirlinglem9.4	|- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
5		eqid	|- ( k e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) ) = ( k e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) )
6	3 4 5	stirlinglem7	|- ( N e. NN -> seq 1 ( + , K ) ~~> ( J ` N ) )
7	1 2 3	stirlinglem4	|- ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( J ` N ) )
8	6 7	breqtrrd	|- ( N e. NN -> seq 1 ( + , K ) ~~> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )