In the paper we show how to express the Fibonacci numbers and Lucas numbers using the floor and ceiling operations.
@article{bwmeta1.element.doi-10_2478_v10037-010-0010-1,
author = {Magdalena Jastrz\k ebska},
title = {Representation of the Fibonacci and Lucas Numbers in Terms of Floor and Ceiling},
journal = {Formalized Mathematics},
volume = {18},
year = {2010},
pages = {77-80},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-010-0010-1}
}
Magdalena Jastrzębska. Representation of the Fibonacci and Lucas Numbers in Terms of Floor and Ceiling. Formalized Mathematics, Tome 18 (2010) pp. 77-80. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-010-0010-1/
[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
[2] Grzegorz Bancerek and Piotr Rudnicki. Two programs for SCM. Part I - preliminaries. Formalized Mathematics, 4(1):69-72, 1993.
[3] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990.
[4] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Public-key cryptography and Pepin's test for the primality of Fermat numbers. Formalized Mathematics, 7(2):317-321, 1998.
[5] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990.
[6] Konrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213-216, 1991.
[7] Piotr Rudnicki and Andrzej Trybulec. Abian's fixed point theorem. Formalized Mathematics, 6(3):335-338, 1997.
[8] Robert M. Solovay. Fibonacci numbers. Formalized Mathematics, 10(2):81-83, 2002.
[9] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990.
[10] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
[11] Piotr Wojtecki and Adam Grabowski. Lucas numbers and generalized Fibonacci numbers. Formalized Mathematics, 12(3):329-333, 2004.