:: Fibonacci Numbers
:: by Robert M. Solovay
::
:: Received April 19, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: FIB_NUM:1
theorem Th2: :: FIB_NUM:2
theorem Th3: :: FIB_NUM:3
(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
Lm4:
for m being Element of NAT holds Fib (m + 1) >= Fib m
Lm5:
for m, n being Element of NAT st m >= n holds
Fib m >= Fib n
Lm6:
for m being Element of NAT holds Fib (m + 1) <> 0
theorem Th4: :: FIB_NUM:4
Lm7:
for n being Element of NAT holds (Fib n) gcd (Fib (n + 1)) = 1
theorem :: FIB_NUM:5
theorem Th6: :: FIB_NUM:6
:: deftheorem defines tau FIB_NUM:def 1 :
:: deftheorem defines tau_bar FIB_NUM:def 2 :
Lm8:
( tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 )
Lm9:
2 < sqrt 5
by SQUARE_1:85, SQUARE_1:95;
Lm10:
sqrt 5 <> 0
by SQUARE_1:85, SQUARE_1:95;
Lm11:
sqrt 5 < 3
1 < tau
then Lm12:
0 < tau
by XXREAL_0:2;
Lm13:
tau_bar < 0
Lm14:
abs tau_bar < 1
theorem Th7: :: FIB_NUM:7
Lm15:
for n being Element of NAT
for x being real number st abs x <= 1 holds
abs (x |^ n) <= 1
Lm16:
for n being Element of NAT holds abs ((tau_bar to_power n) / (sqrt 5)) < 1
theorem :: FIB_NUM:8
theorem :: FIB_NUM:9
canceled;
theorem Th10: :: FIB_NUM:10
theorem Th11: :: FIB_NUM:11
theorem :: FIB_NUM:12