Metamath Proof Explorer

Theorem log2ublem3

Description: Lemma for log2ub . In decimal, this is a proof that the first four terms of the series for log 2 is less than 5 3 0 5 6 / 7 6 5 4 5 . (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Assertion log2ublem3 ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ 5 3 0 5 6

Proof

Step Hyp Ref Expression
1 0le0 ⊢ 0 ≤ 0
2 risefall0lem ⊢ ( 0 ... ( 0 − 1 ) ) = ∅
3 2 sumeq1i ⊢ Σ 𝑛 ∈ ( 0 ... ( 0 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = Σ 𝑛 ∈ ∅ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
4 sum0 ⊢ Σ 𝑛 ∈ ∅ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = 0
5 3 4 eqtri ⊢ Σ 𝑛 ∈ ( 0 ... ( 0 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = 0
6 5 oveq2i ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... ( 0 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) = ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 0 )
7 3cn ⊢ 3 ∈ ℂ
8 7nn0 ⊢ 7 ∈ ℕ0
9 expcl ⊢ ( ( 3 ∈ ℂ ∧ 7 ∈ ℕ0 ) → ( 3 ↑ 7 ) ∈ ℂ )
10 7 8 9 mp2an ⊢ ( 3 ↑ 7 ) ∈ ℂ
11 5cn ⊢ 5 ∈ ℂ
12 7cn ⊢ 7 ∈ ℂ
13 11 12 mulcli ⊢ ( 5 · 7 ) ∈ ℂ
14 10 13 mulcli ⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℂ
15 14 mul01i ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 0 ) = 0
16 6 15 eqtri ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... ( 0 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) = 0
17 2cn ⊢ 2 ∈ ℂ
18 17 mul01i ⊢ ( 2 · 0 ) = 0
19 1 16 18 3brtr4i ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... ( 0 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 0 )
20 0nn0 ⊢ 0 ∈ ℕ0
21 2nn0 ⊢ 2 ∈ ℕ0
22 5nn0 ⊢ 5 ∈ ℕ0
23 21 22 deccl ⊢ 2 5 ∈ ℕ0
24 23 22 deccl ⊢ 2 5 5 ∈ ℕ0
25 1nn0 ⊢ 1 ∈ ℕ0
26 24 25 deccl ⊢ 2 5 5 1 ∈ ℕ0
27 26 22 deccl ⊢ 2 5 5 1 5 ∈ ℕ0
28 eqid ⊢ ( 0 − 1 ) = ( 0 − 1 )
29 27 nn0cni ⊢ 2 5 5 1 5 ∈ ℂ
30 29 addid2i ⊢ ( 0 + 2 5 5 1 5 ) = 2 5 5 1 5
31 3nn0 ⊢ 3 ∈ ℕ0
32 7 addid1i ⊢ ( 3 + 0 ) = 3
33 29 mulid2i ⊢ ( 1 · 2 5 5 1 5 ) = 2 5 5 1 5
34 18 oveq1i ⊢ ( ( 2 · 0 ) + 1 ) = ( 0 + 1 )
35 0p1e1 ⊢ ( 0 + 1 ) = 1
36 34 35 eqtri ⊢ ( ( 2 · 0 ) + 1 ) = 1
37 36 oveq1i ⊢ ( ( ( 2 · 0 ) + 1 ) · 2 5 5 1 5 ) = ( 1 · 2 5 5 1 5 )
38 22 8 nn0mulcli ⊢ ( 5 · 7 ) ∈ ℕ0
39 8 21 deccl ⊢ 7 2 ∈ ℕ0
40 9nn0 ⊢ 9 ∈ ℕ0
41 2p1e3 ⊢ ( 2 + 1 ) = 3
42 8nn0 ⊢ 8 ∈ ℕ0
43 1p1e2 ⊢ ( 1 + 1 ) = 2
44 9cn ⊢ 9 ∈ ℂ
45 exp1 ⊢ ( 9 ∈ ℂ → ( 9 ↑ 1 ) = 9 )
46 44 45 ax-mp ⊢ ( 9 ↑ 1 ) = 9
47 46 oveq1i ⊢ ( ( 9 ↑ 1 ) · 9 ) = ( 9 · 9 )
48 9t9e81 ⊢ ( 9 · 9 ) = 8 1
49 47 48 eqtri ⊢ ( ( 9 ↑ 1 ) · 9 ) = 8 1
50 40 25 43 49 numexpp1 ⊢ ( 9 ↑ 2 ) = 8 1
51 8cn ⊢ 8 ∈ ℂ
52 9t8e72 ⊢ ( 9 · 8 ) = 7 2
53 44 51 52 mulcomli ⊢ ( 8 · 9 ) = 7 2
54 44 mulid2i ⊢ ( 1 · 9 ) = 9
55 40 42 25 50 53 54 decmul1 ⊢ ( ( 9 ↑ 2 ) · 9 ) = 7 2 9
56 40 21 41 55 numexpp1 ⊢ ( 9 ↑ 3 ) = 7 2 9
57 31 25 deccl ⊢ 3 1 ∈ ℕ0
58 eqid ⊢ 7 2 = 7 2
59 eqid ⊢ 3 1 = 3 1
60 7t5e35 ⊢ ( 7 · 5 ) = 3 5
61 12 11 60 mulcomli ⊢ ( 5 · 7 ) = 3 5
62 7p3e10 ⊢ ( 7 + 3 ) = 1 0
63 12 7 62 addcomli ⊢ ( 3 + 7 ) = 1 0
64 ax-1cn ⊢ 1 ∈ ℂ
65 3p1e4 ⊢ ( 3 + 1 ) = 4
66 7 64 65 addcomli ⊢ ( 1 + 3 ) = 4
67 66 oveq2i ⊢ ( ( 3 · 7 ) + ( 1 + 3 ) ) = ( ( 3 · 7 ) + 4 )
68 4nn0 ⊢ 4 ∈ ℕ0
69 7t3e21 ⊢ ( 7 · 3 ) = 2 1
70 12 7 69 mulcomli ⊢ ( 3 · 7 ) = 2 1
71 4cn ⊢ 4 ∈ ℂ
72 4p1e5 ⊢ ( 4 + 1 ) = 5
73 71 64 72 addcomli ⊢ ( 1 + 4 ) = 5
74 21 25 68 70 73 decaddi ⊢ ( ( 3 · 7 ) + 4 ) = 2 5
75 67 74 eqtri ⊢ ( ( 3 · 7 ) + ( 1 + 3 ) ) = 2 5
76 61 oveq1i ⊢ ( ( 5 · 7 ) + 0 ) = ( 3 5 + 0 )
77 31 22 deccl ⊢ 3 5 ∈ ℕ0
78 77 nn0cni ⊢ 3 5 ∈ ℂ
79 78 addid1i ⊢ ( 3 5 + 0 ) = 3 5
80 76 79 eqtri ⊢ ( ( 5 · 7 ) + 0 ) = 3 5
81 31 22 25 20 61 63 8 22 31 75 80 decmac ⊢ ( ( ( 5 · 7 ) · 7 ) + ( 3 + 7 ) ) = 2 5 5
82 25 dec0h ⊢ 1 = 0 1
83 3t2e6 ⊢ ( 3 · 2 ) = 6
84 83 35 oveq12i ⊢ ( ( 3 · 2 ) + ( 0 + 1 ) ) = ( 6 + 1 )
85 6p1e7 ⊢ ( 6 + 1 ) = 7
86 84 85 eqtri ⊢ ( ( 3 · 2 ) + ( 0 + 1 ) ) = 7
87 5t2e10 ⊢ ( 5 · 2 ) = 1 0
88 25 20 35 87 decsuc ⊢ ( ( 5 · 2 ) + 1 ) = 1 1
89 31 22 20 25 61 82 21 25 25 86 88 decmac ⊢ ( ( ( 5 · 7 ) · 2 ) + 1 ) = 7 1
90 8 21 31 25 58 59 38 25 8 81 89 decma2c ⊢ ( ( ( 5 · 7 ) · 7 2 ) + 3 1 ) = 2 5 5 1
91 9t3e27 ⊢ ( 9 · 3 ) = 2 7
92 44 7 91 mulcomli ⊢ ( 3 · 9 ) = 2 7
93 7p4e11 ⊢ ( 7 + 4 ) = 1 1
94 21 8 68 92 41 25 93 decaddci ⊢ ( ( 3 · 9 ) + 4 ) = 3 1
95 9t5e45 ⊢ ( 9 · 5 ) = 4 5
96 44 11 95 mulcomli ⊢ ( 5 · 9 ) = 4 5
97 40 31 22 61 22 68 94 96 decmul1c ⊢ ( ( 5 · 7 ) · 9 ) = 3 1 5
98 38 39 40 56 22 57 90 97 decmul2c ⊢ ( ( 5 · 7 ) · ( 9 ↑ 3 ) ) = 2 5 5 1 5
99 33 37 98 3eqtr4ri ⊢ ( ( 5 · 7 ) · ( 9 ↑ 3 ) ) = ( ( ( 2 · 0 ) + 1 ) · 2 5 5 1 5 )
100 19 20 27 20 28 30 31 32 99 log2ublem2 ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 0 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 2 5 5 1 5 )
101 40 68 deccl ⊢ 9 4 ∈ ℕ0
102 101 22 deccl ⊢ 9 4 5 ∈ ℕ0
103 1m1e0 ⊢ ( 1 − 1 ) = 0
104 eqid ⊢ 2 5 5 1 5 = 2 5 5 1 5
105 eqid ⊢ 9 4 5 = 9 4 5
106 6nn0 ⊢ 6 ∈ ℕ0
107 21 106 deccl ⊢ 2 6 ∈ ℕ0
108 107 68 deccl ⊢ 2 6 4 ∈ ℕ0
109 5p1e6 ⊢ ( 5 + 1 ) = 6
110 eqid ⊢ 2 5 5 1 = 2 5 5 1
111 eqid ⊢ 9 4 = 9 4
112 eqid ⊢ 2 5 5 = 2 5 5
113 eqid ⊢ 2 5 = 2 5
114 21 22 109 113 decsuc ⊢ ( 2 5 + 1 ) = 2 6
115 9p5e14 ⊢ ( 9 + 5 ) = 1 4
116 44 11 115 addcomli ⊢ ( 5 + 9 ) = 1 4
117 23 22 40 112 114 68 116 decaddci ⊢ ( 2 5 5 + 9 ) = 2 6 4
118 24 25 40 68 110 111 117 73 decadd ⊢ ( 2 5 5 1 + 9 4 ) = 2 6 4 5
119 108 22 109 118 decsuc ⊢ ( ( 2 5 5 1 + 9 4 ) + 1 ) = 2 6 4 6
120 5p5e10 ⊢ ( 5 + 5 ) = 1 0
121 26 22 101 22 104 105 119 120 decaddc2 ⊢ ( 2 5 5 1 5 + 9 4 5 ) = 2 6 4 6 0
122 44 sqvali ⊢ ( 9 ↑ 2 ) = ( 9 · 9 )
123 3t3e9 ⊢ ( 3 · 3 ) = 9
124 123 oveq1i ⊢ ( ( 3 · 3 ) · 9 ) = ( 9 · 9 )
125 7 7 44 mulassi ⊢ ( ( 3 · 3 ) · 9 ) = ( 3 · ( 3 · 9 ) )
126 122 124 125 3eqtr2i ⊢ ( 9 ↑ 2 ) = ( 3 · ( 3 · 9 ) )
127 126 oveq2i ⊢ ( ( 5 · 7 ) · ( 9 ↑ 2 ) ) = ( ( 5 · 7 ) · ( 3 · ( 3 · 9 ) ) )
128 7 44 mulcli ⊢ ( 3 · 9 ) ∈ ℂ
129 13 7 128 mul12i ⊢ ( ( 5 · 7 ) · ( 3 · ( 3 · 9 ) ) ) = ( 3 · ( ( 5 · 7 ) · ( 3 · 9 ) ) )
130 21 68 deccl ⊢ 2 4 ∈ ℕ0
131 eqid ⊢ 2 4 = 2 4
132 83 41 oveq12i ⊢ ( ( 3 · 2 ) + ( 2 + 1 ) ) = ( 6 + 3 )
133 6p3e9 ⊢ ( 6 + 3 ) = 9
134 132 133 eqtri ⊢ ( ( 3 · 2 ) + ( 2 + 1 ) ) = 9
135 71 addid2i ⊢ ( 0 + 4 ) = 4
136 25 20 68 87 135 decaddi ⊢ ( ( 5 · 2 ) + 4 ) = 1 4
137 31 22 21 68 61 131 21 68 25 134 136 decmac ⊢ ( ( ( 5 · 7 ) · 2 ) + 2 4 ) = 9 4
138 21 25 31 70 66 decaddi ⊢ ( ( 3 · 7 ) + 3 ) = 2 4
139 8 31 22 61 22 31 138 61 decmul1c ⊢ ( ( 5 · 7 ) · 7 ) = 2 4 5
140 38 21 8 92 22 130 137 139 decmul2c ⊢ ( ( 5 · 7 ) · ( 3 · 9 ) ) = 9 4 5
141 140 oveq2i ⊢ ( 3 · ( ( 5 · 7 ) · ( 3 · 9 ) ) ) = ( 3 · 9 4 5 )
142 129 141 eqtri ⊢ ( ( 5 · 7 ) · ( 3 · ( 3 · 9 ) ) ) = ( 3 · 9 4 5 )
143 df-3 ⊢ 3 = ( 2 + 1 )
144 17 mulid1i ⊢ ( 2 · 1 ) = 2
145 144 oveq1i ⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
146 143 145 eqtr4i ⊢ 3 = ( ( 2 · 1 ) + 1 )
147 146 oveq1i ⊢ ( 3 · 9 4 5 ) = ( ( ( 2 · 1 ) + 1 ) · 9 4 5 )
148 127 142 147 3eqtri ⊢ ( ( 5 · 7 ) · ( 9 ↑ 2 ) ) = ( ( ( 2 · 1 ) + 1 ) · 9 4 5 )
149 100 27 102 25 103 121 21 41 148 log2ublem2 ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 1 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 2 6 4 6 0 )
150 108 106 deccl ⊢ 2 6 4 6 ∈ ℕ0
151 150 20 deccl ⊢ 2 6 4 6 0 ∈ ℕ0
152 106 31 deccl ⊢ 6 3 ∈ ℕ0
153 2m1e1 ⊢ ( 2 − 1 ) = 1
154 eqid ⊢ 2 6 4 6 0 = 2 6 4 6 0
155 eqid ⊢ 6 3 = 6 3
156 eqid ⊢ 2 6 4 6 = 2 6 4 6
157 eqid ⊢ 2 6 4 = 2 6 4
158 107 68 72 157 decsuc ⊢ ( 2 6 4 + 1 ) = 2 6 5
159 6p6e12 ⊢ ( 6 + 6 ) = 1 2
160 108 106 106 156 158 21 159 decaddci ⊢ ( 2 6 4 6 + 6 ) = 2 6 5 2
161 7 addid2i ⊢ ( 0 + 3 ) = 3
162 150 20 106 31 154 155 160 161 decadd ⊢ ( 2 6 4 6 0 + 6 3 ) = 2 6 5 2 3
163 1p2e3 ⊢ ( 1 + 2 ) = 3
164 46 oveq2i ⊢ ( ( 5 · 7 ) · ( 9 ↑ 1 ) ) = ( ( 5 · 7 ) · 9 )
165 11 12 44 mulassi ⊢ ( ( 5 · 7 ) · 9 ) = ( 5 · ( 7 · 9 ) )
166 9t7e63 ⊢ ( 9 · 7 ) = 6 3
167 44 12 166 mulcomli ⊢ ( 7 · 9 ) = 6 3
168 167 oveq2i ⊢ ( 5 · ( 7 · 9 ) ) = ( 5 · 6 3 )
169 165 168 eqtri ⊢ ( ( 5 · 7 ) · 9 ) = ( 5 · 6 3 )
170 df-5 ⊢ 5 = ( 4 + 1 )
171 2t2e4 ⊢ ( 2 · 2 ) = 4
172 171 oveq1i ⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 )
173 170 172 eqtr4i ⊢ 5 = ( ( 2 · 2 ) + 1 )
174 173 oveq1i ⊢ ( 5 · 6 3 ) = ( ( ( 2 · 2 ) + 1 ) · 6 3 )
175 164 169 174 3eqtri ⊢ ( ( 5 · 7 ) · ( 9 ↑ 1 ) ) = ( ( ( 2 · 2 ) + 1 ) · 6 3 )
176 149 151 152 21 153 162 25 163 175 log2ublem2 ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 2 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 2 6 5 2 3 )
177 107 22 deccl ⊢ 2 6 5 ∈ ℕ0
178 177 21 deccl ⊢ 2 6 5 2 ∈ ℕ0
179 178 31 deccl ⊢ 2 6 5 2 3 ∈ ℕ0
180 3m1e2 ⊢ ( 3 − 1 ) = 2
181 eqid ⊢ 2 6 5 2 3 = 2 6 5 2 3
182 5p3e8 ⊢ ( 5 + 3 ) = 8
183 11 7 182 addcomli ⊢ ( 3 + 5 ) = 8
184 178 31 22 181 183 decaddi ⊢ ( 2 6 5 2 3 + 5 ) = 2 6 5 2 8
185 12 11 mulcli ⊢ ( 7 · 5 ) ∈ ℂ
186 185 mulid1i ⊢ ( ( 7 · 5 ) · 1 ) = ( 7 · 5 )
187 11 12 mulcomi ⊢ ( 5 · 7 ) = ( 7 · 5 )
188 exp0 ⊢ ( 9 ∈ ℂ → ( 9 ↑ 0 ) = 1 )
189 44 188 ax-mp ⊢ ( 9 ↑ 0 ) = 1
190 187 189 oveq12i ⊢ ( ( 5 · 7 ) · ( 9 ↑ 0 ) ) = ( ( 7 · 5 ) · 1 )
191 7 17 83 mulcomli ⊢ ( 2 · 3 ) = 6
192 191 oveq1i ⊢ ( ( 2 · 3 ) + 1 ) = ( 6 + 1 )
193 df-7 ⊢ 7 = ( 6 + 1 )
194 192 193 eqtr4i ⊢ ( ( 2 · 3 ) + 1 ) = 7
195 194 oveq1i ⊢ ( ( ( 2 · 3 ) + 1 ) · 5 ) = ( 7 · 5 )
196 186 190 195 3eqtr4i ⊢ ( ( 5 · 7 ) · ( 9 ↑ 0 ) ) = ( ( ( 2 · 3 ) + 1 ) · 5 )
197 176 179 22 31 180 184 20 161 196 log2ublem2 ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 2 6 5 2 8 )
198 eqid ⊢ 2 6 5 2 8 = 2 6 5 2 8
199 eqid ⊢ 2 6 5 2 = 2 6 5 2
200 eqid ⊢ 2 6 5 = 2 6 5
201 00id ⊢ ( 0 + 0 ) = 0
202 20 dec0h ⊢ 0 = 0 0
203 201 202 eqtri ⊢ ( 0 + 0 ) = 0 0
204 eqid ⊢ 2 6 = 2 6
205 35 82 eqtri ⊢ ( 0 + 1 ) = 0 1
206 171 35 oveq12i ⊢ ( ( 2 · 2 ) + ( 0 + 1 ) ) = ( 4 + 1 )
207 206 72 eqtri ⊢ ( ( 2 · 2 ) + ( 0 + 1 ) ) = 5
208 6cn ⊢ 6 ∈ ℂ
209 6t2e12 ⊢ ( 6 · 2 ) = 1 2
210 208 17 209 mulcomli ⊢ ( 2 · 6 ) = 1 2
211 25 21 41 210 decsuc ⊢ ( ( 2 · 6 ) + 1 ) = 1 3
212 21 106 20 25 204 205 21 31 25 207 211 decma2c ⊢ ( ( 2 · 2 6 ) + ( 0 + 1 ) ) = 5 3
213 11 17 87 mulcomli ⊢ ( 2 · 5 ) = 1 0
214 213 oveq1i ⊢ ( ( 2 · 5 ) + 0 ) = ( 1 0 + 0 )
215 dec10p ⊢ ( 1 0 + 0 ) = 1 0
216 214 215 eqtri ⊢ ( ( 2 · 5 ) + 0 ) = 1 0
217 107 22 20 20 200 203 21 20 25 212 216 decma2c ⊢ ( ( 2 · 2 6 5 ) + ( 0 + 0 ) ) = 5 3 0
218 22 dec0h ⊢ 5 = 0 5
219 172 72 218 3eqtri ⊢ ( ( 2 · 2 ) + 1 ) = 0 5
220 177 21 20 25 199 82 21 22 20 217 219 decma2c ⊢ ( ( 2 · 2 6 5 2 ) + 1 ) = 5 3 0 5
221 8t2e16 ⊢ ( 8 · 2 ) = 1 6
222 51 17 221 mulcomli ⊢ ( 2 · 8 ) = 1 6
223 21 178 42 198 106 25 220 222 decmul2c ⊢ ( 2 · 2 6 5 2 8 ) = 5 3 0 5 6
224 197 223 breqtri ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ 5 3 0 5 6