Here's a sketch of an answer. Let $a > b > c$ be the three real roots of $f(x) = x^3 - 3x^2 + 1$ and note that $a > 1 > b > 0 > c > -1$. Let $t_n = a^n + b^n + c^n$. Write down the first three values of $t_n$ and note that it satisfies a recurrence relation with driving polynomial $f$: that is, $t_{n+3} = 3t_{n+2} - t_n$. Reduce modulo 17, find the cycles and check that $t_{1788}$ and $t_{1988}$ are zero mod 17. Finally observe that $t_N$ = $\lfloor a^N \rfloor$ for large even $N$ since $\vert b \vert, \vert c \vert < 1$.

Actually (and fortunately ) you should check that $ t_{1788}$ and $ t_{1988}$ are 1 mod 17, and then observe, that since $ 1>|b|>|c|$ and $ b>0>c$ and $ b^{2}+c^{2}<2$, $ 0<b^{k}+c^{k}<1$ and thus $ 1\equiv t_{1788}>t_{1788}-b^{1788}-c^{1788}=a^{1788}>[a^{1788}]=t_{1788}\equiv0\pmod{17}$. Same with 1988.

Finding the cycles could be a bit boring... Maybe it is more easy to prove that $ a^{n}+b^{n}+c^{n}\equiv 4^{n}+5^{n}+11^{n}\pmod{17}$

piever wrote: Finding the cycles could be a bit boring... Maybe it is more easy to prove that $ a^{n}+b^{n}+c^{n}\equiv 4^{n}+5^{n}+11^{n}\pmod{17}$ And then finding the cycles again for $ 4^{n}$, $ 5^{n}$ and $ 11^{n}$... But you're right, it is clearly visible that their cycles' lengths are at most 16, which is not evident at the $ t_{i}$ sequence. However the latter cycle's length is 16, so this is not a big problem. Another thing is, i don't think your identity shines from $ t_{n}$

I solved for a. Let a-1=k, then we have $ k^3 = 3k + 1$ Let $ k = 2cos m$, then we have $ 2(4cos^3m - 3cosm) = 1$ $ cos(3m) = 1/2$ $ 3m = 60$ gives the largest root. So $ a = 2cos20 + 1$ The other roots are $ 2cos100 + 1$ and $ 2 cos 140 + 1$ Is it possible to solve it this way?

How could someone better explain this problem and fully reverse the recurrence is not my thing but it is very clear. Thanks in advance. Greetings