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