# Metamath Proof Explorer

## Theorem bclbnd

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

Ref Expression
Assertion bclbnd ${⊢}{N}\in {ℤ}_{\ge 4}\to \frac{{4}^{{N}}}{{N}}<\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)$

### 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 \left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)=\left(\genfrac{}{}{0}{}{2\cdot 4}{4}\right)$
6 3 5 breq12d ${⊢}{x}=4\to \left(\frac{{4}^{{x}}}{{x}}<\left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)↔\frac{{4}^{4}}{4}<\left(\genfrac{}{}{0}{}{2\cdot 4}{4}\right)\right)$
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 \left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)=\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)$
12 9 11 breq12d ${⊢}{x}={n}\to \left(\frac{{4}^{{x}}}{{x}}<\left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)↔\frac{{4}^{{n}}}{{n}}<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)\right)$
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\left({n}+1\right)$
17 16 14 oveq12d ${⊢}{x}={n}+1\to \left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)=\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)$
18 15 17 breq12d ${⊢}{x}={n}+1\to \left(\frac{{4}^{{x}}}{{x}}<\left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)↔\frac{{4}^{{n}+1}}{{n}+1}<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
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 \left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)=\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)$
24 21 23 breq12d ${⊢}{x}={N}\to \left(\frac{{4}^{{x}}}{{x}}<\left(\genfrac{}{}{0}{}{2{x}}{{x}}\right)↔\frac{{4}^{{N}}}{{N}}<\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\right)$
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 ${⊢}\left(2\in ℂ\wedge 2\in {ℕ}_{0}\wedge 3\in {ℕ}_{0}\right)\to {2}^{2\cdot 3}={\left({2}^{2}\right)}^{3}$
36 32 33 34 35 mp3an ${⊢}{2}^{2\cdot 3}={\left({2}^{2}\right)}^{3}$
37 sq2 ${⊢}{2}^{2}=4$
38 37 eqcomi ${⊢}4={2}^{2}$
39 4m1e3 ${⊢}4-1=3$
40 38 39 oveq12i ${⊢}{4}^{4-1}={\left({2}^{2}\right)}^{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\ne 0$
50 4z ${⊢}4\in ℤ$
51 expm1 ${⊢}\left(4\in ℂ\wedge 4\ne 0\wedge 4\in ℤ\right)\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\left(3+1\right)$
56 55 54 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 4}{4}\right)=\left(\genfrac{}{}{0}{}{2\left(3+1\right)}{3+1}\right)$
57 bcp1ctr ${⊢}3\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{2\left(3+1\right)}{3+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 3}{3}\right)2\left(\frac{2\cdot 3+1}{3+1}\right)$
58 34 57 ax-mp ${⊢}\left(\genfrac{}{}{0}{}{2\left(3+1\right)}{3+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 3}{3}\right)2\left(\frac{2\cdot 3+1}{3+1}\right)$
59 df-3 ${⊢}3=2+1$
60 59 oveq2i ${⊢}2\cdot 3=2\left(2+1\right)$
61 60 59 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 3}{3}\right)=\left(\genfrac{}{}{0}{}{2\left(2+1\right)}{2+1}\right)$
62 bcp1ctr ${⊢}2\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{2\left(2+1\right)}{2+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 2}{2}\right)2\left(\frac{2\cdot 2+1}{2+1}\right)$
63 33 62 ax-mp ${⊢}\left(\genfrac{}{}{0}{}{2\left(2+1\right)}{2+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 2}{2}\right)2\left(\frac{2\cdot 2+1}{2+1}\right)$
64 df-2 ${⊢}2=1+1$
65 64 oveq2i ${⊢}2\cdot 2=2\left(1+1\right)$
66 65 64 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 2}{2}\right)=\left(\genfrac{}{}{0}{}{2\left(1+1\right)}{1+1}\right)$
67 1nn0 ${⊢}1\in {ℕ}_{0}$
68 bcp1ctr ${⊢}1\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{2\left(1+1\right)}{1+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 1}{1}\right)2\left(\frac{2\cdot 1+1}{1+1}\right)$
69 67 68 ax-mp ${⊢}\left(\genfrac{}{}{0}{}{2\left(1+1\right)}{1+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 1}{1}\right)2\left(\frac{2\cdot 1+1}{1+1}\right)$
70 1e0p1 ${⊢}1=0+1$
71 70 oveq2i ${⊢}2\cdot 1=2\left(0+1\right)$
72 71 70 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 1}{1}\right)=\left(\genfrac{}{}{0}{}{2\left(0+1\right)}{0+1}\right)$
73 bcp1ctr ${⊢}0\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{2\left(0+1\right)}{0+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 0}{0}\right)2\left(\frac{2\cdot 0+1}{0+1}\right)$
74 28 73 ax-mp ${⊢}\left(\genfrac{}{}{0}{}{2\left(0+1\right)}{0+1}\right)=\left(\genfrac{}{}{0}{}{2\cdot 0}{0}\right)2\left(\frac{2\cdot 0+1}{0+1}\right)$
75 33 28 nn0mulcli ${⊢}2\cdot 0\in {ℕ}_{0}$
76 bcn0 ${⊢}2\cdot 0\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{2\cdot 0}{0}\right)=1$
77 75 76 ax-mp ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 0}{0}\right)=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\left(\frac{2\cdot 0+1}{0+1}\right)=2\cdot 1$
86 2t1e2 ${⊢}2\cdot 1=2$
87 85 86 eqtri ${⊢}2\left(\frac{2\cdot 0+1}{0+1}\right)=2$
88 77 87 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 0}{0}\right)2\left(\frac{2\cdot 0+1}{0+1}\right)=1\cdot 2$
89 32 mulid2i ${⊢}1\cdot 2=2$
90 88 89 eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 0}{0}\right)2\left(\frac{2\cdot 0+1}{0+1}\right)=2$
91 72 74 90 3eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 1}{1}\right)=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\left(\frac{2\cdot 1+1}{1+1}\right)=2\left(\frac{3}{2}\right)$
97 2ne0 ${⊢}2\ne 0$
98 42 32 97 divcan2i ${⊢}2\left(\frac{3}{2}\right)=3$
99 96 98 eqtri ${⊢}2\left(\frac{2\cdot 1+1}{1+1}\right)=3$
100 91 99 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 1}{1}\right)2\left(\frac{2\cdot 1+1}{1+1}\right)=2\cdot 3$
101 100 44 eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 1}{1}\right)2\left(\frac{2\cdot 1+1}{1+1}\right)=6$
102 66 69 101 3eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 2}{2}\right)=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\left(\frac{2\cdot 2+1}{2+1}\right)=2\left(\frac{5}{3}\right)$
110 5cn ${⊢}5\in ℂ$
111 3ne0 ${⊢}3\ne 0$
112 32 110 42 111 divassi ${⊢}\frac{2\cdot 5}{3}=2\left(\frac{5}{3}\right)$
113 109 112 eqtr4i ${⊢}2\left(\frac{2\cdot 2+1}{2+1}\right)=\frac{2\cdot 5}{3}$
114 102 113 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 2}{2}\right)2\left(\frac{2\cdot 2+1}{2+1}\right)=6\left(\frac{2\cdot 5}{3}\right)$
115 63 114 eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\left(2+1\right)}{2+1}\right)=6\left(\frac{2\cdot 5}{3}\right)$
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 ${⊢}\left(3\in ℂ\wedge 3\ne 0\right)$
122 div12 ${⊢}\left(6\in ℂ\wedge 2\cdot 5\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to 6\left(\frac{2\cdot 5}{3}\right)=2\cdot 5\left(\frac{6}{3}\right)$
123 116 120 121 122 mp3an ${⊢}6\left(\frac{2\cdot 5}{3}\right)=2\cdot 5\left(\frac{6}{3}\right)$
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↔3\cdot 2=6$
127 43 126 mpbir ${⊢}\frac{6}{3}=2$
128 125 127 oveq12i ${⊢}2\cdot 5\left(\frac{6}{3}\right)=10\cdot 2$
129 123 128 eqtri ${⊢}6\left(\frac{2\cdot 5}{3}\right)=10\cdot 2$
130 61 115 129 3eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 3}{3}\right)=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\left(\frac{2\cdot 3+1}{3+1}\right)=2\left(\frac{7}{4}\right)$
137 130 136 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 3}{3}\right)2\left(\frac{2\cdot 3+1}{3+1}\right)=10\cdot 22\left(\frac{7}{4}\right)$
138 56 58 137 3eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 4}{4}\right)=10\cdot 22\left(\frac{7}{4}\right)$
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\left(\frac{7}{4}\right)\in ℂ$
144 140 32 143 mulassi ${⊢}10\cdot 22\left(\frac{7}{4}\right)=1022\left(\frac{7}{4}\right)$
145 103 oveq1i ${⊢}2\cdot 2\left(\frac{7}{4}\right)=4\left(\frac{7}{4}\right)$
146 32 32 142 mulassi ${⊢}2\cdot 2\left(\frac{7}{4}\right)=22\left(\frac{7}{4}\right)$
147 141 48 49 divcan2i ${⊢}4\left(\frac{7}{4}\right)=7$
148 145 146 147 3eqtr3i ${⊢}22\left(\frac{7}{4}\right)=7$
149 148 oveq2i ${⊢}1022\left(\frac{7}{4}\right)=10\cdot 7$
150 144 149 eqtri ${⊢}10\cdot 22\left(\frac{7}{4}\right)=10\cdot 7$
151 26 dec0u ${⊢}10\cdot 7=70$
152 138 150 151 3eqtri ${⊢}\left(\genfrac{}{}{0}{}{2\cdot 4}{4}\right)=70$
153 31 53 152 3brtr4i ${⊢}\frac{{4}^{4}}{4}<\left(\genfrac{}{}{0}{}{2\cdot 4}{4}\right)$
154 4nn ${⊢}4\in ℕ$
155 eluznn ${⊢}\left(4\in ℕ\wedge {n}\in {ℤ}_{\ge 4}\right)\to {n}\in ℕ$
156 154 155 mpan ${⊢}{n}\in {ℤ}_{\ge 4}\to {n}\in ℕ$
157 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
158 nnexpcl ${⊢}\left(4\in ℕ\wedge {n}\in {ℕ}_{0}\right)\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 ${⊢}\left(2\in ℕ\wedge {n}\in ℕ\right)\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 ${⊢}\left(2{n}\in {ℕ}_{0}\wedge {n}\in ℤ\right)\to \left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)\in {ℕ}_{0}$
169 166 167 168 syl2anc ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)\in {ℕ}_{0}$
170 169 nn0red ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)\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 ${⊢}\left(2\in {ℝ}^{+}\wedge \frac{2{n}+1}{{n}+1}\in {ℝ}^{+}\right)\to 2\left(\frac{2{n}+1}{{n}+1}\right)\in {ℝ}^{+}$
178 171 176 177 sylancr ${⊢}{n}\in ℕ\to 2\left(\frac{2{n}+1}{{n}+1}\right)\in {ℝ}^{+}$
179 163 170 178 ltmul1d ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}}{{n}}<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)↔\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)\right)$
180 bcp1ctr ${⊢}{n}\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)=\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)$
181 157 180 syl ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)=\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)$
182 181 breq2d ${⊢}{n}\in ℕ\to \left(\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)↔\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)\right)$
183 179 182 bitr4d ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}}{{n}}<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)↔\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
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 ${⊢}\left({4}^{{n}}\in ℕ\wedge 2\in ℕ\right)\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 ${⊢}\left(2\in ℝ\wedge \frac{1}{{n}}\in {ℝ}^{+}\right)\to 2<2+\left(\frac{1}{{n}}\right)$
194 184 192 193 sylancr ${⊢}{n}\in ℕ\to 2<2+\left(\frac{1}{{n}}\right)$
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}\ne 0$
199 195 196 197 198 divdird ${⊢}{n}\in ℕ\to \frac{2{n}+1}{{n}}=\left(\frac{2{n}}{{n}}\right)+\left(\frac{1}{{n}}\right)$
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 \left(\frac{2{n}}{{n}}\right)+\left(\frac{1}{{n}}\right)=2+\left(\frac{1}{{n}}\right)$
203 199 202 eqtr2d ${⊢}{n}\in ℕ\to 2+\left(\frac{1}{{n}}\right)=\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 \left(\frac{{4}^{{n}}\cdot 2}{{n}+1}\right)\cdot 2<\left(\frac{{4}^{{n}}\cdot 2}{{n}+1}\right)\left(\frac{2{n}+1}{{n}}\right)$
206 expp1 ${⊢}\left(4\in ℂ\wedge {n}\in {ℕ}_{0}\right)\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\ne 0$
217 214 200 215 216 div23d ${⊢}{n}\in ℕ\to \frac{{4}^{{n}}\cdot 2\cdot 2}{{n}+1}=\left(\frac{{4}^{{n}}\cdot 2}{{n}+1}\right)\cdot 2$
218 213 217 eqtrd ${⊢}{n}\in ℕ\to \frac{{4}^{{n}+1}}{{n}+1}=\left(\frac{{4}^{{n}}\cdot 2}{{n}+1}\right)\cdot 2$
219 208 200 197 198 div23d ${⊢}{n}\in ℕ\to \frac{{4}^{{n}}\cdot 2}{{n}}=\left(\frac{{4}^{{n}}}{{n}}\right)\cdot 2$
220 219 oveq1d ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}\cdot 2}{{n}}\right)\left(\frac{2{n}+1}{{n}+1}\right)=\left(\frac{{4}^{{n}}}{{n}}\right)\cdot 2\left(\frac{2{n}+1}{{n}+1}\right)$
221 172 nncnd ${⊢}{n}\in ℕ\to 2{n}+1\in ℂ$
222 214 197 221 215 198 216 divmul24d ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}\cdot 2}{{n}}\right)\left(\frac{2{n}+1}{{n}+1}\right)=\left(\frac{{4}^{{n}}\cdot 2}{{n}+1}\right)\left(\frac{2{n}+1}{{n}}\right)$
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 \left(\frac{{4}^{{n}}}{{n}}\right)\cdot 2\left(\frac{2{n}+1}{{n}+1}\right)=\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)$
226 220 222 225 3eqtr3rd ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)=\left(\frac{{4}^{{n}}\cdot 2}{{n}+1}\right)\left(\frac{2{n}+1}{{n}}\right)$
227 205 218 226 3brtr4d ${⊢}{n}\in ℕ\to \frac{{4}^{{n}+1}}{{n}+1}<\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)$
228 174 nnnn0d ${⊢}{n}\in ℕ\to {n}+1\in {ℕ}_{0}$
229 nnexpcl ${⊢}\left(4\in ℕ\wedge {n}+1\in {ℕ}_{0}\right)\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\left(\frac{2{n}+1}{{n}+1}\right)\in ℝ$
235 163 234 remulcld ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)\in ℝ$
236 nn0mulcl ${⊢}\left(2\in {ℕ}_{0}\wedge {n}+1\in {ℕ}_{0}\right)\to 2\left({n}+1\right)\in {ℕ}_{0}$
237 33 228 236 sylancr ${⊢}{n}\in ℕ\to 2\left({n}+1\right)\in {ℕ}_{0}$
238 174 nnzd ${⊢}{n}\in ℕ\to {n}+1\in ℤ$
239 bccl ${⊢}\left(2\left({n}+1\right)\in {ℕ}_{0}\wedge {n}+1\in ℤ\right)\to \left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\in {ℕ}_{0}$
240 237 238 239 syl2anc ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\in {ℕ}_{0}$
241 240 nn0red ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\in ℝ$
242 lttr ${⊢}\left(\frac{{4}^{{n}+1}}{{n}+1}\in ℝ\wedge \left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)\in ℝ\wedge \left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\in ℝ\right)\to \left(\left(\frac{{4}^{{n}+1}}{{n}+1}<\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)\wedge \left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)\to \frac{{4}^{{n}+1}}{{n}+1}<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
243 233 235 241 242 syl3anc ${⊢}{n}\in ℕ\to \left(\left(\frac{{4}^{{n}+1}}{{n}+1}<\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)\wedge \left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)\to \frac{{4}^{{n}+1}}{{n}+1}<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
244 227 243 mpand ${⊢}{n}\in ℕ\to \left(\left(\frac{{4}^{{n}}}{{n}}\right)2\left(\frac{2{n}+1}{{n}+1}\right)<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\to \frac{{4}^{{n}+1}}{{n}+1}<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
245 183 244 sylbid ${⊢}{n}\in ℕ\to \left(\frac{{4}^{{n}}}{{n}}<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)\to \frac{{4}^{{n}+1}}{{n}+1}<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
246 156 245 syl ${⊢}{n}\in {ℤ}_{\ge 4}\to \left(\frac{{4}^{{n}}}{{n}}<\left(\genfrac{}{}{0}{}{2{n}}{{n}}\right)\to \frac{{4}^{{n}+1}}{{n}+1}<\left(\genfrac{}{}{0}{}{2\left({n}+1\right)}{{n}+1}\right)\right)$
247 6 12 18 24 153 246 uzind4i ${⊢}{N}\in {ℤ}_{\ge 4}\to \frac{{4}^{{N}}}{{N}}<\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)$