# Fungrim entry: a0206a

$\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:$x \in \mathbb{Z}_{\ge 0}$
TeX:
\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}
Definitions:
Fungrim symbol Notation Short description
Fibonacci$F_{n}$ Fibonacci number
ZZGreaterEqual$\mathbb{Z}_{\ge n}$ Integers greater than or equal to n
Sqrt$\sqrt{z}$ Principal square root
Pow${a}^{b}$ Power
ZZ$\mathbb{Z}$ Integers
Source code for this entry:
Entry(ID("a0206a"),
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)))),
Variables(x),
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