FORMALIZED MATHEMATICS

12

3

Volume
,
Number ,
University of Białystok

2004

Some Properties of Fibonacci Numbers
Adam Grabowski1
University of Białystok

Magdalena Jastrz¸ebska
University of Białystok

Summary. We formalized some basic properties of the Fibonacci numbers using deﬁnitions and lemmas from [7] and [23], e.g. Cassini’s and Catalan’s
identities. We also showed the connections between Fibonacci numbers and Pythagorean triples as deﬁned in [31]. The main result of this article is a proof of
Carmichael’s Theorem on prime divisors of prime-generated Fibonacci numbers.
According to it, if we look at the prime factors of a Fibonacci number generated
by a prime number, none of them have appeared as a factor in any earlier Fibonacci number. We plan to develop the full proof of the Carmichael Theorem
following [33].

This work has been partially supported by the CALCULEMUS grant HPRN-CT-200000102.

307

c
°

2004 University of Białystok
ISSN 1426–2630

(11) (−1)−2·n = 1.
Let f be a function from N into N and let A be a finite natural-membered
set with non empty elements. y such that 0 < i and i < j holds {hhi.
(14) For all natural numbers k. 2.
One can prove the following proposition
(15) For every finite subsequence p holds rng Seq p ⊆ rng p.
(12) For every non empty real number a holds ak · a−k = 1. then
m < n.
Let n be an odd integer. n1 such that k | m and k | n holds
k | m · m1 + n · n 1 . 2. The functor Prefix(f.
Let us mention that {1.
(8) For every non empty real number k and for every odd integer m holds
(k m )n = k m·n . A) = Seq(f ↾A).
The following proposition is true
(16) For every natural number k such that k 6= 0 holds if k + m ¬ n.
(10) For every non empty real number a holds a−k · a−m = a−k−m . A) yields a finite sequence
of elements of N and is defined as follows:
(Def.
(6) For every non empty real number m and for every integer n holds ((−1) ·
m)n = (−1)n · mn .
. Note that f ↾A is finite subsequence-like.
Let us mention that N is lower bounded. y and for every finite subsequence q such that i < j and
q = {hhi.
(7) For every non empty real number a holds ak+m = ak · am . xii.
(9) ((−1)−n )2 = 1. One can verify that −n is odd. h j. m. yii} is a finite
subsequence. xii.
Let f be a function from N into N and let A be a finite natural-membered
set with non empty elements. 4} is natural-membered and has non empty elements. 3. h j. yi. non empty.
Let n be an even integer. 1) Prefix(f. and naturalmembered and has non empty elements.
One can check that there exists a set which is finite.
(18) For all sets x. m1 . Note that −n is even.
Let us note that {1. yii} holds Seq q = hx.
One can prove the following two propositions:
(13) (−1)−n = (−1)n .
The following propositions are true:
(17) For all sets x.308
magdalena jastrze
¸ bska and adam grabowski
(5) For every even integer n holds (−1)n = 1. 3} is natural-membered and has non empty elements.

(24) Fib(3) = 2. y be a set. yii}.
(26) Fib(n + 2) = Fib(n) + Fib(n + 1).
If f = {hh1. yii}. The scheme Fib Ind 1
concerns a unary predicate P. Fibonacci Numbers
In this article we present several logical schemes. Then there exists a finite sequence p such that
q ⊆ p and dom p = Seg n.
Next we state a number of propositions:
(23) Fib(2) = 1.some properties of fibonacci numbers
309
Let n be a natural number. then Shifti f = {hh1 + i. Observe that
A ∩ B has non empty elements and B ∩ A has non empty elements.
. and
• For every non trivial natural number k such that P[k] and P[k+1]
holds P[k + 2]. Suppose
dom q ⊆ Seg k and n > k.
(25) Fib(4) = 3.
We now state four propositions:
(19) For every natural number k and for every set a such that k ­ 1 holds
{hhk.
• P[3]. and states that:
For every non empty natural number k holds P[k]
provided the parameters have the following properties:
• P[1]. n be natural numbers.
The scheme Fib Ind 2 concerns a unary predicate P. Observe that Seg n has non empty elements.
(22) For every finite subsequence q there exists a finite sequence p such that
q ⊆ p.
Let A be a set with non empty elements and let B be a set.
(27) Fib(n + 3) = Fib(n + 2) + Fib(n + 1). aii} is a finite subsequence.
• P[2].
(20) Let i.
(21) Let q be a finite subsequence and k. Note that every subset of A has
non empty elements.
(28) Fib(n + 4) = Fib(n + 2) + Fib(n + 3). and f be a finite subsequence. and states that:
For every non trivial natural number k holds P[k]
provided the parameters meet the following conditions:
• P[2]. and
• For every non empty natural number k such that P[k] and P[k+1]
holds P[k + 2].
Let A be a set with non empty elements.
2. k be natural numbers.