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 ⊢ 𝐻 = ( 𝑗 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) )
Assertion stirlinglem6 ( 𝑁 ∈ ℕ → seq 0 ( + , 𝐻 ) ⇝ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )

Proof

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