Metamath Proof Explorer

Theorem bclbnd

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

Ref Expression
Assertion bclbnd 
|- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )

Proof

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