How to invert Binet's formula for Fibonacci numbers

According to Wikipedia, it is possible to invert Binet's formula for Fibonacci numbers:

$$F_n = \frac{\varphi^n-\psi^n}{\varphi-\psi} = \frac{\varphi^n-\psi^n}{\sqrt 5}$$ where $\varphi = \frac{1 + \sqrt{5}}{2} \approx 1.61803\,39887\ldots$ and $\psi = \frac{1 - \sqrt{5}}{2} = 1 - \varphi = - {1 \over \varphi} \approx -0.61803\,39887\ldots$, or more specifically the truncating variant of that:

$$F_n = \left\lfloor\frac{\varphi^n}{\sqrt 5} + \frac{1}{2}\right\rfloor$$

to find the index $n(F)$ of the largest Fibonacci number that is not greater than a real number $F > 1$:

$$n(F) = \left\lfloor \log_\varphi (F\sqrt5 + 1/2)\right\rfloor$$

Since no justification is given, besides the floor function being monotonic, I would like to prove this.

So assuming the truncating formula holds: $$F_n = \left\lfloor\frac{\varphi^n}{\sqrt 5} + \frac{1}{2}\right\rfloor$$ $$F_n = \frac{\varphi^n}{\sqrt 5} + \frac{1}{2} + E, \text{where $0 \le E < 1$}$$ $$\varphi^n = \sqrt5(F_n - \frac{1}{2} - E), \text{where $0 \le E < 1$}$$ $$n \log\varphi = \log(\sqrt5(F_n - \frac{1}{2} - E)), \text{where $0 \le E < 1$}$$ $$n = \log_\varphi(\sqrt5(F_n - \frac{1}{2} - E)), \text{where $0 \le E < 1$}$$

Since n is a whole number we can take the floor:

$$n = \lfloor n \rfloor = \left\lfloor \log_\varphi(\sqrt5(F_n - \frac{1}{2} - E)) \right\rfloor, \text{where $0 \le E < 1$}$$ $$n = \left\lfloor \log_\varphi(\sqrt5 F_n \left(1 - \frac{1 + 2E}{2F_n}\right) \right\rfloor, \text{where $0 \le E < 1$}$$ $$n = \left\lfloor \log_\varphi(\sqrt5 F_n) + \log_\varphi \left(1 - \frac{1 + 2E}{2F_n}\right) \right\rfloor, \text{where $0 \le E < 1$}$$

And this does not seem to be the right path...

We have $$F_n =\frac{\phi^n-(-\frac{1}{\phi})^n}{\sqrt{5}}$$ what can be inversed writing $$\phi^{2n}-F_n\sqrt{5}\,\phi^n-(-1)^n = 0$$ which is a quadratic in $\phi^n$. So $$\phi^n=\frac{F_n\sqrt{5}+\sqrt{5F_n^2\pm 4}}{2}\implies n_\pm \log(\phi)=\log\Bigg[\frac{F_n\sqrt{5}+\sqrt{5F_n^2\pm 4}}{2} \Bigg]$$ One of the two solution is an integer $$\left( \begin{array}{cccc} n & F_n & n_- & n_+ \\ 3 & 2 & 3.000000000 & 3.209573980 \\ 4 & 3 & 3.907487979 & 4.000000000 \\ 5 & 5 & 5.000000000 & 5.033256487 \\ 6 & 8 & 5.987011534 & 6.000000000 \\ 7 & 13 & 7.000000000 & 7.004918572 \\ 8 & 21 & 7.998115113 & 8.000000000 \\ 9 & 34 & 9.000000000 & 9.000719061 \\ 10 & 55 & 9.999725212 & 10.00000000 \end{array} \right)$$

If this is not the case, then the number is not Fibonacci. Trying for $12345678987654321$, the result is $n_\pm=78.669724$; so, it is not a Fibonacci number (but we know the closest one). $$F_{78}=8944394323791464 \quad < \quad 12345678987654321$$ $$F_{79}=14472334024676221 \quad > \quad 12345678987654321$$

Edit

Consider what is the difference between the two roots : consider $F_n$ to be large and make a series expansion $$n_+-n_-\sim\frac{2}{5 F_n^2 \log (\phi )} <\frac{1}{ F_n^2 }$$