IrMO 1990 Problem 8

Let $t$ be a real number, and let $$a_n=2\cos \left(\frac{t}{2^n}\right)-1, n=1,2,3,\dots$$ Let $b_n$ be the product $a_1a_2a_3\cdots a_n$ . Find a formula for $b_n$ that does not involve a product of $n$ terms, and deduce that $$\lim_{n\to \infty}b_n=\frac{2\cos t+1}{3}$$