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

Metamath Proof Explorer

Theorem stirlinglem10

Proof