Fungrim home page

Fungrim entry: a0206a

(x{Fn:nZ0})    (5x2+4Z  or  5x24Z)\left(x \in \left\{ F_{n} : n \in \mathbb{Z}_{\ge 0} \right\}\right) \iff \left(\sqrt{5 {x}^{2} + 4} \in \mathbb{Z} \;\mathbin{\operatorname{or}}\; \sqrt{5 {x}^{2} - 4} \in \mathbb{Z}\right)
Assumptions:xZ0x \in \mathbb{Z}_{\ge 0}
\left(x \in \left\{ F_{n} : n \in \mathbb{Z}_{\ge 0} \right\}\right) \iff \left(\sqrt{5 {x}^{2} + 4} \in \mathbb{Z} \;\mathbin{\operatorname{or}}\; \sqrt{5 {x}^{2} - 4} \in \mathbb{Z}\right)

x \in \mathbb{Z}_{\ge 0}
Fungrim symbol Notation Short description
FibonacciFnF_{n} Fibonacci number
ZZGreaterEqualZn\mathbb{Z}_{\ge n} Integers greater than or equal to n
Sqrtz\sqrt{z} Principal square root
Powab{a}^{b} Power
ZZZ\mathbb{Z} Integers
Source code for this entry:
    Formula(Equivalent(Element(x, Set(Fibonacci(n), ForElement(n, ZZGreaterEqual(0)))), Or(Element(Sqrt(Add(Mul(5, Pow(x, 2)), 4)), ZZ), Element(Sqrt(Sub(Mul(5, Pow(x, 2)), 4)), ZZ)))),
    Assumptions(Element(x, ZZGreaterEqual(0))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC