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

Fibonacci numbers