bclbnd

Description: A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014)

		Ref	Expression
	Assertion	bclbnd	$⊢ N \in ℤ_{\geq 4} \to \frac{4^{N}}{N} < (\binom{2 \cdot N}{N})$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 4 \to 4^{x} = 4^{4}$
2		id	$⊢ x = 4 \to x = 4$
3	1 2	oveq12d	$⊢ x = 4 \to \frac{4^{x}}{x} = \frac{4^{4}}{4}$
4		oveq2	$⊢ x = 4 \to 2 x = 2 \cdot 4$
5	4 2	oveq12d	$⊢ x = 4 \to (\binom{2 x}{x}) = (\binom{2 \cdot 4}{4})$
6	3 5	breq12d	$⊢ x = 4 \to (\frac{4^{x}}{x} < (\binom{2 x}{x}) \leftrightarrow \frac{4^{4}}{4} < (\binom{2 \cdot 4}{4}))$
7		oveq2	$⊢ x = n \to 4^{x} = 4^{n}$
8		id	$⊢ x = n \to x = n$
9	7 8	oveq12d	$⊢ x = n \to \frac{4^{x}}{x} = \frac{4^{n}}{n}$
10		oveq2	$⊢ x = n \to 2 x = 2 n$
11	10 8	oveq12d	$⊢ x = n \to (\binom{2 x}{x}) = (\binom{2 n}{n})$
12	9 11	breq12d	$⊢ x = n \to (\frac{4^{x}}{x} < (\binom{2 x}{x}) \leftrightarrow \frac{4^{n}}{n} < (\binom{2 n}{n}))$
13		oveq2	$⊢ x = n + 1 \to 4^{x} = 4^{n + 1}$
14		id	$⊢ x = n + 1 \to x = n + 1$
15	13 14	oveq12d	$⊢ x = n + 1 \to \frac{4^{x}}{x} = \frac{4^{n + 1}}{n + 1}$
16		oveq2	$⊢ x = n + 1 \to 2 x = 2 (n + 1)$
17	16 14	oveq12d	$⊢ x = n + 1 \to (\binom{2 x}{x}) = (\binom{2 (n + 1)}{n + 1})$
18	15 17	breq12d	$⊢ x = n + 1 \to (\frac{4^{x}}{x} < (\binom{2 x}{x}) \leftrightarrow \frac{4^{n + 1}}{n + 1} < (\binom{2 (n + 1)}{n + 1}))$
19		oveq2	$⊢ x = N \to 4^{x} = 4^{N}$
20		id	$⊢ x = N \to x = N$
21	19 20	oveq12d	$⊢ x = N \to \frac{4^{x}}{x} = \frac{4^{N}}{N}$
22		oveq2	$⊢ x = N \to 2 x = 2 \cdot N$
23	22 20	oveq12d	$⊢ x = N \to (\binom{2 x}{x}) = (\binom{2 \cdot N}{N})$
24	21 23	breq12d	$⊢ x = N \to (\frac{4^{x}}{x} < (\binom{2 x}{x}) \leftrightarrow \frac{4^{N}}{N} < (\binom{2 \cdot N}{N}))$
25		6nn0	$⊢ 6 \in ℕ_{0}$
26		7nn0	$⊢ 7 \in ℕ_{0}$
27		4nn0	$⊢ 4 \in ℕ_{0}$
28		0nn0	$⊢ 0 \in ℕ_{0}$
29		4lt10	$⊢ 4 < 10$
30		6lt7	$⊢ 6 < 7$
31	25 26 27 28 29 30	decltc	$⊢ 64 < 70$
32		2cn	$⊢ 2 \in ℂ$
33		2nn0	$⊢ 2 \in ℕ_{0}$
34		3nn0	$⊢ 3 \in ℕ_{0}$
35		expmul	$⊢ (2 \in ℂ \land 2 \in ℕ_{0} \land 3 \in ℕ_{0}) \to 2^{2 \cdot 3} = {(2^{2})}^{3}$
36	32 33 34 35	mp3an	$⊢ 2^{2 \cdot 3} = {(2^{2})}^{3}$
37		sq2	$⊢ 2^{2} = 4$
38	37	eqcomi	$⊢ 4 = 2^{2}$
39		4m1e3	$⊢ 4 - 1 = 3$
40	38 39	oveq12i	$⊢ 4^{4 - 1} = {(2^{2})}^{3}$
41	36 40	eqtr4i	$⊢ 2^{2 \cdot 3} = 4^{4 - 1}$
42		3cn	$⊢ 3 \in ℂ$
43		3t2e6	$⊢ 3 \cdot 2 = 6$
44	42 32 43	mulcomli	$⊢ 2 \cdot 3 = 6$
45	44	oveq2i	$⊢ 2^{2 \cdot 3} = 2^{6}$
46		2exp6	$⊢ 2^{6} = 64$
47	45 46	eqtri	$⊢ 2^{2 \cdot 3} = 64$
48		4cn	$⊢ 4 \in ℂ$
49		4ne0	$⊢ 4 \neq 0$
50		4z	$⊢ 4 \in ℤ$
51		expm1	$⊢ (4 \in ℂ \land 4 \neq 0 \land 4 \in ℤ) \to 4^{4 - 1} = \frac{4^{4}}{4}$
52	48 49 50 51	mp3an	$⊢ 4^{4 - 1} = \frac{4^{4}}{4}$
53	41 47 52	3eqtr3ri	$⊢ \frac{4^{4}}{4} = 64$
54		df-4	$⊢ 4 = 3 + 1$
55	54	oveq2i	$⊢ 2 \cdot 4 = 2 (3 + 1)$
56	55 54	oveq12i	$⊢ (\binom{2 \cdot 4}{4}) = (\binom{2 (3 + 1)}{3 + 1})$
57		bcp1ctr	$⊢ 3 \in ℕ_{0} \to (\binom{2 (3 + 1)}{3 + 1}) = (\binom{2 \cdot 3}{3}) 2 (\frac{2 \cdot 3 + 1}{3 + 1})$
58	34 57	ax-mp	$⊢ (\binom{2 (3 + 1)}{3 + 1}) = (\binom{2 \cdot 3}{3}) 2 (\frac{2 \cdot 3 + 1}{3 + 1})$
59		df-3	$⊢ 3 = 2 + 1$
60	59	oveq2i	$⊢ 2 \cdot 3 = 2 (2 + 1)$
61	60 59	oveq12i	$⊢ (\binom{2 \cdot 3}{3}) = (\binom{2 (2 + 1)}{2 + 1})$
62		bcp1ctr	$⊢ 2 \in ℕ_{0} \to (\binom{2 (2 + 1)}{2 + 1}) = (\binom{2 \cdot 2}{2}) 2 (\frac{2 \cdot 2 + 1}{2 + 1})$
63	33 62	ax-mp	$⊢ (\binom{2 (2 + 1)}{2 + 1}) = (\binom{2 \cdot 2}{2}) 2 (\frac{2 \cdot 2 + 1}{2 + 1})$
64		df-2	$⊢ 2 = 1 + 1$
65	64	oveq2i	$⊢ 2 \cdot 2 = 2 (1 + 1)$
66	65 64	oveq12i	$⊢ (\binom{2 \cdot 2}{2}) = (\binom{2 (1 + 1)}{1 + 1})$
67		1nn0	$⊢ 1 \in ℕ_{0}$
68		bcp1ctr	$⊢ 1 \in ℕ_{0} \to (\binom{2 (1 + 1)}{1 + 1}) = (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1})$
69	67 68	ax-mp	$⊢ (\binom{2 (1 + 1)}{1 + 1}) = (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1})$
70		1e0p1	$⊢ 1 = 0 + 1$
71	70	oveq2i	$⊢ 2 \cdot 1 = 2 (0 + 1)$
72	71 70	oveq12i	$⊢ (\binom{2 \cdot 1}{1}) = (\binom{2 (0 + 1)}{0 + 1})$
73		bcp1ctr	$⊢ 0 \in ℕ_{0} \to (\binom{2 (0 + 1)}{0 + 1}) = (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1})$
74	28 73	ax-mp	$⊢ (\binom{2 (0 + 1)}{0 + 1}) = (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1})$
75	33 28	nn0mulcli	$⊢ 2 \cdot 0 \in ℕ_{0}$
76		bcn0	$⊢ 2 \cdot 0 \in ℕ_{0} \to (\binom{2 \cdot 0}{0}) = 1$
77	75 76	ax-mp	$⊢ (\binom{2 \cdot 0}{0}) = 1$
78		2t0e0	$⊢ 2 \cdot 0 = 0$
79	78	oveq1i	$⊢ 2 \cdot 0 + 1 = 0 + 1$
80	79 70	eqtr4i	$⊢ 2 \cdot 0 + 1 = 1$
81	70	eqcomi	$⊢ 0 + 1 = 1$
82	80 81	oveq12i	$⊢ \frac{2 \cdot 0 + 1}{0 + 1} = \frac{1}{1}$
83		1div1e1	$⊢ \frac{1}{1} = 1$
84	82 83	eqtri	$⊢ \frac{2 \cdot 0 + 1}{0 + 1} = 1$
85	84	oveq2i	$⊢ 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 2 \cdot 1$
86		2t1e2	$⊢ 2 \cdot 1 = 2$
87	85 86	eqtri	$⊢ 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 2$
88	77 87	oveq12i	$⊢ (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 1 \cdot 2$
89	32	mulid2i	$⊢ 1 \cdot 2 = 2$
90	88 89	eqtri	$⊢ (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 2$
91	72 74 90	3eqtri	$⊢ (\binom{2 \cdot 1}{1}) = 2$
92	86	oveq1i	$⊢ 2 \cdot 1 + 1 = 2 + 1$
93	92 59	eqtr4i	$⊢ 2 \cdot 1 + 1 = 3$
94	64	eqcomi	$⊢ 1 + 1 = 2$
95	93 94	oveq12i	$⊢ \frac{2 \cdot 1 + 1}{1 + 1} = \frac{3}{2}$
96	95	oveq2i	$⊢ 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 2 (\frac{3}{2})$
97		2ne0	$⊢ 2 \neq 0$
98	42 32 97	divcan2i	$⊢ 2 (\frac{3}{2}) = 3$
99	96 98	eqtri	$⊢ 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 3$
100	91 99	oveq12i	$⊢ (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 2 \cdot 3$
101	100 44	eqtri	$⊢ (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 6$
102	66 69 101	3eqtri	$⊢ (\binom{2 \cdot 2}{2}) = 6$
103		2t2e4	$⊢ 2 \cdot 2 = 4$
104	103	oveq1i	$⊢ 2 \cdot 2 + 1 = 4 + 1$
105		df-5	$⊢ 5 = 4 + 1$
106	104 105	eqtr4i	$⊢ 2 \cdot 2 + 1 = 5$
107	59	eqcomi	$⊢ 2 + 1 = 3$
108	106 107	oveq12i	$⊢ \frac{2 \cdot 2 + 1}{2 + 1} = \frac{5}{3}$
109	108	oveq2i	$⊢ 2 (\frac{2 \cdot 2 + 1}{2 + 1}) = 2 (\frac{5}{3})$
110		5cn	$⊢ 5 \in ℂ$
111		3ne0	$⊢ 3 \neq 0$
112	32 110 42 111	divassi	$⊢ \frac{2 \cdot 5}{3} = 2 (\frac{5}{3})$
113	109 112	eqtr4i	$⊢ 2 (\frac{2 \cdot 2 + 1}{2 + 1}) = \frac{2 \cdot 5}{3}$
114	102 113	oveq12i	$⊢ (\binom{2 \cdot 2}{2}) 2 (\frac{2 \cdot 2 + 1}{2 + 1}) = 6 (\frac{2 \cdot 5}{3})$
115	63 114	eqtri	$⊢ (\binom{2 (2 + 1)}{2 + 1}) = 6 (\frac{2 \cdot 5}{3})$
116		6cn	$⊢ 6 \in ℂ$
117		2nn	$⊢ 2 \in ℕ$
118		5nn	$⊢ 5 \in ℕ$
119	117 118	nnmulcli	$⊢ 2 \cdot 5 \in ℕ$
120	119	nncni	$⊢ 2 \cdot 5 \in ℂ$
121	42 111	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
122		div12	$⊢ (6 \in ℂ \land 2 \cdot 5 \in ℂ \land (3 \in ℂ \land 3 \neq 0)) \to 6 (\frac{2 \cdot 5}{3}) = 2 \cdot 5 (\frac{6}{3})$
123	116 120 121 122	mp3an	$⊢ 6 (\frac{2 \cdot 5}{3}) = 2 \cdot 5 (\frac{6}{3})$
124		5t2e10	$⊢ 5 \cdot 2 = 10$
125	110 32 124	mulcomli	$⊢ 2 \cdot 5 = 10$
126	116 42 32 111	divmuli	$⊢ \frac{6}{3} = 2 \leftrightarrow 3 \cdot 2 = 6$
127	43 126	mpbir	$⊢ \frac{6}{3} = 2$
128	125 127	oveq12i	$⊢ 2 \cdot 5 (\frac{6}{3}) = 10 \cdot 2$
129	123 128	eqtri	$⊢ 6 (\frac{2 \cdot 5}{3}) = 10 \cdot 2$
130	61 115 129	3eqtri	$⊢ (\binom{2 \cdot 3}{3}) = 10 \cdot 2$
131	44	oveq1i	$⊢ 2 \cdot 3 + 1 = 6 + 1$
132		df-7	$⊢ 7 = 6 + 1$
133	131 132	eqtr4i	$⊢ 2 \cdot 3 + 1 = 7$
134		3p1e4	$⊢ 3 + 1 = 4$
135	133 134	oveq12i	$⊢ \frac{2 \cdot 3 + 1}{3 + 1} = \frac{7}{4}$
136	135	oveq2i	$⊢ 2 (\frac{2 \cdot 3 + 1}{3 + 1}) = 2 (\frac{7}{4})$
137	130 136	oveq12i	$⊢ (\binom{2 \cdot 3}{3}) 2 (\frac{2 \cdot 3 + 1}{3 + 1}) = 10 \cdot 2 2 (\frac{7}{4})$
138	56 58 137	3eqtri	$⊢ (\binom{2 \cdot 4}{4}) = 10 \cdot 2 2 (\frac{7}{4})$
139		10nn	$⊢ 10 \in ℕ$
140	139	nncni	$⊢ 10 \in ℂ$
141		7cn	$⊢ 7 \in ℂ$
142	141 48 49	divcli	$⊢ \frac{7}{4} \in ℂ$
143	32 142	mulcli	$⊢ 2 (\frac{7}{4}) \in ℂ$
144	140 32 143	mulassi	$⊢ 10 \cdot 2 2 (\frac{7}{4}) = 10 2 2 (\frac{7}{4})$
145	103	oveq1i	$⊢ 2 \cdot 2 (\frac{7}{4}) = 4 (\frac{7}{4})$
146	32 32 142	mulassi	$⊢ 2 \cdot 2 (\frac{7}{4}) = 2 2 (\frac{7}{4})$
147	141 48 49	divcan2i	$⊢ 4 (\frac{7}{4}) = 7$
148	145 146 147	3eqtr3i	$⊢ 2 2 (\frac{7}{4}) = 7$
149	148	oveq2i	$⊢ 10 2 2 (\frac{7}{4}) = 10 \cdot 7$
150	144 149	eqtri	$⊢ 10 \cdot 2 2 (\frac{7}{4}) = 10 \cdot 7$
151	26	dec0u	$⊢ 10 \cdot 7 = 70$
152	138 150 151	3eqtri	$⊢ (\binom{2 \cdot 4}{4}) = 70$
153	31 53 152	3brtr4i	$⊢ \frac{4^{4}}{4} < (\binom{2 \cdot 4}{4})$
154		4nn	$⊢ 4 \in ℕ$
155		eluznn	$⊢ (4 \in ℕ \land n \in ℤ_{\geq 4}) \to n \in ℕ$
156	154 155	mpan	$⊢ n \in ℤ_{\geq 4} \to n \in ℕ$
157		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
158		nnexpcl	$⊢ (4 \in ℕ \land n \in ℕ_{0}) \to 4^{n} \in ℕ$
159	154 157 158	sylancr	$⊢ n \in ℕ \to 4^{n} \in ℕ$
160	159	nnrpd	$⊢ n \in ℕ \to 4^{n} \in ℝ^{+}$
161		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
162	160 161	rpdivcld	$⊢ n \in ℕ \to \frac{4^{n}}{n} \in ℝ^{+}$
163	162	rpred	$⊢ n \in ℕ \to \frac{4^{n}}{n} \in ℝ$
164		nnmulcl	$⊢ (2 \in ℕ \land n \in ℕ) \to 2 n \in ℕ$
165	117 164	mpan	$⊢ n \in ℕ \to 2 n \in ℕ$
166	165	nnnn0d	$⊢ n \in ℕ \to 2 n \in ℕ_{0}$
167		nnz	$⊢ n \in ℕ \to n \in ℤ$
168		bccl	$⊢ (2 n \in ℕ_{0} \land n \in ℤ) \to (\binom{2 n}{n}) \in ℕ_{0}$
169	166 167 168	syl2anc	$⊢ n \in ℕ \to (\binom{2 n}{n}) \in ℕ_{0}$
170	169	nn0red	$⊢ n \in ℕ \to (\binom{2 n}{n}) \in ℝ$
171		2rp	$⊢ 2 \in ℝ^{+}$
172	165	peano2nnd	$⊢ n \in ℕ \to 2 n + 1 \in ℕ$
173	172	nnrpd	$⊢ n \in ℕ \to 2 n + 1 \in ℝ^{+}$
174		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
175	174	nnrpd	$⊢ n \in ℕ \to n + 1 \in ℝ^{+}$
176	173 175	rpdivcld	$⊢ n \in ℕ \to \frac{2 n + 1}{n + 1} \in ℝ^{+}$
177		rpmulcl	$⊢ (2 \in ℝ^{+} \land \frac{2 n + 1}{n + 1} \in ℝ^{+}) \to 2 (\frac{2 n + 1}{n + 1}) \in ℝ^{+}$
178	171 176 177	sylancr	$⊢ n \in ℕ \to 2 (\frac{2 n + 1}{n + 1}) \in ℝ^{+}$
179	163 170 178	ltmul1d	$⊢ n \in ℕ \to (\frac{4^{n}}{n} < (\binom{2 n}{n}) \leftrightarrow (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 n}{n}) 2 (\frac{2 n + 1}{n + 1}))$
180		bcp1ctr	$⊢ n \in ℕ_{0} \to (\binom{2 (n + 1)}{n + 1}) = (\binom{2 n}{n}) 2 (\frac{2 n + 1}{n + 1})$
181	157 180	syl	$⊢ n \in ℕ \to (\binom{2 (n + 1)}{n + 1}) = (\binom{2 n}{n}) 2 (\frac{2 n + 1}{n + 1})$
182	181	breq2d	$⊢ n \in ℕ \to ((\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 (n + 1)}{n + 1}) \leftrightarrow (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 n}{n}) 2 (\frac{2 n + 1}{n + 1}))$
183	179 182	bitr4d	$⊢ n \in ℕ \to (\frac{4^{n}}{n} < (\binom{2 n}{n}) \leftrightarrow (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 (n + 1)}{n + 1}))$
184		2re	$⊢ 2 \in ℝ$
185	184	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
186	173 161	rpdivcld	$⊢ n \in ℕ \to \frac{2 n + 1}{n} \in ℝ^{+}$
187	186	rpred	$⊢ n \in ℕ \to \frac{2 n + 1}{n} \in ℝ$
188		nnmulcl	$⊢ (4^{n} \in ℕ \land 2 \in ℕ) \to 4^{n} \cdot 2 \in ℕ$
189	159 117 188	sylancl	$⊢ n \in ℕ \to 4^{n} \cdot 2 \in ℕ$
190	189	nnrpd	$⊢ n \in ℕ \to 4^{n} \cdot 2 \in ℝ^{+}$
191	190 175	rpdivcld	$⊢ n \in ℕ \to \frac{4^{n} \cdot 2}{n + 1} \in ℝ^{+}$
192	161	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
193		ltaddrp	$⊢ (2 \in ℝ \land \frac{1}{n} \in ℝ^{+}) \to 2 < 2 + (\frac{1}{n})$
194	184 192 193	sylancr	$⊢ n \in ℕ \to 2 < 2 + (\frac{1}{n})$
195	165	nncnd	$⊢ n \in ℕ \to 2 n \in ℂ$
196		1cnd	$⊢ n \in ℕ \to 1 \in ℂ$
197		nncn	$⊢ n \in ℕ \to n \in ℂ$
198		nnne0	$⊢ n \in ℕ \to n \neq 0$
199	195 196 197 198	divdird	$⊢ n \in ℕ \to \frac{2 n + 1}{n} = (\frac{2 n}{n}) + (\frac{1}{n})$
200	32	a1i	$⊢ n \in ℕ \to 2 \in ℂ$
201	200 197 198	divcan4d	$⊢ n \in ℕ \to \frac{2 n}{n} = 2$
202	201	oveq1d	$⊢ n \in ℕ \to (\frac{2 n}{n}) + (\frac{1}{n}) = 2 + (\frac{1}{n})$
203	199 202	eqtr2d	$⊢ n \in ℕ \to 2 + (\frac{1}{n}) = \frac{2 n + 1}{n}$
204	194 203	breqtrd	$⊢ n \in ℕ \to 2 < \frac{2 n + 1}{n}$
205	185 187 191 204	ltmul2dd	$⊢ n \in ℕ \to (\frac{4^{n} \cdot 2}{n + 1}) \cdot 2 < (\frac{4^{n} \cdot 2}{n + 1}) (\frac{2 n + 1}{n})$
206		expp1	$⊢ (4 \in ℂ \land n \in ℕ_{0}) \to 4^{n + 1} = 4^{n} \cdot 4$
207	48 157 206	sylancr	$⊢ n \in ℕ \to 4^{n + 1} = 4^{n} \cdot 4$
208	159	nncnd	$⊢ n \in ℕ \to 4^{n} \in ℂ$
209	208 200 200	mulassd	$⊢ n \in ℕ \to 4^{n} \cdot 2 \cdot 2 = 4^{n} 2 \cdot 2$
210	103	oveq2i	$⊢ 4^{n} 2 \cdot 2 = 4^{n} \cdot 4$
211	209 210	syl6eq	$⊢ n \in ℕ \to 4^{n} \cdot 2 \cdot 2 = 4^{n} \cdot 4$
212	207 211	eqtr4d	$⊢ n \in ℕ \to 4^{n + 1} = 4^{n} \cdot 2 \cdot 2$
213	212	oveq1d	$⊢ n \in ℕ \to \frac{4^{n + 1}}{n + 1} = \frac{4^{n} \cdot 2 \cdot 2}{n + 1}$
214	189	nncnd	$⊢ n \in ℕ \to 4^{n} \cdot 2 \in ℂ$
215	174	nncnd	$⊢ n \in ℕ \to n + 1 \in ℂ$
216	174	nnne0d	$⊢ n \in ℕ \to n + 1 \neq 0$
217	214 200 215 216	div23d	$⊢ n \in ℕ \to \frac{4^{n} \cdot 2 \cdot 2}{n + 1} = (\frac{4^{n} \cdot 2}{n + 1}) \cdot 2$
218	213 217	eqtrd	$⊢ n \in ℕ \to \frac{4^{n + 1}}{n + 1} = (\frac{4^{n} \cdot 2}{n + 1}) \cdot 2$
219	208 200 197 198	div23d	$⊢ n \in ℕ \to \frac{4^{n} \cdot 2}{n} = (\frac{4^{n}}{n}) \cdot 2$
220	219	oveq1d	$⊢ n \in ℕ \to (\frac{4^{n} \cdot 2}{n}) (\frac{2 n + 1}{n + 1}) = (\frac{4^{n}}{n}) \cdot 2 (\frac{2 n + 1}{n + 1})$
221	172	nncnd	$⊢ n \in ℕ \to 2 n + 1 \in ℂ$
222	214 197 221 215 198 216	divmul24d	$⊢ n \in ℕ \to (\frac{4^{n} \cdot 2}{n}) (\frac{2 n + 1}{n + 1}) = (\frac{4^{n} \cdot 2}{n + 1}) (\frac{2 n + 1}{n})$
223	162	rpcnd	$⊢ n \in ℕ \to \frac{4^{n}}{n} \in ℂ$
224	176	rpcnd	$⊢ n \in ℕ \to \frac{2 n + 1}{n + 1} \in ℂ$
225	223 200 224	mulassd	$⊢ n \in ℕ \to (\frac{4^{n}}{n}) \cdot 2 (\frac{2 n + 1}{n + 1}) = (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1})$
226	220 222 225	3eqtr3rd	$⊢ n \in ℕ \to (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) = (\frac{4^{n} \cdot 2}{n + 1}) (\frac{2 n + 1}{n})$
227	205 218 226	3brtr4d	$⊢ n \in ℕ \to \frac{4^{n + 1}}{n + 1} < (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1})$
228	174	nnnn0d	$⊢ n \in ℕ \to n + 1 \in ℕ_{0}$
229		nnexpcl	$⊢ (4 \in ℕ \land n + 1 \in ℕ_{0}) \to 4^{n + 1} \in ℕ$
230	154 228 229	sylancr	$⊢ n \in ℕ \to 4^{n + 1} \in ℕ$
231	230	nnrpd	$⊢ n \in ℕ \to 4^{n + 1} \in ℝ^{+}$
232	231 175	rpdivcld	$⊢ n \in ℕ \to \frac{4^{n + 1}}{n + 1} \in ℝ^{+}$
233	232	rpred	$⊢ n \in ℕ \to \frac{4^{n + 1}}{n + 1} \in ℝ$
234	178	rpred	$⊢ n \in ℕ \to 2 (\frac{2 n + 1}{n + 1}) \in ℝ$
235	163 234	remulcld	$⊢ n \in ℕ \to (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) \in ℝ$
236		nn0mulcl	$⊢ (2 \in ℕ_{0} \land n + 1 \in ℕ_{0}) \to 2 (n + 1) \in ℕ_{0}$
237	33 228 236	sylancr	$⊢ n \in ℕ \to 2 (n + 1) \in ℕ_{0}$
238	174	nnzd	$⊢ n \in ℕ \to n + 1 \in ℤ$
239		bccl	$⊢ (2 (n + 1) \in ℕ_{0} \land n + 1 \in ℤ) \to (\binom{2 (n + 1)}{n + 1}) \in ℕ_{0}$
240	237 238 239	syl2anc	$⊢ n \in ℕ \to (\binom{2 (n + 1)}{n + 1}) \in ℕ_{0}$
241	240	nn0red	$⊢ n \in ℕ \to (\binom{2 (n + 1)}{n + 1}) \in ℝ$
242		lttr	$⊢ (\frac{4^{n + 1}}{n + 1} \in ℝ \land (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) \in ℝ \land (\binom{2 (n + 1)}{n + 1}) \in ℝ) \to ((\frac{4^{n + 1}}{n + 1} < (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) \land (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 (n + 1)}{n + 1})) \to \frac{4^{n + 1}}{n + 1} < (\binom{2 (n + 1)}{n + 1}))$
243	233 235 241 242	syl3anc	$⊢ n \in ℕ \to ((\frac{4^{n + 1}}{n + 1} < (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) \land (\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 (n + 1)}{n + 1})) \to \frac{4^{n + 1}}{n + 1} < (\binom{2 (n + 1)}{n + 1}))$
244	227 243	mpand	$⊢ n \in ℕ \to ((\frac{4^{n}}{n}) 2 (\frac{2 n + 1}{n + 1}) < (\binom{2 (n + 1)}{n + 1}) \to \frac{4^{n + 1}}{n + 1} < (\binom{2 (n + 1)}{n + 1}))$
245	183 244	sylbid	$⊢ n \in ℕ \to (\frac{4^{n}}{n} < (\binom{2 n}{n}) \to \frac{4^{n + 1}}{n + 1} < (\binom{2 (n + 1)}{n + 1}))$
246	156 245	syl	$⊢ n \in ℤ_{\geq 4} \to (\frac{4^{n}}{n} < (\binom{2 n}{n}) \to \frac{4^{n + 1}}{n + 1} < (\binom{2 (n + 1)}{n + 1}))$
247	6 12 18 24 153 246	uzind4i	$⊢ N \in ℤ_{\geq 4} \to \frac{4^{N}}{N} < (\binom{2 \cdot N}{N})$

Metamath Proof Explorer

Theorem bclbnd

Proof