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=\left(j\in {\mathbb{N}}_0⟼2\left(\frac{1}{2j+1}\right){\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^{2j+1}\right)$$
Assertion	stirlinglem6	$$⊢N\in \mathbb{N}\to seq0\left(+,H\right)⇝\log \left(\frac{N+1}{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem6.1	$$⊢H=\left(j\in {\mathbb{N}}_0⟼2\left(\frac{1}{2j+1}\right){\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^{2j+1}\right)$$
2		eqid	$$⊢\left(j\in \mathbb{N}⟼{\left(-1\right)}^{j-1}\left(\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)\right)=\left(j\in \mathbb{N}⟼{\left(-1\right)}^{j-1}\left(\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)\right)$$
3		eqid	$$⊢\left(j\in \mathbb{N}⟼\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)=\left(j\in \mathbb{N}⟼\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)$$
4		eqid	$$⊢\left(j\in \mathbb{N}⟼{\left(-1\right)}^{j-1}\left(\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)+\left(\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)\right)=\left(j\in \mathbb{N}⟼{\left(-1\right)}^{j-1}\left(\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)+\left(\frac{{\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}^j}{j}\right)\right)$$
5		eqid	$$⊢\left(j\in {\mathbb{N}}_0⟼2j+1\right)=\left(j\in {\mathbb{N}}_0⟼2j+1\right)$$
6		2re	$$⊢2\in ℝ$$
7	6	a1i	$$⊢N\in \mathbb{N}\to 2\in ℝ$$
8		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
9	7 8	remulcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
10		0le2	$$⊢0\le 2$$
11	10	a1i	$$⊢N\in \mathbb{N}\to 0\le 2$$
12		0red	$$⊢N\in \mathbb{N}\to 0\in ℝ$$
13		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
14	12 8 13	ltled	$$⊢N\in \mathbb{N}\to 0\le N$$
15	7 8 11 14	mulge0d	$$⊢N\in \mathbb{N}\to 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
16	9 15	ge0p1rpd	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in {ℝ}^{+}$$
17	16	rpreccld	$$⊢N\in \mathbb{N}\to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\in {ℝ}^{+}$$
18		1red	$$⊢N\in \mathbb{N}\to 1\in ℝ$$
19	18	renegcld	$$⊢N\in \mathbb{N}\to -1\in ℝ$$
20	17	rpred	$$⊢N\in \mathbb{N}\to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\in ℝ$$
21		neg1lt0	$$⊢-1<0$$
22	21	a1i	$$⊢N\in \mathbb{N}\to -1<0$$
23	17	rpgt0d	$$⊢N\in \mathbb{N}\to 0<\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
24	19 12 20 22 23	lttrd	$$⊢N\in \mathbb{N}\to -1<\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
25		1rp	$$⊢1\in {ℝ}^{+}$$
26	25	a1i	$$⊢N\in \mathbb{N}\to 1\in {ℝ}^{+}$$
27		1cnd	$$⊢N\in \mathbb{N}\to 1\in ℂ$$
28	27	div1d	$$⊢N\in \mathbb{N}\to \frac{1}{1}=1$$
29		2rp	$$⊢2\in {ℝ}^{+}$$
30	29	a1i	$$⊢N\in \mathbb{N}\to 2\in {ℝ}^{+}$$
31		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
32	30 31	rpmulcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
33	18 32	ltaddrp2d	$$⊢N\in \mathbb{N}\to 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
34	28 33	eqbrtrd	$$⊢N\in \mathbb{N}\to \frac{1}{1}<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
35	26 16 34	ltrec1d	$$⊢N\in \mathbb{N}\to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}<1$$
36	20 18	absltd	$$⊢N\in \mathbb{N}\to \left(\left|\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right|<1\leftrightarrow \left(-1<\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\wedge \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}<1\right)\right)$$
37	24 35 36	mpbir2and	$$⊢N\in \mathbb{N}\to \left|\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right|<1$$
38	2 3 4 1 5 17 37	stirlinglem5	$$⊢N\in \mathbb{N}\to seq0\left(+,H\right)⇝\log \left(\frac{1+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}\right)$$
39		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
40		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
41	39 40	mulcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
42	41 27	addcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in ℂ$$
43	9 18	readdcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in ℝ$$
44		2pos	$$⊢0<2$$
45	44	a1i	$$⊢N\in \mathbb{N}\to 0<2$$
46	7 8 45 13	mulgt0d	$$⊢N\in \mathbb{N}\to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
47	9	ltp1d	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
48	12 9 43 46 47	lttrd	$$⊢N\in \mathbb{N}\to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
49	48	gt0ne0d	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\ne 0$$
50	42 49	dividd	$$⊢N\in \mathbb{N}\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}=1$$
51	50	eqcomd	$$⊢N\in \mathbb{N}\to 1=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
52	51	oveq1d	$$⊢N\in \mathbb{N}\to 1+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)$$
53	51	oveq1d	$$⊢N\in \mathbb{N}\to 1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)$$
54	52 53	oveq12d	$$⊢N\in \mathbb{N}\to \frac{1+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}=\frac{\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}$$
55	42 27 42 49	divdird	$$⊢N\in \mathbb{N}\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)$$
56	55	eqcomd	$$⊢N\in \mathbb{N}\to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
57	42 27 42 49	divsubdird	$$⊢N\in \mathbb{N}\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)$$
58	57	eqcomd	$$⊢N\in \mathbb{N}\to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
59	56 58	oveq12d	$$⊢N\in \mathbb{N}\to \frac{\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}=\frac{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}$$
60	41 27 27	addassd	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1$$
61		1p1e2	$$⊢1+1=2$$
62	61	a1i	$$⊢N\in \mathbb{N}\to 1+1=2$$
63	62	oveq2d	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2$$
64	39	mulridd	$$⊢N\in \mathbb{N}\to 2\cdot 1=2$$
65	64	eqcomd	$$⊢N\in \mathbb{N}\to 2=2\cdot 1$$
66	65	oveq2d	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot 1$$
67	39 40 27	adddid	$$⊢N\in \mathbb{N}\to 2\left(N+1\right)=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot 1$$
68	66 67	eqtr4d	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2=2\left(N+1\right)$$
69	60 63 68	3eqtrd	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1=2\left(N+1\right)$$
70	69	oveq1d	$$⊢N\in \mathbb{N}\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}=\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
71	41 27	pncand	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
72	71	oveq1d	$$⊢N\in \mathbb{N}\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}$$
73	70 72	oveq12d	$$⊢N\in \mathbb{N}\to \frac{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}=\frac{\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}$$
74	59 73	eqtrd	$$⊢N\in \mathbb{N}\to \frac{\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}=\frac{\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}$$
75	40 27	addcld	$$⊢N\in \mathbb{N}\to N+1\in ℂ$$
76	39 75	mulcld	$$⊢N\in \mathbb{N}\to 2\left(N+1\right)\in ℂ$$
77	46	gt0ne0d	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
78	76 41 42 77 49	divcan7d	$$⊢N\in \mathbb{N}\to \frac{\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}=\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
79	45	gt0ne0d	$$⊢N\in \mathbb{N}\to 2\ne 0$$
80	13	gt0ne0d	$$⊢N\in \mathbb{N}\to N\ne 0$$
81	39 39 75 40 79 80	divmuldivd	$$⊢N\in \mathbb{N}\to \left(\frac{2}{2}\right)\left(\frac{N+1}{N}\right)=\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
82	81	eqcomd	$$⊢N\in \mathbb{N}\to \frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=\left(\frac{2}{2}\right)\left(\frac{N+1}{N}\right)$$
83	39 79	dividd	$$⊢N\in \mathbb{N}\to \frac{2}{2}=1$$
84	83	oveq1d	$$⊢N\in \mathbb{N}\to \left(\frac{2}{2}\right)\left(\frac{N+1}{N}\right)=1\left(\frac{N+1}{N}\right)$$
85	75 40 80	divcld	$$⊢N\in \mathbb{N}\to \frac{N+1}{N}\in ℂ$$
86	85	mullidd	$$⊢N\in \mathbb{N}\to 1\left(\frac{N+1}{N}\right)=\frac{N+1}{N}$$
87	84 86	eqtrd	$$⊢N\in \mathbb{N}\to \left(\frac{2}{2}\right)\left(\frac{N+1}{N}\right)=\frac{N+1}{N}$$
88	78 82 87	3eqtrd	$$⊢N\in \mathbb{N}\to \frac{\frac{2\left(N+1\right)}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}{\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}}=\frac{N+1}{N}$$
89	54 74 88	3eqtrd	$$⊢N\in \mathbb{N}\to \frac{1+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}=\frac{N+1}{N}$$
90	89	fveq2d	$$⊢N\in \mathbb{N}\to \log \left(\frac{1+\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}{1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\right)}\right)=\log \left(\frac{N+1}{N}\right)$$
91	38 90	breqtrd	$$⊢N\in \mathbb{N}\to seq0\left(+,H\right)⇝\log \left(\frac{N+1}{N}\right)$$