stirlinglem10

Description: A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole B sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem10.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
	stirlinglem10.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
	stirlinglem10.4	$⊢ K = (k \in ℕ ⟼ (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k})$
	stirlinglem10.5	$⊢ L = (k \in ℕ ⟼ {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{k})$
Assertion	stirlinglem10	$⊢ N \in ℕ \to B (N) - B (N + 1) \leq (\frac{1}{4}) (\frac{1}{N (N + 1)})$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem10.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
2		stirlinglem10.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
3		stirlinglem10.4	$⊢ K = (k \in ℕ ⟼ (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k})$
4		stirlinglem10.5	$⊢ L = (k \in ℕ ⟼ {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{k})$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		1zzd	$⊢ N \in ℕ \to 1 \in ℤ$
7		eqid	$⊢ (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1) = (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1)$
8	1 2 7 3	stirlinglem9	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ (B (N) - B (N + 1))$
9		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
10		nncn	$⊢ N \in ℕ \to N \in ℂ$
11	9 10	mulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℂ$
12		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
13	11 12	addcld	$⊢ N \in ℕ \to 2 \cdot N + 1 \in ℂ$
14	13	sqcld	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} \in ℂ$
15		0red	$⊢ N \in ℕ \to 0 \in ℝ$
16		1red	$⊢ N \in ℕ \to 1 \in ℝ$
17		2re	$⊢ 2 \in ℝ$
18	17	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
19		nnre	$⊢ N \in ℕ \to N \in ℝ$
20	18 19	remulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℝ$
21	20 16	readdcld	$⊢ N \in ℕ \to 2 \cdot N + 1 \in ℝ$
22		0lt1	$⊢ 0 < 1$
23	22	a1i	$⊢ N \in ℕ \to 0 < 1$
24		2rp	$⊢ 2 \in ℝ^{+}$
25	24	a1i	$⊢ N \in ℕ \to 2 \in ℝ^{+}$
26		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
27	25 26	rpmulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℝ^{+}$
28	16 27	ltaddrp2d	$⊢ N \in ℕ \to 1 < 2 \cdot N + 1$
29	15 16 21 23 28	lttrd	$⊢ N \in ℕ \to 0 < 2 \cdot N + 1$
30	29	gt0ne0d	$⊢ N \in ℕ \to 2 \cdot N + 1 \neq 0$
31		2z	$⊢ 2 \in ℤ$
32	31	a1i	$⊢ N \in ℕ \to 2 \in ℤ$
33	13 30 32	expne0d	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} \neq 0$
34	14 33	reccld	$⊢ N \in ℕ \to \frac{1}{{(2 \cdot N + 1)}^{2}} \in ℂ$
35	16	renegcld	$⊢ N \in ℕ \to - 1 \in ℝ$
36	21	resqcld	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} \in ℝ$
37	36 33	rereccld	$⊢ N \in ℕ \to \frac{1}{{(2 \cdot N + 1)}^{2}} \in ℝ$
38		1re	$⊢ 1 \in ℝ$
39		lt0neg2	$⊢ 1 \in ℝ \to (0 < 1 \leftrightarrow - 1 < 0)$
40	38 39	ax-mp	$⊢ 0 < 1 \leftrightarrow - 1 < 0$
41	23 40	sylib	$⊢ N \in ℕ \to - 1 < 0$
42	21 30	sqgt0d	$⊢ N \in ℕ \to 0 < {(2 \cdot N + 1)}^{2}$
43	36 42	recgt0d	$⊢ N \in ℕ \to 0 < \frac{1}{{(2 \cdot N + 1)}^{2}}$
44	35 15 37 41 43	lttrd	$⊢ N \in ℕ \to - 1 < \frac{1}{{(2 \cdot N + 1)}^{2}}$
45		2nn	$⊢ 2 \in ℕ$
46	45	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
47		expgt1	$⊢ (2 \cdot N + 1 \in ℝ \land 2 \in ℕ \land 1 < 2 \cdot N + 1) \to 1 < {(2 \cdot N + 1)}^{2}$
48	21 46 28 47	syl3anc	$⊢ N \in ℕ \to 1 < {(2 \cdot N + 1)}^{2}$
49	36 42	elrpd	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} \in ℝ^{+}$
50	49	recgt1d	$⊢ N \in ℕ \to (1 < {(2 \cdot N + 1)}^{2} \leftrightarrow \frac{1}{{(2 \cdot N + 1)}^{2}} < 1)$
51	48 50	mpbid	$⊢ N \in ℕ \to \frac{1}{{(2 \cdot N + 1)}^{2}} < 1$
52	37 16	absltd	$⊢ N \in ℕ \to (\|\frac{1}{{(2 \cdot N + 1)}^{2}}\| < 1 \leftrightarrow (- 1 < \frac{1}{{(2 \cdot N + 1)}^{2}} \land \frac{1}{{(2 \cdot N + 1)}^{2}} < 1))$
53	44 51 52	mpbir2and	$⊢ N \in ℕ \to \|\frac{1}{{(2 \cdot N + 1)}^{2}}\| < 1$
54		1nn0	$⊢ 1 \in ℕ_{0}$
55	54	a1i	$⊢ N \in ℕ \to 1 \in ℕ_{0}$
56	4	a1i	$⊢ (N \in ℕ \land j \in ℤ_{\geq 1}) \to L = (k \in ℕ ⟼ {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{k})$
57		simpr	$⊢ ((N \in ℕ \land j \in ℤ_{\geq 1}) \land k = j) \to k = j$
58	57	oveq2d	$⊢ ((N \in ℕ \land j \in ℤ_{\geq 1}) \land k = j) \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{k} = {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{j}$
59		elnnuz	$⊢ j \in ℕ \leftrightarrow j \in ℤ_{\geq 1}$
60	59	biimpri	$⊢ j \in ℤ_{\geq 1} \to j \in ℕ$
61	60	adantl	$⊢ (N \in ℕ \land j \in ℤ_{\geq 1}) \to j \in ℕ$
62	34	adantr	$⊢ (N \in ℕ \land j \in ℤ_{\geq 1}) \to \frac{1}{{(2 \cdot N + 1)}^{2}} \in ℂ$
63	61	nnnn0d	$⊢ (N \in ℕ \land j \in ℤ_{\geq 1}) \to j \in ℕ_{0}$
64	62 63	expcld	$⊢ (N \in ℕ \land j \in ℤ_{\geq 1}) \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{j} \in ℂ$
65	56 58 61 64	fvmptd	$⊢ (N \in ℕ \land j \in ℤ_{\geq 1}) \to L (j) = {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{j}$
66	34 53 55 65	geolim2	$⊢ N \in ℕ \to seq 1 (+ L) ⇝ (\frac{{(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{1}}{1 - (\frac{1}{{(2 \cdot N + 1)}^{2}})})$
67	34	exp1d	$⊢ N \in ℕ \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{1} = \frac{1}{{(2 \cdot N + 1)}^{2}}$
68	14 33	dividd	$⊢ N \in ℕ \to \frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}} = 1$
69	68	eqcomd	$⊢ N \in ℕ \to 1 = \frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}}$
70	69	oveq1d	$⊢ N \in ℕ \to 1 - (\frac{1}{{(2 \cdot N + 1)}^{2}}) = (\frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}}) - (\frac{1}{{(2 \cdot N + 1)}^{2}})$
71	49	rpcnne0d	$⊢ N \in ℕ \to ({(2 \cdot N + 1)}^{2} \in ℂ \land {(2 \cdot N + 1)}^{2} \neq 0)$
72		divsubdir	$⊢ ({(2 \cdot N + 1)}^{2} \in ℂ \land 1 \in ℂ \land ({(2 \cdot N + 1)}^{2} \in ℂ \land {(2 \cdot N + 1)}^{2} \neq 0)) \to \frac{{(2 \cdot N + 1)}^{2} - 1}{{(2 \cdot N + 1)}^{2}} = (\frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}}) - (\frac{1}{{(2 \cdot N + 1)}^{2}})$
73	14 12 71 72	syl3anc	$⊢ N \in ℕ \to \frac{{(2 \cdot N + 1)}^{2} - 1}{{(2 \cdot N + 1)}^{2}} = (\frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}}) - (\frac{1}{{(2 \cdot N + 1)}^{2}})$
74		ax-1cn	$⊢ 1 \in ℂ$
75		binom2	$⊢ (2 \cdot N \in ℂ \land 1 \in ℂ) \to {(2 \cdot N + 1)}^{2} = {2 \cdot N}^{2} + 2 2 \cdot N \cdot 1 + 1^{2}$
76	11 74 75	sylancl	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} = {2 \cdot N}^{2} + 2 2 \cdot N \cdot 1 + 1^{2}$
77	76	oveq1d	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} - 1 = ({2 \cdot N}^{2} + 2 2 \cdot N \cdot 1) + 1^{2} - 1$
78	9 10	sqmuld	$⊢ N \in ℕ \to {2 \cdot N}^{2} = 2^{2} N^{2}$
79		sq2	$⊢ 2^{2} = 4$
80	79	a1i	$⊢ N \in ℕ \to 2^{2} = 4$
81	80	oveq1d	$⊢ N \in ℕ \to 2^{2} N^{2} = 4 N^{2}$
82	78 81	eqtrd	$⊢ N \in ℕ \to {2 \cdot N}^{2} = 4 N^{2}$
83	11	mulid1d	$⊢ N \in ℕ \to 2 \cdot N \cdot 1 = 2 \cdot N$
84	83	oveq2d	$⊢ N \in ℕ \to 2 2 \cdot N \cdot 1 = 2 2 \cdot N$
85	9 9 10	mulassd	$⊢ N \in ℕ \to 2 \cdot 2 \cdot N = 2 2 \cdot N$
86		2t2e4	$⊢ 2 \cdot 2 = 4$
87	86	a1i	$⊢ N \in ℕ \to 2 \cdot 2 = 4$
88	87	oveq1d	$⊢ N \in ℕ \to 2 \cdot 2 \cdot N = 4 \cdot N$
89	84 85 88	3eqtr2d	$⊢ N \in ℕ \to 2 2 \cdot N \cdot 1 = 4 \cdot N$
90	82 89	oveq12d	$⊢ N \in ℕ \to {2 \cdot N}^{2} + 2 2 \cdot N \cdot 1 = 4 N^{2} + 4 \cdot N$
91		4cn	$⊢ 4 \in ℂ$
92	91	a1i	$⊢ N \in ℕ \to 4 \in ℂ$
93	10	sqcld	$⊢ N \in ℕ \to N^{2} \in ℂ$
94	92 93 10	adddid	$⊢ N \in ℕ \to 4 (N^{2} + N) = 4 N^{2} + 4 \cdot N$
95	10	sqvald	$⊢ N \in ℕ \to N^{2} = N \cdot N$
96	10	mulid1d	$⊢ N \in ℕ \to N \cdot 1 = N$
97	96	eqcomd	$⊢ N \in ℕ \to N = N \cdot 1$
98	95 97	oveq12d	$⊢ N \in ℕ \to N^{2} + N = N \cdot N + N \cdot 1$
99	10 10 12	adddid	$⊢ N \in ℕ \to N (N + 1) = N \cdot N + N \cdot 1$
100	98 99	eqtr4d	$⊢ N \in ℕ \to N^{2} + N = N (N + 1)$
101	100	oveq2d	$⊢ N \in ℕ \to 4 (N^{2} + N) = 4 N (N + 1)$
102	90 94 101	3eqtr2d	$⊢ N \in ℕ \to {2 \cdot N}^{2} + 2 2 \cdot N \cdot 1 = 4 N (N + 1)$
103		sq1	$⊢ 1^{2} = 1$
104	103	a1i	$⊢ N \in ℕ \to 1^{2} = 1$
105	102 104	oveq12d	$⊢ N \in ℕ \to {2 \cdot N}^{2} + 2 2 \cdot N \cdot 1 + 1^{2} = 4 N (N + 1) + 1$
106	105	oveq1d	$⊢ N \in ℕ \to ({2 \cdot N}^{2} + 2 2 \cdot N \cdot 1) + 1^{2} - 1 = 4 N (N + 1) + 1 - 1$
107	10 12	addcld	$⊢ N \in ℕ \to N + 1 \in ℂ$
108	10 107	mulcld	$⊢ N \in ℕ \to N (N + 1) \in ℂ$
109	92 108	mulcld	$⊢ N \in ℕ \to 4 N (N + 1) \in ℂ$
110	109 12	pncand	$⊢ N \in ℕ \to 4 N (N + 1) + 1 - 1 = 4 N (N + 1)$
111	77 106 110	3eqtrd	$⊢ N \in ℕ \to {(2 \cdot N + 1)}^{2} - 1 = 4 N (N + 1)$
112	111	oveq1d	$⊢ N \in ℕ \to \frac{{(2 \cdot N + 1)}^{2} - 1}{{(2 \cdot N + 1)}^{2}} = \frac{4 N (N + 1)}{{(2 \cdot N + 1)}^{2}}$
113	70 73 112	3eqtr2d	$⊢ N \in ℕ \to 1 - (\frac{1}{{(2 \cdot N + 1)}^{2}}) = \frac{4 N (N + 1)}{{(2 \cdot N + 1)}^{2}}$
114	67 113	oveq12d	$⊢ N \in ℕ \to \frac{{(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{1}}{1 - (\frac{1}{{(2 \cdot N + 1)}^{2}})} = \frac{\frac{1}{{(2 \cdot N + 1)}^{2}}}{\frac{4 N (N + 1)}{{(2 \cdot N + 1)}^{2}}}$
115		4pos	$⊢ 0 < 4$
116	115	a1i	$⊢ N \in ℕ \to 0 < 4$
117	116	gt0ne0d	$⊢ N \in ℕ \to 4 \neq 0$
118		nnne0	$⊢ N \in ℕ \to N \neq 0$
119	19 16	readdcld	$⊢ N \in ℕ \to N + 1 \in ℝ$
120		nngt0	$⊢ N \in ℕ \to 0 < N$
121	19	ltp1d	$⊢ N \in ℕ \to N < N + 1$
122	15 19 119 120 121	lttrd	$⊢ N \in ℕ \to 0 < N + 1$
123	122	gt0ne0d	$⊢ N \in ℕ \to N + 1 \neq 0$
124	10 107 118 123	mulne0d	$⊢ N \in ℕ \to N (N + 1) \neq 0$
125	92 108 117 124	mulne0d	$⊢ N \in ℕ \to 4 N (N + 1) \neq 0$
126	12 14 109 14 33 33 125	divdivdivd	$⊢ N \in ℕ \to \frac{\frac{1}{{(2 \cdot N + 1)}^{2}}}{\frac{4 N (N + 1)}{{(2 \cdot N + 1)}^{2}}} = \frac{1 {(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2} 4 N (N + 1)}$
127	12 14	mulcomd	$⊢ N \in ℕ \to 1 {(2 \cdot N + 1)}^{2} = {(2 \cdot N + 1)}^{2} \cdot 1$
128	127	oveq1d	$⊢ N \in ℕ \to \frac{1 {(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2} 4 N (N + 1)} = \frac{{(2 \cdot N + 1)}^{2} \cdot 1}{{(2 \cdot N + 1)}^{2} 4 N (N + 1)}$
129	12	mulid1d	$⊢ N \in ℕ \to 1 \cdot 1 = 1$
130	129	eqcomd	$⊢ N \in ℕ \to 1 = 1 \cdot 1$
131	130	oveq1d	$⊢ N \in ℕ \to \frac{1}{4 N (N + 1)} = \frac{1 \cdot 1}{4 N (N + 1)}$
132	12 92 12 108 117 124	divmuldivd	$⊢ N \in ℕ \to (\frac{1}{4}) (\frac{1}{N (N + 1)}) = \frac{1 \cdot 1}{4 N (N + 1)}$
133	131 132	eqtr4d	$⊢ N \in ℕ \to \frac{1}{4 N (N + 1)} = (\frac{1}{4}) (\frac{1}{N (N + 1)})$
134	68 133	oveq12d	$⊢ N \in ℕ \to (\frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}}) (\frac{1}{4 N (N + 1)}) = 1 (\frac{1}{4}) (\frac{1}{N (N + 1)})$
135	14 14 12 109 33 125	divmuldivd	$⊢ N \in ℕ \to (\frac{{(2 \cdot N + 1)}^{2}}{{(2 \cdot N + 1)}^{2}}) (\frac{1}{4 N (N + 1)}) = \frac{{(2 \cdot N + 1)}^{2} \cdot 1}{{(2 \cdot N + 1)}^{2} 4 N (N + 1)}$
136	92 117	reccld	$⊢ N \in ℕ \to \frac{1}{4} \in ℂ$
137	108 124	reccld	$⊢ N \in ℕ \to \frac{1}{N (N + 1)} \in ℂ$
138	136 137	mulcld	$⊢ N \in ℕ \to (\frac{1}{4}) (\frac{1}{N (N + 1)}) \in ℂ$
139	138	mulid2d	$⊢ N \in ℕ \to 1 (\frac{1}{4}) (\frac{1}{N (N + 1)}) = (\frac{1}{4}) (\frac{1}{N (N + 1)})$
140	134 135 139	3eqtr3d	$⊢ N \in ℕ \to \frac{{(2 \cdot N + 1)}^{2} \cdot 1}{{(2 \cdot N + 1)}^{2} 4 N (N + 1)} = (\frac{1}{4}) (\frac{1}{N (N + 1)})$
141	126 128 140	3eqtrd	$⊢ N \in ℕ \to \frac{\frac{1}{{(2 \cdot N + 1)}^{2}}}{\frac{4 N (N + 1)}{{(2 \cdot N + 1)}^{2}}} = (\frac{1}{4}) (\frac{1}{N (N + 1)})$
142	114 141	eqtrd	$⊢ N \in ℕ \to \frac{{(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{1}}{1 - (\frac{1}{{(2 \cdot N + 1)}^{2}})} = (\frac{1}{4}) (\frac{1}{N (N + 1)})$
143	66 142	breqtrd	$⊢ N \in ℕ \to seq 1 (+ L) ⇝ (\frac{1}{4}) (\frac{1}{N (N + 1)})$
144	59	biimpi	$⊢ j \in ℕ \to j \in ℤ_{\geq 1}$
145	144	adantl	$⊢ (N \in ℕ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
146		oveq2	$⊢ k = n \to 2 k = 2 n$
147	146	oveq1d	$⊢ k = n \to 2 k + 1 = 2 n + 1$
148	147	oveq2d	$⊢ k = n \to \frac{1}{2 k + 1} = \frac{1}{2 n + 1}$
149	146	oveq2d	$⊢ k = n \to {(\frac{1}{2 \cdot N + 1})}^{2 k} = {(\frac{1}{2 \cdot N + 1})}^{2 n}$
150	148 149	oveq12d	$⊢ k = n \to (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k} = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
151		elfznn	$⊢ n \in (1 \dots j) \to n \in ℕ$
152	151	adantl	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to n \in ℕ$
153		2cnd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \in ℂ$
154	152	nncnd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to n \in ℂ$
155	153 154	mulcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 n \in ℂ$
156		1cnd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 1 \in ℂ$
157	155 156	addcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 n + 1 \in ℂ$
158		0red	$⊢ n \in ℕ \to 0 \in ℝ$
159		1red	$⊢ n \in ℕ \to 1 \in ℝ$
160	17	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
161		nnre	$⊢ n \in ℕ \to n \in ℝ$
162	160 161	remulcld	$⊢ n \in ℕ \to 2 n \in ℝ$
163	162 159	readdcld	$⊢ n \in ℕ \to 2 n + 1 \in ℝ$
164	22	a1i	$⊢ n \in ℕ \to 0 < 1$
165	24	a1i	$⊢ n \in ℕ \to 2 \in ℝ^{+}$
166		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
167	165 166	rpmulcld	$⊢ n \in ℕ \to 2 n \in ℝ^{+}$
168	159 167	ltaddrp2d	$⊢ n \in ℕ \to 1 < 2 n + 1$
169	158 159 163 164 168	lttrd	$⊢ n \in ℕ \to 0 < 2 n + 1$
170	151 169	syl	$⊢ n \in (1 \dots j) \to 0 < 2 n + 1$
171	170	gt0ne0d	$⊢ n \in (1 \dots j) \to 2 n + 1 \neq 0$
172	171	adantl	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 n + 1 \neq 0$
173	157 172	reccld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \in ℂ$
174	10	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to N \in ℂ$
175	153 174	mulcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \cdot N \in ℂ$
176	175 156	addcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \cdot N + 1 \in ℂ$
177	30	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \cdot N + 1 \neq 0$
178	176 177	reccld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{2 \cdot N + 1} \in ℂ$
179		2nn0	$⊢ 2 \in ℕ_{0}$
180	179	a1i	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \in ℕ_{0}$
181	152	nnnn0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to n \in ℕ_{0}$
182	180 181	nn0mulcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 n \in ℕ_{0}$
183	178 182	expcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℂ$
184	173 183	mulcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℂ$
185	3 150 152 184	fvmptd3	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to K (n) = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
186	185	adantlr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to K (n) = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
187	169	gt0ne0d	$⊢ n \in ℕ \to 2 n + 1 \neq 0$
188	163 187	rereccld	$⊢ n \in ℕ \to \frac{1}{2 n + 1} \in ℝ$
189	151 188	syl	$⊢ n \in (1 \dots j) \to \frac{1}{2 n + 1} \in ℝ$
190	189	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \in ℝ$
191	21 30	rereccld	$⊢ N \in ℕ \to \frac{1}{2 \cdot N + 1} \in ℝ$
192	191	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{2 \cdot N + 1} \in ℝ$
193	192 182	reexpcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℝ$
194	193	adantlr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℝ$
195	190 194	remulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℝ$
196	186 195	eqeltrd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to K (n) \in ℝ$
197		readdcl	$⊢ (n \in ℝ \land i \in ℝ) \to n + i \in ℝ$
198	197	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℝ \land i \in ℝ)) \to n + i \in ℝ$
199	145 196 198	seqcl	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ K) (j) \in ℝ$
200		oveq2	$⊢ k = n \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{k} = {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
201	34	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{{(2 \cdot N + 1)}^{2}} \in ℂ$
202	201 181	expcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} \in ℂ$
203	4 200 152 202	fvmptd3	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to L (n) = {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
204	37	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{{(2 \cdot N + 1)}^{2}} \in ℝ$
205	204 181	reexpcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} \in ℝ$
206	203 205	eqeltrd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to L (n) \in ℝ$
207	206	adantlr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to L (n) \in ℝ$
208	145 207 198	seqcl	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ L) (j) \in ℝ$
209	31	a1i	$⊢ n \in (1 \dots j) \to 2 \in ℤ$
210		elfzelz	$⊢ n \in (1 \dots j) \to n \in ℤ$
211	209 210	zmulcld	$⊢ n \in (1 \dots j) \to 2 n \in ℤ$
212		1exp	$⊢ 2 n \in ℤ \to 1^{2 n} = 1$
213	211 212	syl	$⊢ n \in (1 \dots j) \to 1^{2 n} = 1$
214		1exp	$⊢ n \in ℤ \to 1^{n} = 1$
215	210 214	syl	$⊢ n \in (1 \dots j) \to 1^{n} = 1$
216	213 215	eqtr4d	$⊢ n \in (1 \dots j) \to 1^{2 n} = 1^{n}$
217	216	adantl	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 1^{2 n} = 1^{n}$
218	176 181 180	expmuld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n} = {({(2 \cdot N + 1)}^{2})}^{n}$
219	217 218	oveq12d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1^{2 n}}{{(2 \cdot N + 1)}^{2 n}} = \frac{1^{n}}{{({(2 \cdot N + 1)}^{2})}^{n}}$
220	156 176 177 182	expdivd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} = \frac{1^{2 n}}{{(2 \cdot N + 1)}^{2 n}}$
221	176	sqcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2} \in ℂ$
222	31	a1i	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \in ℤ$
223	176 177 222	expne0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2} \neq 0$
224	156 221 223 181	expdivd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} = \frac{1^{n}}{{({(2 \cdot N + 1)}^{2})}^{n}}$
225	219 220 224	3eqtr4d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} = {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
226	225	oveq2d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n} = (\frac{1}{2 n + 1}) {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
227		1rp	$⊢ 1 \in ℝ^{+}$
228	227	a1i	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 1 \in ℝ^{+}$
229	17	a1i	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \in ℝ$
230	152	nnred	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to n \in ℝ$
231	229 230	remulcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 n \in ℝ$
232	180	nn0ge0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 0 \leq 2$
233	181	nn0ge0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 0 \leq n$
234	229 230 232 233	mulge0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 0 \leq 2 n$
235	231 234	ge0p1rpd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 n + 1 \in ℝ^{+}$
236		1red	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 1 \in ℝ$
237	228	rpge0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 0 \leq 1$
238	159 163 168	ltled	$⊢ n \in ℕ \to 1 \leq 2 n + 1$
239	151 238	syl	$⊢ n \in (1 \dots j) \to 1 \leq 2 n + 1$
240	239	adantl	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 1 \leq 2 n + 1$
241	228 235 236 237 240	lediv2ad	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \leq \frac{1}{1}$
242	156	div1d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{1} = 1$
243	241 242	breqtrd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \leq 1$
244	152 188	syl	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \in ℝ$
245	19	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to N \in ℝ$
246	229 245	remulcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \cdot N \in ℝ$
247	15 19 120	ltled	$⊢ N \in ℕ \to 0 \leq N$
248	247	adantr	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 0 \leq N$
249	229 245 232 248	mulge0d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 0 \leq 2 \cdot N$
250	246 249	ge0p1rpd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 2 \cdot N + 1 \in ℝ^{+}$
251	250 222	rpexpcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2} \in ℝ^{+}$
252	251	rpreccld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to \frac{1}{{(2 \cdot N + 1)}^{2}} \in ℝ^{+}$
253	210	adantl	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to n \in ℤ$
254	252 253	rpexpcld	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} \in ℝ^{+}$
255	244 236 254	lemul1d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1} \leq 1 \leftrightarrow (\frac{1}{2 n + 1}) {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} \leq 1 {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n})$
256	243 255	mpbid	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} \leq 1 {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
257	202	mulid2d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to 1 {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} = {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
258	256 257	breqtrd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n} \leq {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
259	226 258	eqbrtrd	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n} \leq {(\frac{1}{{(2 \cdot N + 1)}^{2}})}^{n}$
260	259 185 203	3brtr4d	$⊢ (N \in ℕ \land n \in (1 \dots j)) \to K (n) \leq L (n)$
261	260	adantlr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to K (n) \leq L (n)$
262	145 196 207 261	serle	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ K) (j) \leq seq 1 (+ L) (j)$
263	5 6 8 143 199 208 262	climle	$⊢ N \in ℕ \to B (N) - B (N + 1) \leq (\frac{1}{4}) (\frac{1}{N (N + 1)})$

Metamath Proof Explorer

Theorem stirlinglem10

Proof