:: Fibonacci Numbers
:: by Robert M. Solovay
::
:: Received April 19, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, INT_2, ARYTM_3, RELAT_1, NAT_1, CARD_1,
XXREAL_0, PRE_FF, FUNCT_3, SQUARE_1, ARYTM_1, COMPLEX1, POWER, NEWTON,
SEQ_1, VALUED_0, VALUED_1, FUNCT_1, SEQ_2, ORDINAL2, XXREAL_2, FIB_NUM,
REAL_1;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1,
NAT_1, NAT_D, INT_2, VALUED_0, VALUED_1, SEQ_1, XXREAL_0, COMPLEX1,
PRE_FF, COMSEQ_2, SEQ_2, QUIN_1, NEWTON, POWER;
constructors REAL_1, SQUARE_1, NAT_1, NAT_D, QUIN_1, SEQ_2, SEQM_3, LIMFUNC1,
NEWTON, POWER, PRE_FF, VALUED_1, PARTFUN1, SETFAM_1, RELSET_1, BINOP_2,
RVSUM_1, COMSEQ_2, NUMBERS;
registrations RELSET_1, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, INT_1,
VALUED_0, VALUED_1, FUNCT_2, NUMBERS, SEQ_4, NAT_1, SEQ_2, ORDINAL1,
FDIFF_1;
requirements SUBSET, NUMERALS, REAL, ARITHM;
begin
:: Fibonacci commutes with gcd
:: The proof we present is a slight adaptation of the one found in
:: ``The Fibonacci Numbers'' by N. N. Vorobyov
reserve k,m, n, p for Element of NAT;
:: Preliminary lemmas
theorem :: FIB_NUM:1
for m, n being Element of NAT holds m gcd n = m gcd (n + m);
theorem :: FIB_NUM:2
for k, m, n being Element of NAT st k gcd m = 1 holds k gcd m * n = k gcd n;
theorem :: FIB_NUM:3
for s being Real st s > 0 ex n being Element of NAT st n >
0 & 0 < 1/n & 1/n <= s;
scheme :: FIB_NUM:sch 1
FibInd {P[set] } : for k being Nat holds P[k]
provided
P[0] and
P[1] and
for k being Nat st P[k] & P[k+1] holds P[k+2];
scheme :: FIB_NUM:sch 2
BinInd { P[Nat,Nat] } : for m, n being Element of NAT holds P[m, n]
provided
for m, n being Element of NAT st P[m,n] holds P[n,m] and
for k being Element of NAT st (for m, n being Element of NAT st (m <
k & n < k) holds P[m,n]) holds for m being Element of NAT st m <= k holds P[k,m
];
theorem :: FIB_NUM:4
for m, n being Nat holds Fib(m + (n + 1)) = (Fib(n) * Fib (m)) +
(Fib(n + 1) * Fib (m + 1));
theorem :: FIB_NUM:5
for m, n being Element of NAT holds Fib(m) gcd Fib(n) = Fib(m gcd n);
begin
:: The relationship between the Fibonacci numbers and the
:: roots of the equation x^2 = x + 1
:: The formula for the roots of a quadratic equation
reserve x, a, b, c for Real;
theorem :: FIB_NUM:6
for x, a, b, c being Real st a <> 0 & delta(a,b,c) >= 0
holds a * x^2 + b * x + c = 0 iff (x = (- b - sqrt delta(a,b,c))/(2 * a) or x =
(- b + sqrt delta(a,b,c))/(2 * a));
:: The roots of x^2 - x - 1 = 0
:: The value of tau is approximately 1.618
definition
func tau -> Real equals
:: FIB_NUM:def 1
(1 + sqrt 5)/2;
end;
:: The value of tau_bar is approximately -.618
definition
func tau_bar -> Real equals
:: FIB_NUM:def 2
(1 - sqrt 5)/2;
end;
theorem :: FIB_NUM:7
for n being Nat holds Fib(n) = ((tau to_power n) - (tau_bar
to_power n))/(sqrt 5);
theorem :: FIB_NUM:8
for n being Element of NAT holds |.Fib(n) - (tau to_power n)/(sqrt 5 ).| < 1;
reserve F, f, g, h for Real_Sequence;
theorem :: FIB_NUM:9
for f, g, h being Real_Sequence st g is non-zero holds (f /" g)
(#) (g /" h) = (f /" h);
theorem :: FIB_NUM:10
for f, g being Real_Sequence for n being Element of NAT holds (f
/" g) . n = (f .n) / (g.n) & (f /" g) . n = (f.n) * (g.n)";
theorem :: FIB_NUM:11
for F being Real_Sequence st (for n being Element of NAT holds F.n =
Fib(n+1)/Fib(n)) holds F is convergent & lim F = tau;