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		2t3e6	$⊢ 2 \cdot 3 = 6$
43	42	oveq2i	$⊢ 2^{2 \cdot 3} = 2^{6}$
44		2exp6	$⊢ 2^{6} = 64$
45	43 44	eqtri	$⊢ 2^{2 \cdot 3} = 64$
46		4cn	$⊢ 4 \in ℂ$
47		4ne0	$⊢ 4 \neq 0$
48		4z	$⊢ 4 \in ℤ$
49		expm1	$⊢ (4 \in ℂ \land 4 \neq 0 \land 4 \in ℤ) \to 4^{4 - 1} = \frac{4^{4}}{4}$
50	46 47 48 49	mp3an	$⊢ 4^{4 - 1} = \frac{4^{4}}{4}$
51	41 45 50	3eqtr3ri	$⊢ \frac{4^{4}}{4} = 64$
52		df-4	$⊢ 4 = 3 + 1$
53	52	oveq2i	$⊢ 2 \cdot 4 = 2 (3 + 1)$
54	53 52	oveq12i	$⊢ (\binom{2 \cdot 4}{4}) = (\binom{2 (3 + 1)}{3 + 1})$
55		bcp1ctr	$⊢ 3 \in ℕ_{0} \to (\binom{2 (3 + 1)}{3 + 1}) = (\binom{2 \cdot 3}{3}) 2 (\frac{2 \cdot 3 + 1}{3 + 1})$
56	34 55	ax-mp	$⊢ (\binom{2 (3 + 1)}{3 + 1}) = (\binom{2 \cdot 3}{3}) 2 (\frac{2 \cdot 3 + 1}{3 + 1})$
57		df-3	$⊢ 3 = 2 + 1$
58	57	oveq2i	$⊢ 2 \cdot 3 = 2 (2 + 1)$
59	58 57	oveq12i	$⊢ (\binom{2 \cdot 3}{3}) = (\binom{2 (2 + 1)}{2 + 1})$
60		bcp1ctr	$⊢ 2 \in ℕ_{0} \to (\binom{2 (2 + 1)}{2 + 1}) = (\binom{2 \cdot 2}{2}) 2 (\frac{2 \cdot 2 + 1}{2 + 1})$
61	33 60	ax-mp	$⊢ (\binom{2 (2 + 1)}{2 + 1}) = (\binom{2 \cdot 2}{2}) 2 (\frac{2 \cdot 2 + 1}{2 + 1})$
62		df-2	$⊢ 2 = 1 + 1$
63	62	oveq2i	$⊢ 2 \cdot 2 = 2 (1 + 1)$
64	63 62	oveq12i	$⊢ (\binom{2 \cdot 2}{2}) = (\binom{2 (1 + 1)}{1 + 1})$
65		1nn0	$⊢ 1 \in ℕ_{0}$
66		bcp1ctr	$⊢ 1 \in ℕ_{0} \to (\binom{2 (1 + 1)}{1 + 1}) = (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1})$
67	65 66	ax-mp	$⊢ (\binom{2 (1 + 1)}{1 + 1}) = (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1})$
68		1e0p1	$⊢ 1 = 0 + 1$
69	68	oveq2i	$⊢ 2 \cdot 1 = 2 (0 + 1)$
70	69 68	oveq12i	$⊢ (\binom{2 \cdot 1}{1}) = (\binom{2 (0 + 1)}{0 + 1})$
71		bcp1ctr	$⊢ 0 \in ℕ_{0} \to (\binom{2 (0 + 1)}{0 + 1}) = (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1})$
72	28 71	ax-mp	$⊢ (\binom{2 (0 + 1)}{0 + 1}) = (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1})$
73	33 28	nn0mulcli	$⊢ 2 \cdot 0 \in ℕ_{0}$
74		bcn0	$⊢ 2 \cdot 0 \in ℕ_{0} \to (\binom{2 \cdot 0}{0}) = 1$
75	73 74	ax-mp	$⊢ (\binom{2 \cdot 0}{0}) = 1$
76		2t0e0	$⊢ 2 \cdot 0 = 0$
77	76	oveq1i	$⊢ 2 \cdot 0 + 1 = 0 + 1$
78	77 68	eqtr4i	$⊢ 2 \cdot 0 + 1 = 1$
79	68	eqcomi	$⊢ 0 + 1 = 1$
80	78 79	oveq12i	$⊢ \frac{2 \cdot 0 + 1}{0 + 1} = \frac{1}{1}$
81		1div1e1	$⊢ \frac{1}{1} = 1$
82	80 81	eqtri	$⊢ \frac{2 \cdot 0 + 1}{0 + 1} = 1$
83	82	oveq2i	$⊢ 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 2 \cdot 1$
84		2t1e2	$⊢ 2 \cdot 1 = 2$
85	83 84	eqtri	$⊢ 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 2$
86	75 85	oveq12i	$⊢ (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 1 \cdot 2$
87	32	mullidi	$⊢ 1 \cdot 2 = 2$
88	86 87	eqtri	$⊢ (\binom{2 \cdot 0}{0}) 2 (\frac{2 \cdot 0 + 1}{0 + 1}) = 2$
89	70 72 88	3eqtri	$⊢ (\binom{2 \cdot 1}{1}) = 2$
90	84	oveq1i	$⊢ 2 \cdot 1 + 1 = 2 + 1$
91	90 57	eqtr4i	$⊢ 2 \cdot 1 + 1 = 3$
92	62	eqcomi	$⊢ 1 + 1 = 2$
93	91 92	oveq12i	$⊢ \frac{2 \cdot 1 + 1}{1 + 1} = \frac{3}{2}$
94	93	oveq2i	$⊢ 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 2 (\frac{3}{2})$
95		3cn	$⊢ 3 \in ℂ$
96		2ne0	$⊢ 2 \neq 0$
97	95 32 96	divcan2i	$⊢ 2 (\frac{3}{2}) = 3$
98	94 97	eqtri	$⊢ 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 3$
99	89 98	oveq12i	$⊢ (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 2 \cdot 3$
100	99 42	eqtri	$⊢ (\binom{2 \cdot 1}{1}) 2 (\frac{2 \cdot 1 + 1}{1 + 1}) = 6$
101	64 67 100	3eqtri	$⊢ (\binom{2 \cdot 2}{2}) = 6$
102		2t2e4	$⊢ 2 \cdot 2 = 4$
103	102	oveq1i	$⊢ 2 \cdot 2 + 1 = 4 + 1$
104		df-5	$⊢ 5 = 4 + 1$
105	103 104	eqtr4i	$⊢ 2 \cdot 2 + 1 = 5$
106	57	eqcomi	$⊢ 2 + 1 = 3$
107	105 106	oveq12i	$⊢ \frac{2 \cdot 2 + 1}{2 + 1} = \frac{5}{3}$
108	107	oveq2i	$⊢ 2 (\frac{2 \cdot 2 + 1}{2 + 1}) = 2 (\frac{5}{3})$
109		5cn	$⊢ 5 \in ℂ$
110		3ne0	$⊢ 3 \neq 0$
111	32 109 95 110	divassi	$⊢ \frac{2 \cdot 5}{3} = 2 (\frac{5}{3})$
112	108 111	eqtr4i	$⊢ 2 (\frac{2 \cdot 2 + 1}{2 + 1}) = \frac{2 \cdot 5}{3}$
113	101 112	oveq12i	$⊢ (\binom{2 \cdot 2}{2}) 2 (\frac{2 \cdot 2 + 1}{2 + 1}) = 6 (\frac{2 \cdot 5}{3})$
114	61 113	eqtri	$⊢ (\binom{2 (2 + 1)}{2 + 1}) = 6 (\frac{2 \cdot 5}{3})$
115		6cn	$⊢ 6 \in ℂ$
116		2nn	$⊢ 2 \in ℕ$
117		5nn	$⊢ 5 \in ℕ$
118	116 117	nnmulcli	$⊢ 2 \cdot 5 \in ℕ$
119	118	nncni	$⊢ 2 \cdot 5 \in ℂ$
120	95 110	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
121		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})$
122	115 119 120 121	mp3an	$⊢ 6 (\frac{2 \cdot 5}{3}) = 2 \cdot 5 (\frac{6}{3})$
123		5t2e10	$⊢ 5 \cdot 2 = 10$
124	109 32 123	mulcomli	$⊢ 2 \cdot 5 = 10$
125		3t2e6	$⊢ 3 \cdot 2 = 6$
126	115 95 32 110	divmuli	$⊢ \frac{6}{3} = 2 \leftrightarrow 3 \cdot 2 = 6$
127	125 126	mpbir	$⊢ \frac{6}{3} = 2$
128	124 127	oveq12i	$⊢ 2 \cdot 5 (\frac{6}{3}) = 10 \cdot 2$
129	122 128	eqtri	$⊢ 6 (\frac{2 \cdot 5}{3}) = 10 \cdot 2$
130	59 114 129	3eqtri	$⊢ (\binom{2 \cdot 3}{3}) = 10 \cdot 2$
131	42	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	54 56 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 46 47	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	102	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 46 47	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 51 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	116 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 116 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	46 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	102	oveq2i	$⊢ 4^{n} 2 \cdot 2 = 4^{n} \cdot 4$
211	209 210	eqtrdi	$⊢ 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