:: Fibonacci Numbers
:: by Robert M. Solovay
::
:: Received April 19, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

:: Preliminary lemmas
theorem Th1: :: FIB_NUM:1
for m, n being Element of NAT holds m gcd n = m gcd (n + m)
proofend;

theorem Th2: :: FIB_NUM:2
for k, m, n being Element of NAT st k gcd m = 1 holds
k gcd (m * n) = k gcd n
proofend;

theorem Th3: :: FIB_NUM:3
for s being real number st s > 0 holds
ex n being Element of NAT st
( n > 0 &amp; 0 < 1 / n &amp; 1 / n <= s )
proofend;

scheme :: FIB_NUM:sch 1
FibInd{ P1[ set ] } :
 for k being Nat holds P1[k]
provided
A1: P1[ 0 ] and
A2: P1[1] and
A3: for k being Nat st P1[k] &amp; P1[k + 1] holds
P1[k + 2]
proofend;

scheme :: FIB_NUM:sch 2
BinInd{ P1[ Nat, Nat] } :
 for m, n being Element of NAT holds P1[m,n]
provided
A1: for m, n being Element of NAT st P1[m,n] holds
P1[n,m] and
A2: for k being Element of NAT st ( for m, n being Element of NAT st m < k &amp; n < k holds
P1[m,n] ) holds
for m being Element of NAT st m <= k holds
P1[k,m]
proofend;

 (0 + 1) + 1 = 2
;

then Lm1:  Fib 2 = 1
by PRE_FF:1;

Lm2:  (1 + 1) + 1 = 3
;

Lm3:  for k being Nat holds Fib (k + 1) >= k
proofend;

Lm4:  for m being Element of NAT holds Fib (m + 1) >= Fib m
proofend;

Lm5:  for m, n being Element of NAT st m >= n holds
Fib m >= Fib n
proofend;

Lm6:  for m being Element of NAT holds Fib (m + 1) <> 0
proofend;

theorem Th4: :: FIB_NUM:4
for m, n being Nat holds Fib (m + (n + 1)) = ((Fib n) * (Fib m)) + ((Fib (n + 1)) * (Fib (m + 1)))
proofend;

Lm7:  for n being Element of NAT holds (Fib n) gcd (Fib (n + 1)) = 1
proofend;

theorem :: FIB_NUM:5
for m, n being Element of NAT holds (Fib m) gcd (Fib n) = Fib (m gcd n)
proofend;

begin

theorem Th6: :: FIB_NUM:6
for x, a, b, c being real number st a <> 0 &amp; 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) ) )
proofend;

:: The roots of x^2 - x - 1 = 0
:: The value of tau is approximately 1.618
definition
func tau  ->  real number  equals :: FIB_NUM:def 1
(1 + (sqrt 5)) / 2;
correctness
coherence
(1 + (sqrt 5)) / 2 is real number ;
;
end;

:: deftheorem  defines tau FIB_NUM:def_1_:_
 tau = (1 + (sqrt 5)) / 2;

:: The value of tau_bar is approximately -.618
definition
func tau_bar  ->  real number  equals :: FIB_NUM:def 2
(1 - (sqrt 5)) / 2;
correctness
coherence
(1 - (sqrt 5)) / 2 is real number ;
;
end;

:: deftheorem  defines tau_bar FIB_NUM:def_2_:_
 tau_bar = (1 - (sqrt 5)) / 2;

Lm8:  ( tau ^2 = tau + 1 &amp; tau_bar ^2 = tau_bar + 1 )
proofend;

Lm9:  2 < sqrt 5
by SQUARE_1:20, SQUARE_1:27;

Lm10:  sqrt 5 <> 0
by SQUARE_1:20, SQUARE_1:27;

Lm11:  sqrt 5 < 3
proofend;

 1 < tau
proofend;

then Lm12:  0 < tau
by XXREAL_0:2;

Lm13:  tau_bar < 0
proofend;

Lm14:  abs tau_bar < 1
proofend;

theorem Th7: :: FIB_NUM:7
for n being Nat holds Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)
proofend;

Lm15:  for n being Element of NAT
for x being real number st abs x <= 1 holds
abs (x |^ n) <= 1
proofend;

Lm16:  for n being Element of NAT holds abs ((tau_bar to_power n) / (sqrt 5)) < 1
proofend;

theorem :: FIB_NUM:8
for n being Element of NAT holds abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1
proofend;

theorem Th9: :: FIB_NUM:9
for f, g, h being Real_Sequence st g is non-zero holds
(f /" g) (#) (g /" h) = f /" h
proofend;

theorem Th10: :: FIB_NUM:10
for f, g being Real_Sequence
for n being Element of NAT holds
( (f /" g) . n = (f . n) / (g . n) &amp; (f /" g) . n = (f . n) * ((g . n) ") )
proofend;

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 &amp; lim F = tau )
proofend;