:: Representation of the {F}ibonacci and {L}ucas Numbers in Terms of
:: the Floor and Ceiling Functor
:: by Magdalena Jastrz\c{e}bska
::
:: Received November 30, 2009
:: Copyright (c) 2009-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 ARYTM_1, ARYTM_3, SQUARE_1, PRE_FF, NAT_1, FIB_NUM, POWER, INT_1,
FIB_NUM3, CARD_1, NUMBERS, ABIAN, XXREAL_0, RELAT_1, NEWTON, PREPOWER,
COMPLEX1, ZFMISC_1, SUBSET_1, REAL_1, XCMPLX_0;
notations ORDINAL1, SUBSET_1, XBOOLE_0, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, INT_1, NAT_D, PRE_FF, ZFMISC_1, NEWTON, POWER, FIB_NUM3,
PREPOWER, ABIAN, COMPLEX1, FIB_NUM, PEPIN;
constructors REAL_1, NAT_1, NAT_D, NEWTON, PREPOWER, POWER, PRE_FF, ABIAN,
PEPIN, FIB_NUM, FIB_NUM3;
registrations ORDINAL1, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, XCMPLX_0,
COMPLEX1, FIB_NUM3, POWER, NEWTON, PREPOWER, ABIAN, NAT_2;
requirements SUBSET, NUMERALS, REAL, ARITHM;
begin
theorem :: FIB_NUM4:1
for a,b being Real, c being Nat holds
(a / b) to_power c = (a to_power c) / (b to_power c);
theorem :: FIB_NUM4:2
for a being Real, b,c being Integer st a <> 0 holds
a to_power (b+c) = a to_power b * a to_power c;
theorem :: FIB_NUM4:3
for n being Nat, a being Real st n is even & a <> 0 holds
(-a) to_power n = a to_power n;
theorem :: FIB_NUM4:4
for n being Nat, a being Real st n is odd & a <> 0 holds
(-a) to_power n = -(a to_power n);
theorem :: FIB_NUM4:5
|.tau_bar.| < 1;
theorem :: FIB_NUM4:6
for n being Nat, r being non zero Real st n is even holds
r to_power n > 0;
theorem :: FIB_NUM4:7
for n being Nat, r being Real st n is odd & r < 0 holds
r to_power n < 0;
theorem :: FIB_NUM4:8
for n being Nat st n <> 0 holds tau_bar to_power n < 1/2;
theorem :: FIB_NUM4:9
for n,m being Nat, r being Real st
m is odd & n >= m & r < 0 & r > -1 holds
r to_power n >= r to_power m;
theorem :: FIB_NUM4:10
for n,m being Nat st m is odd & n >= m holds
tau_bar to_power n >= tau_bar to_power m;
theorem :: FIB_NUM4:11
for n,m being Nat st n is even & m is even & n >= m holds
tau_bar to_power n <= tau_bar to_power m;
theorem :: FIB_NUM4:12
for m,n being non zero Nat st m >= n holds Lucas m >= Lucas n;
theorem :: FIB_NUM4:13
for n being non zero Nat holds
tau to_power n > tau_bar to_power n;
theorem :: FIB_NUM4:14
for n being Nat st n > 1 holds -1/2 < tau_bar to_power n;
theorem :: FIB_NUM4:15
for n being Nat st n > 2 holds tau_bar to_power n >= - 1/sqrt 5;
theorem :: FIB_NUM4:16
for n being Nat st n >= 2 holds tau_bar to_power n <= 1/sqrt 5;
theorem :: FIB_NUM4:17
for n being Nat holds (tau_bar to_power n)/sqrt 5 + 1/2 > 0 &
(tau_bar to_power n)/sqrt 5 + 1/2 < 1;
begin :: Formulas for the Fibonacci Numbers
theorem :: FIB_NUM4:18
for n being Nat holds [\ (tau to_power n )/sqrt 5 + 1/2 /] = Fib n;
theorem :: FIB_NUM4:19
for n being Nat st n <> 0 holds
[/ (tau to_power n)/sqrt 5 - 1/2 \] = Fib n;
theorem :: FIB_NUM4:20
for n being Nat st n <> 0 holds
[\ (tau to_power (2*n)) / sqrt 5 /] = Fib (2*n);
theorem :: FIB_NUM4:21
for n being Nat holds
[/ (tau to_power (2*n+1)) / sqrt 5 \] = Fib (2*n+1);
theorem :: FIB_NUM4:22
for n being Nat st n >= 2 & n is even holds
Fib (n+1) = [\ tau * Fib n + 1 /];
theorem :: FIB_NUM4:23
for n being Nat st n >= 2 & n is odd holds
Fib (n+1) = [/ tau * Fib n - 1 \];
theorem :: FIB_NUM4:24
for n being Nat st n >= 2 holds
Fib (n+1) = [\ (Fib n + sqrt 5 * Fib n + 1) / 2 /];
theorem :: FIB_NUM4:25
for n being Nat st n >= 2 holds
Fib (n+1) = [/ (Fib n + sqrt 5 * Fib n - 1)/2 \];
theorem :: FIB_NUM4:26
for n being Nat holds
Fib (n+1) = (Fib n + sqrt(5*(Fib n)^2 + 4*(-1) to_power n))/2;
theorem :: FIB_NUM4:27
for n being Nat st n >= 2 holds
Fib (n+1) = [\ (Fib(n) + 1 + sqrt(5*(Fib(n))^2 - 2 * Fib(n) + 1) )/2 /];
theorem :: FIB_NUM4:28
for n being Nat st n >= 2 holds
Fib n = [\ (1/tau) * (Fib (n+1) + 1/2)/];
theorem :: FIB_NUM4:29
for n,k being Nat st (n >= k & k > 1) or (k = 1 & n > k) holds
[\ tau to_power k * Fib n + 1/2 /] = Fib (n + k);
begin :: Formulas for the Lucas Numbers
theorem :: FIB_NUM4:30
for n being Nat st n >= 2 holds
Lucas(n) = [\ tau to_power n + 1/2 /];
theorem :: FIB_NUM4:31
for n being Nat st n >= 2 holds
Lucas (n) = [/ tau to_power n - 1/2 \];
theorem :: FIB_NUM4:32
for n being Nat st n >= 2 holds
Lucas (2*n) = [/ tau to_power (2*n) \];
theorem :: FIB_NUM4:33
for n being Nat st n >= 2 holds
Lucas (2*n+1) = [\ tau to_power (2*n+1) /];
theorem :: FIB_NUM4:34
for n being Nat st n >= 2 & n is odd holds
Lucas (n+1) = [\ tau * Lucas (n) + 1 /];
theorem :: FIB_NUM4:35
for n being Nat st n >= 2 & n is even holds
Lucas (n+1) = [/ tau * Lucas n - 1 \];
theorem :: FIB_NUM4:36
for n being Nat st n <> 1 holds
Lucas (n+1) = (Lucas n + sqrt(5*((Lucas n)^2 - 4*(-1) to_power n)))/2;
theorem :: FIB_NUM4:37
for n being Nat st n >= 4 holds
Lucas (n+1) = [\ (Lucas n + 1 + sqrt(5*(Lucas n)^2 - 2*Lucas n + 1))/2 /];
theorem :: FIB_NUM4:38
for n being Nat st n > 2 holds
Lucas n = [\ (1/tau) * (Lucas (n+1) + 1/2) /];
theorem :: FIB_NUM4:39
for n,k being Nat st n >= 4 & k >= 1 & n > k & n is odd holds
Lucas (n+k) = [\ tau to_power k * Lucas n + 1 /];