Metamath Proof Explorer

Theorem stirlinglem6

Description: A series that converges to log (N+1)/N. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis stirlinglem6.1 
|- H = ( j e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) ) )
Assertion stirlinglem6 
|- ( N e. NN -> seq 0 ( + , H ) ~~> ( log ` ( ( N + 1 ) / N ) ) )

Proof

Step Hyp Ref Expression
1 stirlinglem6.1 
 |-  H = ( j e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) ) )
2 eqid 
 |-  ( j e. NN |-> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) ) = ( j e. NN |-> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) )
3 eqid 
 |-  ( j e. NN |-> ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) = ( j e. NN |-> ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) )
4 eqid 
 |-  ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) x. ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) + ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) ) = ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) x. ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) + ( ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ j ) / j ) ) )
5 eqid 
 |-  ( j e. NN0 |-> ( ( 2 x. j ) + 1 ) ) = ( j e. NN0 |-> ( ( 2 x. j ) + 1 ) )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( N e. NN -> 2 e. RR )
8 nnre 
 |-  ( N e. NN -> N e. RR )
9 7 8 remulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
10 0le2 
 |-  0 <_ 2
11 10 a1i 
 |-  ( N e. NN -> 0 <_ 2 )
12 0red 
 |-  ( N e. NN -> 0 e. RR )
13 nngt0 
 |-  ( N e. NN -> 0 < N )
14 12 8 13 ltled 
 |-  ( N e. NN -> 0 <_ N )
15 7 8 11 14 mulge0d 
 |-  ( N e. NN -> 0 <_ ( 2 x. N ) )
16 9 15 ge0p1rpd 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR+ )
17 16 rpreccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR+ )
18 1red 
 |-  ( N e. NN -> 1 e. RR )
19 18 renegcld 
 |-  ( N e. NN -> -u 1 e. RR )
20 17 rpred 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR )
21 neg1lt0 
 |-  -u 1 < 0
22 21 a1i 
 |-  ( N e. NN -> -u 1 < 0 )
23 17 rpgt0d 
 |-  ( N e. NN -> 0 < ( 1 / ( ( 2 x. N ) + 1 ) ) )
24 19 12 20 22 23 lttrd 
 |-  ( N e. NN -> -u 1 < ( 1 / ( ( 2 x. N ) + 1 ) ) )
25 1rp 
 |-  1 e. RR+
26 25 a1i 
 |-  ( N e. NN -> 1 e. RR+ )
27 1cnd 
 |-  ( N e. NN -> 1 e. CC )
28 27 div1d 
 |-  ( N e. NN -> ( 1 / 1 ) = 1 )
29 2rp 
 |-  2 e. RR+
30 29 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
31 nnrp 
 |-  ( N e. NN -> N e. RR+ )
32 30 31 rpmulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR+ )
33 18 32 ltaddrp2d 
 |-  ( N e. NN -> 1 < ( ( 2 x. N ) + 1 ) )
34 28 33 eqbrtrd 
 |-  ( N e. NN -> ( 1 / 1 ) < ( ( 2 x. N ) + 1 ) )
35 26 16 34 ltrec1d 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) < 1 )
36 20 18 absltd 
 |-  ( N e. NN -> ( ( abs ` ( 1 / ( ( 2 x. N ) + 1 ) ) ) < 1 <-> ( -u 1 < ( 1 / ( ( 2 x. N ) + 1 ) ) /\ ( 1 / ( ( 2 x. N ) + 1 ) ) < 1 ) ) )
37 24 35 36 mpbir2and 
 |-  ( N e. NN -> ( abs ` ( 1 / ( ( 2 x. N ) + 1 ) ) ) < 1 )
38 2 3 4 1 5 17 37 stirlinglem5 
 |-  ( N e. NN -> seq 0 ( + , H ) ~~> ( log ` ( ( 1 + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( 1 - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) ) )
39 2cnd 
 |-  ( N e. NN -> 2 e. CC )
40 nncn 
 |-  ( N e. NN -> N e. CC )
41 39 40 mulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. CC )
42 41 27 addcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. CC )
43 9 18 readdcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR )
44 2pos 
 |-  0 < 2
45 44 a1i 
 |-  ( N e. NN -> 0 < 2 )
46 7 8 45 13 mulgt0d 
 |-  ( N e. NN -> 0 < ( 2 x. N ) )
47 9 ltp1d 
 |-  ( N e. NN -> ( 2 x. N ) < ( ( 2 x. N ) + 1 ) )
48 12 9 43 46 47 lttrd 
 |-  ( N e. NN -> 0 < ( ( 2 x. N ) + 1 ) )
49 48 gt0ne0d 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) =/= 0 )
50 42 49 dividd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = 1 )
51 50 eqcomd 
 |-  ( N e. NN -> 1 = ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) )
52 51 oveq1d 
 |-  ( N e. NN -> ( 1 + ( 1 / ( ( 2 x. N ) + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) + ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
53 51 oveq1d 
 |-  ( N e. NN -> ( 1 - ( 1 / ( ( 2 x. N ) + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) - ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
54 52 53 oveq12d 
 |-  ( N e. NN -> ( ( 1 + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( 1 - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) )
55 42 27 42 49 divdird 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) + ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
56 55 eqcomd 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) + ( 1 / ( ( 2 x. N ) + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) + 1 ) / ( ( 2 x. N ) + 1 ) ) )
57 42 27 42 49 divsubdird 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) - 1 ) / ( ( 2 x. N ) + 1 ) ) = ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) - ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
58 57 eqcomd 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) - ( 1 / ( ( 2 x. N ) + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) - 1 ) / ( ( 2 x. N ) + 1 ) ) )
59 56 58 oveq12d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( ( ( 2 x. N ) + 1 ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( ( 2 x. N ) + 1 ) - 1 ) / ( ( 2 x. N ) + 1 ) ) ) )
60 41 27 27 addassd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) + 1 ) = ( ( 2 x. N ) + ( 1 + 1 ) ) )
61 1p1e2 
 |-  ( 1 + 1 ) = 2
