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 2t3e6 ⊢ ( 2 · 3 ) = 6
43 42 oveq2i ⊢ ( 2 ↑ ( 2 · 3 ) ) = ( 2 ↑ 6 )
44 2exp6 ⊢ ( 2 ↑ 6 ) = 6 4
45 43 44 eqtri ⊢ ( 2 ↑ ( 2 · 3 ) ) = 6 4
46 4cn ⊢ 4 ∈ ℂ
47 4ne0 ⊢ 4 ≠ 0
48 4z ⊢ 4 ∈ ℤ
49 expm1 ⊢ ( ( 4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ ) → ( 4 ↑ ( 4 − 1 ) ) = ( ( 4 ↑ 4 ) / 4 ) )
50 46 47 48 49 mp3an ⊢ ( 4 ↑ ( 4 − 1 ) ) = ( ( 4 ↑ 4 ) / 4 )
51 41 45 50 3eqtr3ri ⊢ ( ( 4 ↑ 4 ) / 4 ) = 6 4
52 df-4 ⊢ 4 = ( 3 + 1 )
53 52 oveq2i ⊢ ( 2 · 4 ) = ( 2 · ( 3 + 1 ) )
54 53 52 oveq12i ⊢ ( ( 2 · 4 ) C 4 ) = ( ( 2 · ( 3 + 1 ) ) C ( 3 + 1 ) )
55 bcp1ctr ⊢ ( 3 ∈ ℕ0 → ( ( 2 · ( 3 + 1 ) ) C ( 3 + 1 ) ) = ( ( ( 2 · 3 ) C 3 ) · ( 2 · ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) ) ) )
56 34 55 ax-mp ⊢ ( ( 2 · ( 3 + 1 ) ) C ( 3 + 1 ) ) = ( ( ( 2 · 3 ) C 3 ) · ( 2 · ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) ) )
57 df-3 ⊢ 3 = ( 2 + 1 )
58 57 oveq2i ⊢ ( 2 · 3 ) = ( 2 · ( 2 + 1 ) )
59 58 57 oveq12i ⊢ ( ( 2 · 3 ) C 3 ) = ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) )
60 bcp1ctr ⊢ ( 2 ∈ ℕ0 → ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) = ( ( ( 2 · 2 ) C 2 ) · ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) ) )
61 33 60 ax-mp ⊢ ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) = ( ( ( 2 · 2 ) C 2 ) · ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) )
62 df-2 ⊢ 2 = ( 1 + 1 )
63 62 oveq2i ⊢ ( 2 · 2 ) = ( 2 · ( 1 + 1 ) )
64 63 62 oveq12i ⊢ ( ( 2 · 2 ) C 2 ) = ( ( 2 · ( 1 + 1 ) ) C ( 1 + 1 ) )
65 1nn0 ⊢ 1 ∈ ℕ0
66 bcp1ctr ⊢ ( 1 ∈ ℕ0 → ( ( 2 · ( 1 + 1 ) ) C ( 1 + 1 ) ) = ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) )
67 65 66 ax-mp ⊢ ( ( 2 · ( 1 + 1 ) ) C ( 1 + 1 ) ) = ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) )
68 1e0p1 ⊢ 1 = ( 0 + 1 )
69 68 oveq2i ⊢ ( 2 · 1 ) = ( 2 · ( 0 + 1 ) )
70 69 68 oveq12i ⊢ ( ( 2 · 1 ) C 1 ) = ( ( 2 · ( 0 + 1 ) ) C ( 0 + 1 ) )
71 bcp1ctr ⊢ ( 0 ∈ ℕ0 → ( ( 2 · ( 0 + 1 ) ) C ( 0 + 1 ) ) = ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) )
72 28 71 ax-mp ⊢ ( ( 2 · ( 0 + 1 ) ) C ( 0 + 1 ) ) = ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) )
73 33 28 nn0mulcli ⊢ ( 2 · 0 ) ∈ ℕ0
74 bcn0 ⊢ ( ( 2 · 0 ) ∈ ℕ0 → ( ( 2 · 0 ) C 0 ) = 1 )
75 73 74 ax-mp ⊢ ( ( 2 · 0 ) C 0 ) = 1
76 2t0e0 ⊢ ( 2 · 0 ) = 0
77 76 oveq1i ⊢ ( ( 2 · 0 ) + 1 ) = ( 0 + 1 )
78 77 68 eqtr4i ⊢ ( ( 2 · 0 ) + 1 ) = 1
79 68 eqcomi ⊢ ( 0 + 1 ) = 1
80 78 79 oveq12i ⊢ ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) = ( 1 / 1 )
81 1div1e1 ⊢ ( 1 / 1 ) = 1
82 80 81 eqtri ⊢ ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) = 1
83 82 oveq2i ⊢ ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) = ( 2 · 1 )
84 2t1e2 ⊢ ( 2 · 1 ) = 2
85 83 84 eqtri ⊢ ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) = 2
86 75 85 oveq12i ⊢ ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = ( 1 · 2 )
87 32 mullidi ⊢ ( 1 · 2 ) = 2
88 86 87 eqtri ⊢ ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = 2
89 70 72 88 3eqtri ⊢ ( ( 2 · 1 ) C 1 ) = 2
90 84 oveq1i ⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
91 90 57 eqtr4i ⊢ ( ( 2 · 1 ) + 1 ) = 3
92 62 eqcomi ⊢ ( 1 + 1 ) = 2
93 91 92 oveq12i ⊢ ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) = ( 3 / 2 )
94 93 oveq2i ⊢ ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) = ( 2 · ( 3 / 2 ) )
95 3cn ⊢ 3 ∈ ℂ
96 2ne0 ⊢ 2 ≠ 0
97 95 32 96 divcan2i ⊢ ( 2 · ( 3 / 2 ) ) = 3
98 94 97 eqtri ⊢ ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) = 3
99 89 98 oveq12i ⊢ ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) = ( 2 · 3 )
100 99 42 eqtri ⊢ ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) = 6
101 64 67 100 3eqtri ⊢ ( ( 2 · 2 ) C 2 ) = 6
102 2t2e4 ⊢ ( 2 · 2 ) = 4
103 102 oveq1i ⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 )
104 df-5 ⊢ 5 = ( 4 + 1 )
105 103 104 eqtr4i ⊢ ( ( 2 · 2 ) + 1 ) = 5
106 57 eqcomi ⊢ ( 2 + 1 ) = 3
107 105 106 oveq12i ⊢ ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) = ( 5 / 3 )
108 107 oveq2i ⊢ ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( 2 · ( 5 / 3 ) )
109 5cn ⊢ 5 ∈ ℂ
110 3ne0 ⊢ 3 ≠ 0
111 32 109 95 110 divassi ⊢ ( ( 2 · 5 ) / 3 ) = ( 2 · ( 5 / 3 ) )
112 108 111 eqtr4i ⊢ ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( ( 2 · 5 ) / 3 )
113 101 112 oveq12i ⊢ ( ( ( 2 · 2 ) C 2 ) · ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) ) = ( 6 · ( ( 2 · 5 ) / 3 ) )
114 61 113 eqtri ⊢ ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) = ( 6 · ( ( 2 · 5 ) / 3 ) )
115 6cn ⊢ 6 ∈ ℂ
116 2nn ⊢ 2 ∈ ℕ
117 5nn ⊢ 5 ∈ ℕ
118 116 117 nnmulcli ⊢ ( 2 · 5 ) ∈ ℕ
119 118 nncni ⊢ ( 2 · 5 ) ∈ ℂ
120 95 110 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
121 div12 ⊢ ( ( 6 ∈ ℂ ∧ ( 2 · 5 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( 6 · ( ( 2 · 5 ) / 3 ) ) = ( ( 2 · 5 ) · ( 6 / 3 ) ) )
122 115 119 120 121 mp3an ⊢ ( 6 · ( ( 2 · 5 ) / 3 ) ) = ( ( 2 · 5 ) · ( 6 / 3 ) )
123 5t2e10 ⊢ ( 5 · 2 ) = 1 0
124 109 32 123 mulcomli ⊢ ( 2 · 5 ) = 1 0
125 3t2e6 ⊢ ( 3 · 2 ) = 6
126 115 95 32 110 divmuli ⊢ ( ( 6 / 3 ) = 2 ↔ ( 3 · 2 ) = 6 )
127 125 126 mpbir ⊢ ( 6 / 3 ) = 2
128 124 127 oveq12i ⊢ ( ( 2 · 5 ) · ( 6 / 3 ) ) = ( 1 0 · 2 )
129 122 128 eqtri ⊢ ( 6 · ( ( 2 · 5 ) / 3 ) ) = ( 1 0 · 2 )
130 59 114 129 3eqtri ⊢ ( ( 2 · 3 ) C 3 ) = ( 1 0 · 2 )
131 42 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 54 56 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 46 47 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 102 oveq1i ⊢ ( ( 2 · 2 ) · ( 7 / 4 ) ) = ( 4 · ( 7 / 4 ) )
146 32 32 142 mulassi ⊢ ( ( 2 · 2 ) · ( 7 / 4 ) ) = ( 2 · ( 2 · ( 7 / 4 ) ) )
147 141 46 47 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 51 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 116 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 116 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 46 157 206 sylancr ⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ ( 𝑛 + 1 ) ) = ( ( 4 ↑ 𝑛 ) · 4 ) )
208 159 nncnd ⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℂ )
209 208 200 200 mulassd ⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) · 2 ) · 2 ) = ( ( 4 ↑ 𝑛 ) · ( 2 · 2 ) ) )
210 102 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 𝑁 ) )