Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

Fibonacci Numbers


Robert M. Solovay
P. O. Box 5949, Eugene OR 97405, U. S. A.

Summary.

We show that Fibonacci commutes with g.c.d.; we then derive the formula connecting the Fibonacci sequence with the roots of the polynomial $x^2 - x - 1.$

MML Identifier: FIB_NUM

The terminology and notation used in this paper have been introduced in the following articles [2] [9] [10] [5] [1] [3] [4] [7] [6] [8]

Contents (PDF format)

  1. Fibonacci Commutes with gcd
  2. Fibonacci Numbers and the Golden Mean

Acknowledgments

My thanks to Freek Wiedijk for helping me learn Mizar and to Piotr Rudnicki for instructive comments on an earlier version of this article. This article was finished while I was visiting Bialystok and Adam Naumowicz and Josef Urban helped me through some difficult moments.

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek and Piotr Rudnicki. Two programs for \bf scm. Part I - preliminaries. Journal of Formalized Mathematics, 5, 1993.
[4] Jaroslaw Kotowicz. Convergent sequences and the limit of sequences. Journal of Formalized Mathematics, 1, 1989.
[5] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.
[6] Jan Popiolek. Some properties of functions modul and signum. Journal of Formalized Mathematics, 1, 1989.
[7] Jan Popiolek. Quadratic inequalities. Journal of Formalized Mathematics, 3, 1991.
[8] Konrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Journal of Formalized Mathematics, 2, 1990.
[9] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[10] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

Received April 19, 2002

[ Download a postscript version, MML identifier index, Mizar home page]