62 61 a1i 
 |-  ( N e. NN -> ( 1 + 1 ) = 2 )
63 62 oveq2d 
 |-  ( N e. NN -> ( ( 2 x. N ) + ( 1 + 1 ) ) = ( ( 2 x. N ) + 2 ) )
64 39 mulid1d 
 |-  ( N e. NN -> ( 2 x. 1 ) = 2 )
65 64 eqcomd 
 |-  ( N e. NN -> 2 = ( 2 x. 1 ) )
66 65 oveq2d 
 |-  ( N e. NN -> ( ( 2 x. N ) + 2 ) = ( ( 2 x. N ) + ( 2 x. 1 ) ) )
67 39 40 27 adddid 
 |-  ( N e. NN -> ( 2 x. ( N + 1 ) ) = ( ( 2 x. N ) + ( 2 x. 1 ) ) )
68 66 67 eqtr4d 
 |-  ( N e. NN -> ( ( 2 x. N ) + 2 ) = ( 2 x. ( N + 1 ) ) )
69 60 63 68 3eqtrd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) + 1 ) = ( 2 x. ( N + 1 ) ) )
70 69 oveq1d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = ( ( 2 x. ( N + 1 ) ) / ( ( 2 x. N ) + 1 ) ) )
71 41 27 pncand 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) - 1 ) = ( 2 x. N ) )
72 71 oveq1d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) - 1 ) / ( ( 2 x. N ) + 1 ) ) = ( ( 2 x. N ) / ( ( 2 x. N ) + 1 ) ) )
73 70 72 oveq12d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( ( 2 x. N ) + 1 ) - 1 ) / ( ( 2 x. N ) + 1 ) ) ) = ( ( ( 2 x. ( N + 1 ) ) / ( ( 2 x. N ) + 1 ) ) / ( ( 2 x. N ) / ( ( 2 x. N ) + 1 ) ) ) )
74 59 73 eqtrd 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( 2 x. ( N + 1 ) ) / ( ( 2 x. N ) + 1 ) ) / ( ( 2 x. N ) / ( ( 2 x. N ) + 1 ) ) ) )
75 40 27 addcld 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
76 39 75 mulcld 
 |-  ( N e. NN -> ( 2 x. ( N + 1 ) ) e. CC )
77 46 gt0ne0d 
 |-  ( N e. NN -> ( 2 x. N ) =/= 0 )
78 76 41 42 77 49 divcan7d 
 |-  ( N e. NN -> ( ( ( 2 x. ( N + 1 ) ) / ( ( 2 x. N ) + 1 ) ) / ( ( 2 x. N ) / ( ( 2 x. N ) + 1 ) ) ) = ( ( 2 x. ( N + 1 ) ) / ( 2 x. N ) ) )
79 45 gt0ne0d 
 |-  ( N e. NN -> 2 =/= 0 )
80 13 gt0ne0d 
 |-  ( N e. NN -> N =/= 0 )
81 39 39 75 40 79 80 divmuldivd 
 |-  ( N e. NN -> ( ( 2 / 2 ) x. ( ( N + 1 ) / N ) ) = ( ( 2 x. ( N + 1 ) ) / ( 2 x. N ) ) )
82 81 eqcomd 
 |-  ( N e. NN -> ( ( 2 x. ( N + 1 ) ) / ( 2 x. N ) ) = ( ( 2 / 2 ) x. ( ( N + 1 ) / N ) ) )
83 39 79 dividd 
 |-  ( N e. NN -> ( 2 / 2 ) = 1 )
84 83 oveq1d 
 |-  ( N e. NN -> ( ( 2 / 2 ) x. ( ( N + 1 ) / N ) ) = ( 1 x. ( ( N + 1 ) / N ) ) )
85 75 40 80 divcld 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) e. CC )
86 85 mulid2d 
 |-  ( N e. NN -> ( 1 x. ( ( N + 1 ) / N ) ) = ( ( N + 1 ) / N ) )
87 84 86 eqtrd 
 |-  ( N e. NN -> ( ( 2 / 2 ) x. ( ( N + 1 ) / N ) ) = ( ( N + 1 ) / N ) )
88 78 82 87 3eqtrd 
 |-  ( N e. NN -> ( ( ( 2 x. ( N + 1 ) ) / ( ( 2 x. N ) + 1 ) ) / ( ( 2 x. N ) / ( ( 2 x. N ) + 1 ) ) ) = ( ( N + 1 ) / N ) )
89 54 74 88 3eqtrd 
 |-  ( N e. NN -> ( ( 1 + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( 1 - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( N + 1 ) / N ) )
90 89 fveq2d 
 |-  ( N e. NN -> ( log ` ( ( 1 + ( 1 / ( ( 2 x. N ) + 1 ) ) ) / ( 1 - ( 1 / ( ( 2 x. N ) + 1 ) ) ) ) ) = ( log ` ( ( N + 1 ) / N ) ) )
91 38 90 breqtrd 
 |-  ( N e. NN -> seq 0 ( + , H ) ~~> ( log ` ( ( N + 1 ) / N ) ) )