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]

Fibonacci Commutes with gcd

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]