Fungrim home page

Fungrim entry: a0206a

(x{Fn:nZ0})    (5x2+4Zor5x24Z)\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}
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{f ⁣(x):P ⁣(x)}\left\{ f\!\left(x\right) : P\!\left(x\right) \right\} Set comprehension
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:
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