:: 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;