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
SetBuilder$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$ Set comprehension
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, SetBuilder(Fibonacci(n), n, Element(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.

2019-08-19 14:38:23.809000 UTC