:: by Robert M. Solovay

::

:: Received April 19, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

:: Preliminary lemmas

scheme :: FIB_NUM:sch 2

BinInd{ P_{1}[ Nat, Nat] } :

provided

BinInd{ P

provided

A1:
for m, n being Element of NAT st P_{1}[m,n] holds

P_{1}[n,m]
and

A2: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds

P_{1}[m,n] ) holds

for m being Element of NAT st m <= k holds

P_{1}[k,m]

P

A2: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds

P

for m being Element of NAT st m <= k holds

P

proof end;

(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

proof end;

Lm4: for m being Nat holds Fib (m + 1) >= Fib m

proof end;

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

Fib m >= Fib n

proof end;

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

proof end;

Lm7: for n being Nat holds (Fib n) gcd (Fib (n + 1)) = 1

proof end;

theorem Th6: :: 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) ) )

( ((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) ) )

proof end;

:: The roots of x^2 - x - 1 = 0

:: The value of tau is approximately 1.618

:: The value of tau is approximately 1.618

:: The value of tau_bar is approximately -.618

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

proof end;

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

proof end;

1 < tau

proof end;

then Lm12: 0 < tau

;

Lm13: tau_bar < 0

proof end;

Lm14: |.tau_bar.| < 1

proof end;

Lm15: for n being Element of NAT

for x being Real st |.x.| <= 1 holds

|.(x |^ n).| <= 1

proof end;

Lm16: for n being Element of NAT holds |.((tau_bar to_power n) / (sqrt 5)).| < 1

proof end;

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) & (f /" g) . n = (f . n) * ((g . n) ") )

for n being Element of NAT holds

( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") )

proof end;

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 )

( F is convergent & lim F = tau )

proof end;