stirlinglem12

Description: The sequence B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem12.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
	stirlinglem12.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
	stirlinglem12.3	$⊢ F = (n \in ℕ ⟼ \frac{1}{n (n + 1)})$
Assertion	stirlinglem12	$⊢ N \in ℕ \to B (1) - (\frac{1}{4}) \leq B (N)$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem12.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
2		stirlinglem12.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
3		stirlinglem12.3	$⊢ F = (n \in ℕ ⟼ \frac{1}{n (n + 1)})$
4		1nn	$⊢ 1 \in ℕ$
5	1	stirlinglem2	$⊢ 1 \in ℕ \to A (1) \in ℝ^{+}$
6		relogcl	$⊢ A (1) \in ℝ^{+} \to \log A (1) \in ℝ$
7	4 5 6	mp2b	$⊢ \log A (1) \in ℝ$
8		nfcv	$⊢ \underline{Ⅎ} n 1$
9		nfcv	$⊢ \underline{Ⅎ} n log$
10		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
11	1 10	nfcxfr	$⊢ \underline{Ⅎ} n A$
12	11 8	nffv	$⊢ \underline{Ⅎ} n A (1)$
13	9 12	nffv	$⊢ \underline{Ⅎ} n \log A (1)$
14		2fveq3	$⊢ n = 1 \to \log A (n) = \log A (1)$
15	8 13 14 2	fvmptf	$⊢ (1 \in ℕ \land \log A (1) \in ℝ) \to B (1) = \log A (1)$
16	4 7 15	mp2an	$⊢ B (1) = \log A (1)$
17	16 7	eqeltri	$⊢ B (1) \in ℝ$
18	17	a1i	$⊢ N \in ℕ \to B (1) \in ℝ$
19	1	stirlinglem2	$⊢ N \in ℕ \to A (N) \in ℝ^{+}$
20	19	relogcld	$⊢ N \in ℕ \to \log A (N) \in ℝ$
21		nfcv	$⊢ \underline{Ⅎ} n N$
22	11 21	nffv	$⊢ \underline{Ⅎ} n A (N)$
23	9 22	nffv	$⊢ \underline{Ⅎ} n \log A (N)$
24		2fveq3	$⊢ n = N \to \log A (n) = \log A (N)$
25	21 23 24 2	fvmptf	$⊢ (N \in ℕ \land \log A (N) \in ℝ) \to B (N) = \log A (N)$
26	20 25	mpdan	$⊢ N \in ℕ \to B (N) = \log A (N)$
27	26 20	eqeltrd	$⊢ N \in ℕ \to B (N) \in ℝ$
28		4re	$⊢ 4 \in ℝ$
29		4ne0	$⊢ 4 \neq 0$
30	28 29	rereccli	$⊢ \frac{1}{4} \in ℝ$
31	30	a1i	$⊢ N \in ℕ \to \frac{1}{4} \in ℝ$
32		fveq2	$⊢ k = j \to B (k) = B (j)$
33		fveq2	$⊢ k = j + 1 \to B (k) = B (j + 1)$
34		fveq2	$⊢ k = 1 \to B (k) = B (1)$
35		fveq2	$⊢ k = N \to B (k) = B (N)$
36		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
37	36	biimpi	$⊢ N \in ℕ \to N \in ℤ_{\geq 1}$
38		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
39	1	stirlinglem2	$⊢ k \in ℕ \to A (k) \in ℝ^{+}$
40	38 39	syl	$⊢ k \in (1 \dots N) \to A (k) \in ℝ^{+}$
41	40	relogcld	$⊢ k \in (1 \dots N) \to \log A (k) \in ℝ$
42		nfcv	$⊢ \underline{Ⅎ} n k$
43	11 42	nffv	$⊢ \underline{Ⅎ} n A (k)$
44	9 43	nffv	$⊢ \underline{Ⅎ} n \log A (k)$
45		2fveq3	$⊢ n = k \to \log A (n) = \log A (k)$
46	42 44 45 2	fvmptf	$⊢ (k \in ℕ \land \log A (k) \in ℝ) \to B (k) = \log A (k)$
47	38 41 46	syl2anc	$⊢ k \in (1 \dots N) \to B (k) = \log A (k)$
48	47	adantl	$⊢ (N \in ℕ \land k \in (1 \dots N)) \to B (k) = \log A (k)$
49	40	rpcnd	$⊢ k \in (1 \dots N) \to A (k) \in ℂ$
50	49	adantl	$⊢ (N \in ℕ \land k \in (1 \dots N)) \to A (k) \in ℂ$
51	39	rpne0d	$⊢ k \in ℕ \to A (k) \neq 0$
52	38 51	syl	$⊢ k \in (1 \dots N) \to A (k) \neq 0$
53	52	adantl	$⊢ (N \in ℕ \land k \in (1 \dots N)) \to A (k) \neq 0$
54	50 53	logcld	$⊢ (N \in ℕ \land k \in (1 \dots N)) \to \log A (k) \in ℂ$
55	48 54	eqeltrd	$⊢ (N \in ℕ \land k \in (1 \dots N)) \to B (k) \in ℂ$
56	32 33 34 35 37 55	telfsumo	$⊢ N \in ℕ \to \sum_{j \in (1 ..^N)} (B (j) - B (j + 1)) = B (1) - B (N)$
57		nnz	$⊢ N \in ℕ \to N \in ℤ$
58		fzoval	$⊢ N \in ℤ \to (1 ..^N) = (1 \dots N - 1)$
59	57 58	syl	$⊢ N \in ℕ \to (1 ..^N) = (1 \dots N - 1)$
60	59	sumeq1d	$⊢ N \in ℕ \to \sum_{j \in (1 ..^N)} (B (j) - B (j + 1)) = \sum_{j = 1}^{N - 1} (B (j) - B (j + 1))$
61	56 60	eqtr3d	$⊢ N \in ℕ \to B (1) - B (N) = \sum_{j = 1}^{N - 1} (B (j) - B (j + 1))$
62		fzfid	$⊢ N \in ℕ \to (1 \dots N - 1) \in Fin$
63		elfznn	$⊢ j \in (1 \dots N - 1) \to j \in ℕ$
64	63	adantl	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to j \in ℕ$
65	1	stirlinglem2	$⊢ j \in ℕ \to A (j) \in ℝ^{+}$
66	65	relogcld	$⊢ j \in ℕ \to \log A (j) \in ℝ$
67		nfcv	$⊢ \underline{Ⅎ} n j$
68	11 67	nffv	$⊢ \underline{Ⅎ} n A (j)$
69	9 68	nffv	$⊢ \underline{Ⅎ} n \log A (j)$
70		2fveq3	$⊢ n = j \to \log A (n) = \log A (j)$
71	67 69 70 2	fvmptf	$⊢ (j \in ℕ \land \log A (j) \in ℝ) \to B (j) = \log A (j)$
72	66 71	mpdan	$⊢ j \in ℕ \to B (j) = \log A (j)$
73	72 66	eqeltrd	$⊢ j \in ℕ \to B (j) \in ℝ$
74	64 73	syl	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to B (j) \in ℝ$
75		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
76	1	stirlinglem2	$⊢ j + 1 \in ℕ \to A (j + 1) \in ℝ^{+}$
77	75 76	syl	$⊢ j \in ℕ \to A (j + 1) \in ℝ^{+}$
78	77	relogcld	$⊢ j \in ℕ \to \log A (j + 1) \in ℝ$
79		nfcv	$⊢ \underline{Ⅎ} n (j + 1)$
80	11 79	nffv	$⊢ \underline{Ⅎ} n A (j + 1)$
81	9 80	nffv	$⊢ \underline{Ⅎ} n \log A (j + 1)$
82		2fveq3	$⊢ n = j + 1 \to \log A (n) = \log A (j + 1)$
83	79 81 82 2	fvmptf	$⊢ (j + 1 \in ℕ \land \log A (j + 1) \in ℝ) \to B (j + 1) = \log A (j + 1)$
84	75 78 83	syl2anc	$⊢ j \in ℕ \to B (j + 1) = \log A (j + 1)$
85	84 78	eqeltrd	$⊢ j \in ℕ \to B (j + 1) \in ℝ$
86	63 85	syl	$⊢ j \in (1 \dots N - 1) \to B (j + 1) \in ℝ$
87	86	adantl	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to B (j + 1) \in ℝ$
88	74 87	resubcld	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to B (j) - B (j + 1) \in ℝ$
89	62 88	fsumrecl	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (B (j) - B (j + 1)) \in ℝ$
90	30	a1i	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to \frac{1}{4} \in ℝ$
91	63	nnred	$⊢ j \in (1 \dots N - 1) \to j \in ℝ$
92		1red	$⊢ j \in (1 \dots N - 1) \to 1 \in ℝ$
93	91 92	readdcld	$⊢ j \in (1 \dots N - 1) \to j + 1 \in ℝ$
94	91 93	remulcld	$⊢ j \in (1 \dots N - 1) \to j (j + 1) \in ℝ$
95	91	recnd	$⊢ j \in (1 \dots N - 1) \to j \in ℂ$
96		1cnd	$⊢ j \in (1 \dots N - 1) \to 1 \in ℂ$
97	95 96	addcld	$⊢ j \in (1 \dots N - 1) \to j + 1 \in ℂ$
98	63	nnne0d	$⊢ j \in (1 \dots N - 1) \to j \neq 0$
99	75	nnne0d	$⊢ j \in ℕ \to j + 1 \neq 0$
100	63 99	syl	$⊢ j \in (1 \dots N - 1) \to j + 1 \neq 0$
101	95 97 98 100	mulne0d	$⊢ j \in (1 \dots N - 1) \to j (j + 1) \neq 0$
102	94 101	rereccld	$⊢ j \in (1 \dots N - 1) \to \frac{1}{j (j + 1)} \in ℝ$
103	102	adantl	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to \frac{1}{j (j + 1)} \in ℝ$
104	90 103	remulcld	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to (\frac{1}{4}) (\frac{1}{j (j + 1)}) \in ℝ$
105	62 104	fsumrecl	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{4}) (\frac{1}{j (j + 1)}) \in ℝ$
106		eqid	$⊢ (i \in ℕ ⟼ (\frac{1}{2 i + 1}) {(\frac{1}{2 j + 1})}^{2 i}) = (i \in ℕ ⟼ (\frac{1}{2 i + 1}) {(\frac{1}{2 j + 1})}^{2 i})$
107		eqid	$⊢ (i \in ℕ ⟼ {(\frac{1}{{(2 j + 1)}^{2}})}^{i}) = (i \in ℕ ⟼ {(\frac{1}{{(2 j + 1)}^{2}})}^{i})$
108	1 2 106 107	stirlinglem10	$⊢ j \in ℕ \to B (j) - B (j + 1) \leq (\frac{1}{4}) (\frac{1}{j (j + 1)})$
109	64 108	syl	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to B (j) - B (j + 1) \leq (\frac{1}{4}) (\frac{1}{j (j + 1)})$
110	62 88 104 109	fsumle	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (B (j) - B (j + 1)) \leq \sum_{j = 1}^{N - 1} (\frac{1}{4}) (\frac{1}{j (j + 1)})$
111	62 103	fsumrecl	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) \in ℝ$
112		1red	$⊢ N \in ℕ \to 1 \in ℝ$
113		4pos	$⊢ 0 < 4$
114	28 113	elrpii	$⊢ 4 \in ℝ^{+}$
115	114	a1i	$⊢ N \in ℕ \to 4 \in ℝ^{+}$
116		0red	$⊢ N \in ℕ \to 0 \in ℝ$
117		0lt1	$⊢ 0 < 1$
118	117	a1i	$⊢ N \in ℕ \to 0 < 1$
119	116 112 118	ltled	$⊢ N \in ℕ \to 0 \leq 1$
120	112 115 119	divge0d	$⊢ N \in ℕ \to 0 \leq \frac{1}{4}$
121		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
122		eluznn	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j \in ℕ$
123	3	a1i	$⊢ j \in ℕ \to F = (n \in ℕ ⟼ \frac{1}{n (n + 1)})$
124		simpr	$⊢ (j \in ℕ \land n = j) \to n = j$
125	124	oveq1d	$⊢ (j \in ℕ \land n = j) \to n + 1 = j + 1$
126	124 125	oveq12d	$⊢ (j \in ℕ \land n = j) \to n (n + 1) = j (j + 1)$
127	126	oveq2d	$⊢ (j \in ℕ \land n = j) \to \frac{1}{n (n + 1)} = \frac{1}{j (j + 1)}$
128		id	$⊢ j \in ℕ \to j \in ℕ$
129		nnre	$⊢ j \in ℕ \to j \in ℝ$
130		1red	$⊢ j \in ℕ \to 1 \in ℝ$
131	129 130	readdcld	$⊢ j \in ℕ \to j + 1 \in ℝ$
132	129 131	remulcld	$⊢ j \in ℕ \to j (j + 1) \in ℝ$
133		nncn	$⊢ j \in ℕ \to j \in ℂ$
134		1cnd	$⊢ j \in ℕ \to 1 \in ℂ$
135	133 134	addcld	$⊢ j \in ℕ \to j + 1 \in ℂ$
136		nnne0	$⊢ j \in ℕ \to j \neq 0$
137	133 135 136 99	mulne0d	$⊢ j \in ℕ \to j (j + 1) \neq 0$
138	132 137	rereccld	$⊢ j \in ℕ \to \frac{1}{j (j + 1)} \in ℝ$
139	123 127 128 138	fvmptd	$⊢ j \in ℕ \to F (j) = \frac{1}{j (j + 1)}$
140	122 139	syl	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to F (j) = \frac{1}{j (j + 1)}$
141	122	nnred	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j \in ℝ$
142		1red	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to 1 \in ℝ$
143	141 142	readdcld	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j + 1 \in ℝ$
144	141 143	remulcld	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j (j + 1) \in ℝ$
145	141	recnd	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j \in ℂ$
146		1cnd	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to 1 \in ℂ$
147	145 146	addcld	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j + 1 \in ℂ$
148	122	nnne0d	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j \neq 0$
149	122 99	syl	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j + 1 \neq 0$
150	145 147 148 149	mulne0d	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j (j + 1) \neq 0$
151	144 150	rereccld	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to \frac{1}{j (j + 1)} \in ℝ$
152		seqeq1	$⊢ N = 1 \to seq N (+ F) = seq 1 (+ F)$
153	3	trireciplem	$⊢ seq 1 (+ F) ⇝ 1$
154		climrel	$⊢ Rel ⇝$
155	154	releldmi	$⊢ seq 1 (+ F) ⇝ 1 \to seq 1 (+ F) \in dom ⇝$
156	153 155	mp1i	$⊢ N = 1 \to seq 1 (+ F) \in dom ⇝$
157	152 156	eqeltrd	$⊢ N = 1 \to seq N (+ F) \in dom ⇝$
158	157	adantl	$⊢ (N \in ℕ \land N = 1) \to seq N (+ F) \in dom ⇝$
159		simpl	$⊢ (N \in ℕ \land \neg N = 1) \to N \in ℕ$
160		simpr	$⊢ (N \in ℕ \land \neg N = 1) \to \neg N = 1$
161		elnn1uz2	$⊢ N \in ℕ \leftrightarrow (N = 1 \lor N \in ℤ_{\geq 2})$
162	159 161	sylib	$⊢ (N \in ℕ \land \neg N = 1) \to (N = 1 \lor N \in ℤ_{\geq 2})$
163	162	ord	$⊢ (N \in ℕ \land \neg N = 1) \to (\neg N = 1 \to N \in ℤ_{\geq 2})$
164	160 163	mpd	$⊢ (N \in ℕ \land \neg N = 1) \to N \in ℤ_{\geq 2}$
165		uz2m1nn	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℕ$
166	164 165	syl	$⊢ (N \in ℕ \land \neg N = 1) \to N - 1 \in ℕ$
167		nncn	$⊢ N \in ℕ \to N \in ℂ$
168	167	adantr	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to N \in ℂ$
169		1cnd	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to 1 \in ℂ$
170	168 169	npcand	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to N - 1 + 1 = N$
171	170	eqcomd	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to N = N - 1 + 1$
172	171	seqeq1d	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to seq N (+ F) = seq (N - 1 + 1) (+ F)$
173		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
174		id	$⊢ N - 1 \in ℕ \to N - 1 \in ℕ$
175	138	recnd	$⊢ j \in ℕ \to \frac{1}{j (j + 1)} \in ℂ$
176	139 175	eqeltrd	$⊢ j \in ℕ \to F (j) \in ℂ$
177	176	adantl	$⊢ (N - 1 \in ℕ \land j \in ℕ) \to F (j) \in ℂ$
178	153	a1i	$⊢ N - 1 \in ℕ \to seq 1 (+ F) ⇝ 1$
179	173 174 177 178	clim2ser	$⊢ N - 1 \in ℕ \to seq (N - 1 + 1) (+ F) ⇝ (1 - seq 1 (+ F) (N - 1))$
180	179	adantl	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to seq (N - 1 + 1) (+ F) ⇝ (1 - seq 1 (+ F) (N - 1))$
181	172 180	eqbrtrd	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to seq N (+ F) ⇝ (1 - seq 1 (+ F) (N - 1))$
182	154	releldmi	$⊢ seq N (+ F) ⇝ (1 - seq 1 (+ F) (N - 1)) \to seq N (+ F) \in dom ⇝$
183	181 182	syl	$⊢ (N \in ℕ \land N - 1 \in ℕ) \to seq N (+ F) \in dom ⇝$
184	159 166 183	syl2anc	$⊢ (N \in ℕ \land \neg N = 1) \to seq N (+ F) \in dom ⇝$
185	158 184	pm2.61dan	$⊢ N \in ℕ \to seq N (+ F) \in dom ⇝$
186	121 57 140 151 185	isumrecl	$⊢ N \in ℕ \to \sum_{j \in ℤ_{\geq N}} (\frac{1}{j (j + 1)}) \in ℝ$
187	122	nnrpd	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j \in ℝ^{+}$
188	187	rpge0d	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to 0 \leq j$
189	141 188	ge0p1rpd	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j + 1 \in ℝ^{+}$
190	187 189	rpmulcld	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to j (j + 1) \in ℝ^{+}$
191	119	adantr	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to 0 \leq 1$
192	142 190 191	divge0d	$⊢ (N \in ℕ \land j \in ℤ_{\geq N}) \to 0 \leq \frac{1}{j (j + 1)}$
193	121 57 140 151 185 192	isumge0	$⊢ N \in ℕ \to 0 \leq \sum_{j \in ℤ_{\geq N}} (\frac{1}{j (j + 1)})$
194	116 186 111 193	leadd2dd	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) + 0 \leq \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) + \sum_{j \in ℤ_{\geq N}} (\frac{1}{j (j + 1)})$
195	111	recnd	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) \in ℂ$
196	195	addridd	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) + 0 = \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)})$
197	196	eqcomd	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) = \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) + 0$
198		id	$⊢ N \in ℕ \to N \in ℕ$
199	139	adantl	$⊢ (N \in ℕ \land j \in ℕ) \to F (j) = \frac{1}{j (j + 1)}$
200	133	adantl	$⊢ (N \in ℕ \land j \in ℕ) \to j \in ℂ$
201		1cnd	$⊢ (N \in ℕ \land j \in ℕ) \to 1 \in ℂ$
202	200 201	addcld	$⊢ (N \in ℕ \land j \in ℕ) \to j + 1 \in ℂ$
203	200 202	mulcld	$⊢ (N \in ℕ \land j \in ℕ) \to j (j + 1) \in ℂ$
204	136	adantl	$⊢ (N \in ℕ \land j \in ℕ) \to j \neq 0$
205	99	adantl	$⊢ (N \in ℕ \land j \in ℕ) \to j + 1 \neq 0$
206	200 202 204 205	mulne0d	$⊢ (N \in ℕ \land j \in ℕ) \to j (j + 1) \neq 0$
207	203 206	reccld	$⊢ (N \in ℕ \land j \in ℕ) \to \frac{1}{j (j + 1)} \in ℂ$
208	153 155	mp1i	$⊢ N \in ℕ \to seq 1 (+ F) \in dom ⇝$
209	173 121 198 199 207 208	isumsplit	$⊢ N \in ℕ \to \sum_{j \in ℕ} (\frac{1}{j (j + 1)}) = \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) + \sum_{j \in ℤ_{\geq N}} (\frac{1}{j (j + 1)})$
210	194 197 209	3brtr4d	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) \leq \sum_{j \in ℕ} (\frac{1}{j (j + 1)})$
211		1zzd	$⊢ ⊤ \to 1 \in ℤ$
212	139	adantl	$⊢ (⊤ \land j \in ℕ) \to F (j) = \frac{1}{j (j + 1)}$
213	175	adantl	$⊢ (⊤ \land j \in ℕ) \to \frac{1}{j (j + 1)} \in ℂ$
214	153	a1i	$⊢ ⊤ \to seq 1 (+ F) ⇝ 1$
215	173 211 212 213 214	isumclim	$⊢ ⊤ \to \sum_{j \in ℕ} (\frac{1}{j (j + 1)}) = 1$
216	215	mptru	$⊢ \sum_{j \in ℕ} (\frac{1}{j (j + 1)}) = 1$
217	210 216	breqtrdi	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) \leq 1$
218	111 112 31 120 217	lemul2ad	$⊢ N \in ℕ \to (\frac{1}{4}) \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) \leq (\frac{1}{4}) \cdot 1$
219		4cn	$⊢ 4 \in ℂ$
220	219	a1i	$⊢ N \in ℕ \to 4 \in ℂ$
221	113	a1i	$⊢ N \in ℕ \to 0 < 4$
222	221	gt0ne0d	$⊢ N \in ℕ \to 4 \neq 0$
223	220 222	reccld	$⊢ N \in ℕ \to \frac{1}{4} \in ℂ$
224	103	recnd	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to \frac{1}{j (j + 1)} \in ℂ$
225	62 223 224	fsummulc2	$⊢ N \in ℕ \to (\frac{1}{4}) \sum_{j = 1}^{N - 1} (\frac{1}{j (j + 1)}) = \sum_{j = 1}^{N - 1} (\frac{1}{4}) (\frac{1}{j (j + 1)})$
226	223	mulridd	$⊢ N \in ℕ \to (\frac{1}{4}) \cdot 1 = \frac{1}{4}$
227	218 225 226	3brtr3d	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (\frac{1}{4}) (\frac{1}{j (j + 1)}) \leq \frac{1}{4}$
228	89 105 31 110 227	letrd	$⊢ N \in ℕ \to \sum_{j = 1}^{N - 1} (B (j) - B (j + 1)) \leq \frac{1}{4}$
229	61 228	eqbrtrd	$⊢ N \in ℕ \to B (1) - B (N) \leq \frac{1}{4}$
230	18 27 31 229	subled	$⊢ N \in ℕ \to B (1) - (\frac{1}{4}) \leq B (N)$

Metamath Proof Explorer

Theorem stirlinglem12

Proof