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 𝑁 ) )