Metamath Proof Explorer


Theorem bclbnd

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

Ref Expression
Assertion bclbnd ( 𝑁 ∈ ( ℤ ‘ 4 ) → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) )

Proof

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