:: Fibonacci Numbers
::  by Robert M. Solovay
::
:: Received April 19, 2002
:: Copyright (c) 2002-2012 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 NUMBERS, SUBSET_1, INT_2, ARYTM_3, RELAT_1, NAT_1, CARD_1,
      XXREAL_0, XREAL_0, ORDINAL1, PRE_FF, FUNCT_3, SQUARE_1, ARYTM_1,
      COMPLEX1, POWER, NEWTON, SEQ_1, VALUED_0, VALUED_1, FUNCT_1, SEQ_2,
      ORDINAL2, XXREAL_2, FIB_NUM;
 notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, NAT_1,
      NAT_D, INT_2, VALUED_0, VALUED_1, SEQ_1, XXREAL_0, COMPLEX1, PRE_FF,
      COMSEQ_2, SEQ_2, QUIN_1, NEWTON, POWER;
 constructors REAL_1, SQUARE_1, NAT_1, NAT_D, QUIN_1, SEQ_2, SEQM_3, LIMFUNC1,
      NEWTON, POWER, PRE_FF, SEQ_1, VALUED_1, PARTFUN1, SETFAM_1, RELSET_1,
      BINOP_2, RVSUM_1, COMSEQ_2;
 registrations RELSET_1, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, INT_1,
      VALUED_0, VALUED_1, FUNCT_2, NUMBERS, SEQ_4, SETFAM_1, REALSET1,
      FINSET_1, COMSEQ_2, NAT_1;
 requirements SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
 definitions SQUARE_1, VALUED_1, XCMPLX_0;
 theorems NAT_1, PRE_FF, INT_2, SQUARE_1, WSIERP_1, EULER_1, PYTHTRIP, QUIN_1,
      ABSVALUE, POWER, NEWTON, SEQM_3, SEQ_1, SEQ_2, SEQ_4, PREPOWER, XCMPLX_0,
      XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, FUNCT_2, ORDINAL1, NAT_D,
      VALUED_1, VALUED_0, XREAL_0;
 schemes NAT_1, SEQ_1;

begin

:: Fibonacci commutes with gcd
:: The proof we present is a slight adaptation of the one found in
:: ``The Fibonacci Numbers'' by N. N. Vorobyov

reserve k,m, n, p for Element of NAT;

:: Preliminary lemmas

theorem Th1:
  for m, n being Element of NAT holds m gcd n = m gcd (n + m)
proof
  let m, n;
  set a = m gcd n;
  set b = m gcd (n + m);
A1: a divides m by NAT_D:def 5;
A2: b divides m by NAT_D:def 5;
  b divides n + m by NAT_D:def 5;
  then b divides n by A2,NAT_D:10;
  then
A3: b divides a by A2,NAT_D:def 5;
  a divides n by NAT_D:def 5;
  then a divides n + m by A1,NAT_D:8;
  then a divides b by A1,NAT_D:def 5;
  hence thesis by A3,NAT_D:5;
end;

theorem Th2:
  for k, m, n being Element of NAT st k gcd m = 1 holds k gcd m * n = k gcd n
proof
  defpred P[Nat] means for m, n holds $1 gcd m = 1 implies $1 gcd m * n = $1
  gcd n;
A1: for k being Nat holds (for a being Nat st a < k holds P[a]) implies P[k]
  proof
    let k be Nat;
    assume
A2: for a being Nat st a < k holds P[a];
    per cases by NAT_1:25;
    suppose
A3:   k = 0;
      let m, n;
      assume k gcd m = 1;
      then 1 = m by A3,NEWTON:52;
      hence thesis;
    end;
    suppose
A4:   k = 1;
      let m, n;
      assume k gcd m = 1;
      k gcd m * n = 1 by A4,NEWTON:51;
      hence thesis by A4,NEWTON:51;
    end;
    suppose
A5:   k > 1;
      let m, n;
      set b = k gcd m * n;
      assume
A6:   k gcd m = 1;
      thus thesis
      proof
        per cases by NAT_1:25;
        suppose
          b = 0;
          then 0 divides k by NAT_D:def 5;
          then k = 0 by INT_2:3;
          hence thesis by A5;
        end;
        suppose
A7:       b = 1;
          set c = k gcd n;
A8:       c divides k by NAT_D:def 5;
A9:       n divides m * n by NAT_D:def 3;
          c divides n by NAT_D:def 5;
          then c divides m * n by A9,NAT_D:4;
          then c divides 1 by A7,A8,NAT_D:def 5;
          hence thesis by A7,WSIERP_1:15;
        end;
        suppose
          b > 1;
          then b >= 1 + 1 by NAT_1:13;
          then consider p such that
A10:      p is prime and
A11:      p divides b by INT_2:31;
          b divides k by NAT_D:def 5;
          then
A12:      p divides k by A11,NAT_D:4;
          then consider s being Nat such that
A13:      k = p * s by NAT_D:def 3;
A14:      not p divides m
          proof
            assume p divides m;
            then p divides 1 by A6,A12,NAT_D:def 5;
            then p = 1 by WSIERP_1:15;
            hence thesis by A10,INT_2:def 4;
          end;
          b divides m * n by NAT_D:def 5;
          then p divides m * n by A11,NAT_D:4;
          then p divides n by A10,A14,NEWTON:80;
          then consider r being Nat such that
A15:      n = p * r by NAT_D:def 3;
          reconsider s as Element of NAT by ORDINAL1:def 12;
A16:      s + 1 > s by XREAL_1:29;
          p > 1 by A10,INT_2:def 4;
          then p >= 1 + 1 by NAT_1:13;
          then
A17:      s * p >= s * (1 + 1) by NAT_1:4;
          s <> 0 by A5,A13;
          then s + s > s by NAT_1:3,XREAL_1:29;
          then s + s >= s + 1 by NAT_1:13;
          then k >= s + 1 by A13,A17,XXREAL_0:2;
          then
A18:      s < k by A16,XXREAL_0:2;
A19:      s gcd m = 1
          proof
            set c = s gcd m;
A20:        c divides s by NAT_D:def 5;
A21:        c divides m by NAT_D:def 5;
            s divides k by A13,NAT_D:def 3;
            then c divides k by A20,NAT_D:4;
            then c divides 1 by A6,A21,NAT_D:def 5;
            hence thesis by WSIERP_1:15;
          end;
          reconsider r as Element of NAT by ORDINAL1:def 12;
A22:      k gcd n = p * (s gcd r) by A13,A15,PYTHTRIP:8;
          k gcd m * n = p * s gcd p * (m * r) by A13,A15
            .= p * (s gcd m * r) by PYTHTRIP:8;
          hence thesis by A2,A18,A19,A22;
        end;
      end;
    end;
  end;
  for k being Nat holds P[k] from NAT_1:sch 4(A1);
  hence thesis;
end;

theorem Th3:
  for s being real number st s > 0 ex n being Element of NAT st n >
  0 & 0 < 1/n & 1/n <= s
proof
  let s be real number;
  consider n such that
A1: n > 1/s by SEQ_4:3;
A2: 1/(1/s) = 1/s" .= s;
  assume s > 0;
  then
A3: 1/s > 0 by XREAL_1:139;
  take n;
  n > 0 by A3,A1,XXREAL_0:2;
  hence thesis by A3,A1,A2,XREAL_1:85,139;
end;

scheme
  FibInd {P[set] } : for k being Nat holds P[k]
provided
A1: P[0] and
A2: P[1] and
A3: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
  let k be Nat;
  defpred Q[Nat] means P[$1] & P[$1 + 1];
A4: for k being Nat st Q[k] holds Q[k+1]
  proof
    let k be Nat;
A5: k + 2 = (k + 1) + 1;
    assume Q[k];
    hence thesis by A3,A5;
  end;
A6: Q[0] by A1,A2;
  for k being Nat holds Q[k] from NAT_1:sch 2(A6,A4);
  hence thesis;
end;

scheme
  BinInd { P[Nat,Nat] } : for m, n being Element of NAT holds P[m, n]
provided
A1: for m, n being Element of NAT st P[m,n] holds P[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[m,n]) holds for m being Element of NAT st m <= k holds P[k,m
]
proof
  defpred Q[Nat] means for m, n st (m <= $1 & n <= $1) holds P[m,n];
A3: for k being Nat st (for r being Nat st r < k holds Q[r]) holds Q[k]
  proof
    let k be Nat;
    assume
A4: for r being Nat st r < k holds Q[r];
    let m, n;
    assume that
A5: m <= k and
A6: n <= k;
    set s = max(m,n);
A7: s <= k by A5,A6,XXREAL_0:28;
    per cases by A7,XXREAL_0:1;
    suppose
      s < k;
      then m <= s & n <= s implies P[m,n] by A4;
      hence thesis by XXREAL_0:25;
    end;
    suppose
A8:   s = k;
A9:   for m, n holds m < k & n < k implies P[m,n]
      proof
        let m, n;
        assume that
A10:    m < k and
A11:    n < k;
        set s = max(m,n);
A12:    m <= s by XXREAL_0:25;
A13:    n <= s by XXREAL_0:25;
        s < k by A10,A11,XXREAL_0:16;
        hence thesis by A4,A12,A13;
      end;
      thus thesis
      proof
        per cases by A8,XXREAL_0:16;
        suppose
          k = m;
          hence thesis by A2,A6,A9;
        end;
        suppose
          k = n;
          then P[n,m] by A2,A5,A9;
          hence thesis by A1;
        end;
      end;
    end;
  end;
A14: for k being Nat holds Q[k] from NAT_1:sch 4(A3);
  let m, n;
  set k = max(m,n);
  m <= k & n <= k implies P[m,n] by A14;
  hence thesis by XXREAL_0:30;
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
  defpred P[Nat] means Fib($1 +1) >= $1;
  0 + 1 + 1 = 2;
  then
A1: P[1] by PRE_FF:1;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
  proof
    let k be Nat;
    assume that
A3: P[k] and
A4: P[k+1];
    per cases;
    suppose
      k = 0;
      hence thesis by Lm1,Lm2,PRE_FF:1;
    end;
    suppose
      k <> 0;
      then 1 <= k by NAT_1:14;
      then
A5:   1 + (k+1) <= k + (k+1) by XREAL_1:6;
A6:   Fib((k + 2) + 1) = Fib((k+1) + 1) + Fib(k+1) by PRE_FF:1;
A7:   k + (k+1) <= Fib(k+1) + (k+1) by A3,XREAL_1:6;
      Fib(k+1) + (k+1) <= Fib((k+1)+1) + Fib(k+1) by A4,XREAL_1:6;
      then k + (k+1) <= Fib((k+2)+1) by A6,A7,XXREAL_0:2;
      hence thesis by A5,XXREAL_0:2;
    end;
  end;
A8: P[0] by PRE_FF:1;
  thus for k being Nat holds P[k] from FibInd(A8, A1, A2);
end;

Lm4: for m being Element of NAT holds Fib(m+1) >= Fib(m)
proof
  defpred P[Element of NAT] means Fib($1 + 1) >= Fib($1);
A1: for k st P[k] holds P[k+1]
  proof
    let k;
A2: Fib(k) >= 0 by NAT_1:2;
    Fib((k+1) + 1) = Fib(k+1) + Fib(k) by PRE_FF:1;
    then Fib((k+1) + 1) >= Fib(k+1) + 0 by A2,XREAL_1:6;
    hence thesis;
  end;
A3: P[0] by PRE_FF:1;
  thus for k being Element of NAT holds P[k] from NAT_1:sch 1(A3,A1);
end;

Lm5: for m, n being Element of NAT st m >= n holds Fib(m) >= Fib(n)
proof
A1: for k, n being Element of NAT holds Fib(n+k) >= Fib(n)
  proof
    defpred P[Element of NAT] means for n being Element of NAT holds Fib(n+$1)
    >= Fib(n);
A2: for k being Element of NAT st P[k] holds P[k+1]
    proof
      let k;
      assume
A3:   P[k];
      let n;
      n + (k+1) = (n+k) + 1;
      then
A4:   Fib(n + (k+1)) >= Fib(n+k) by Lm4;
      Fib(n+k) >= Fib(n) by A3;
      hence thesis by A4,XXREAL_0:2;
    end;
    let k, n be Element of NAT;
A5: P[0];
    for k holds P[k] from NAT_1:sch 1(A5, A2);
    hence thesis;
  end;
  let m, n be Element of NAT;
  assume m >= n;
  then consider k be Nat such that
A6: m = n+k by NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  m = n+k by A6;
  hence thesis by A1;
end;

Lm6: for m being Element of NAT holds Fib(m+1) <> 0
proof
  let m;
  per cases;
  suppose
    m = 0;
    hence thesis by PRE_FF:1;
  end;
  suppose
    m <> 0;
    hence thesis by Lm3,NAT_1:3;
  end;
end;

theorem Th4:
  for m, n being Nat holds Fib(m + (n + 1)) = (Fib(n) * Fib (m)) +
  (Fib(n + 1) * Fib (m + 1))
proof
  defpred P[Nat] means for n being Nat holds Fib($1 + (n + 1)) = (Fib(n) * Fib
  ($1)) + (Fib(n + 1) * Fib($1 + 1));
A1: P[0] by PRE_FF:1;
A2: now
    let k be Nat;
    assume that
A3: P[k] and
A4: P[k+1];
    thus P[k+2]
    proof
      let n be Nat;
A5:   Fib(((k+1) + 1) + (n+1)) = Fib(((k + (n + 1)) + 1) + 1)
        .= Fib(k + (n+1)) + Fib((k+1) + (n+1)) by PRE_FF:1;
      set a = Fib(n) * Fib(k), b = Fib(n+1) * Fib(k+1), c = Fib(n) * Fib(k+1),
      d = Fib(n+1) * Fib((k+1) + 1);
A6:   (a + b) + (c + d) = (a + c) + (b + d);
A7:   b + d = Fib(n+1) * (Fib(k+1) + Fib ((k+1) + 1))
        .= Fib(n+1) * Fib(((k + 1) + 1) + 1) by PRE_FF:1;
A8:   a + c = Fib(n) * (Fib(k) + Fib(k+1))
        .= Fib(n) * Fib((k+1) + 1) by PRE_FF:1;
      Fib(k + (n+1)) = Fib(n) * Fib(k) + Fib(n+1) * Fib(k+1) by A3;
      hence thesis by A4,A5,A6,A8,A7;
    end;
  end;
A9: P[1] by Lm1,PRE_FF:1;
  thus for k being Nat holds P[k] from FibInd(A1, A9, A2);
end;

Lm7: for n being Element of NAT holds Fib(n) gcd Fib(n + 1) = 1
proof
  defpred P[Element of NAT] means Fib($1) gcd Fib($1 + 1) = 1;
A1: now
    let k;
    assume
A2: P[k];
    Fib(k +1) gcd Fib((k + 1) + 1) = Fib(k +1) gcd (Fib(k + 1) + Fib(k))
    by PRE_FF:1
      .= 1 by A2,Th1;
    hence P[k+1];
  end;
A3: P[0] by NEWTON:52,PRE_FF:1;
  thus for m being Element of NAT holds P[m] from NAT_1:sch 1(A3,A1);
end;

theorem
  for m, n being Element of NAT holds Fib(m) gcd Fib(n) = Fib(m gcd n)
proof
  defpred P[Element of NAT,Element of NAT] means Fib($1) gcd Fib($2) = Fib($1
  gcd $2);
A1: for k st (for m, n st (m < k & n < k) holds P[m,n]) holds for m st m <=
  k holds P[k,m]
  proof
    let k;
    assume
A2: for m, n st m < k & n < k holds P[m,n];
    let m;
    assume
A3: m <= k;
    per cases by A3,XXREAL_0:1;
    suppose
A4:   m = k;
      hence Fib k gcd Fib m = Fib k by NAT_D:32
        .= Fib(k gcd m) by A4,NAT_D:32;
    end;
    suppose
A5:   m < k;
A6:   not m < 0 by NAT_1:2;
      thus thesis
      proof
        per cases by A6,XXREAL_0:1;
        suppose
A7:       m = 0;
          then Fib(k) gcd Fib(m) = Fib(k) by NEWTON:52,PRE_FF:1;
          hence thesis by A7,NEWTON:52;
        end;
        suppose
A8:       m > 0;
          thus thesis
          proof
            consider r be Nat such that
A9:         k = m + r by A3,NAT_1:10;
            reconsider r as Element of NAT by ORDINAL1:def 12;
A10:        r <= k by A9,NAT_1:11;
            r <> 0 by A5,A9;
            then consider rr being Nat such that
A11:        r = rr + 1 by NAT_1:6;
            reconsider rr as Element of NAT by ORDINAL1:def 12;
            Fib(k) = (Fib(rr+1) * Fib(m+1)) + (Fib (rr) * Fib(m)) by A9,A11,Th4
;
            then
A12:        Fib
(k) gcd Fib(m) = Fib(m) gcd (Fib(m+1) * Fib(r)) by A11,EULER_1:8;
            Fib(m) gcd Fib(m+1) = 1 by Lm7;
            then
A13:        Fib(k) gcd Fib(m) = Fib(m) gcd Fib(r) by A12,Th2;
            r <> k by A8,A9;
            then
A14:        r < k by A10,XXREAL_0:1;
            k gcd m = m gcd r by A9,Th1;
            hence thesis by A2,A5,A13,A14;
          end;
        end;
      end;
    end;
  end;
A15: for m, n holds P[m,n] implies P[n,m];
  thus for m, n holds P[m,n] from BinInd(A15,A1);
end;

begin

:: The relationship between the Fibonacci numbers and the
:: roots of the equation x^2 = x + 1
:: The formula for the roots of a quadratic equation

reserve x, a, b, c for real number;

theorem Th6:
  for x, a, b, c being real number 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))
proof
  let x, a, b, c;
  set lh = a * x^2 + b * x + c;
  set r1 = (- b - sqrt delta(a,b,c))/(2 * a);
  set r2 = ( - b + sqrt delta(a,b,c))/(2 * a);
  assume that
A1: a <> 0 and
A2: delta(a,b,c) >= 0;
  lh = a * (x - r1) * (x - r2) by A1,A2,QUIN_1:16;
  hence thesis by A1,A2,QUIN_1:15;
end;

:: The roots of x^2 - x - 1 = 0
:: The value of tau is approximately 1.618

definition
  func tau -> real number equals
  (1 + sqrt 5)/2;
  correctness;
end;

:: The value of tau_bar is approximately -.618

definition
  func tau_bar -> real number equals
  (1 - sqrt 5)/2;
  correctness;
end;

Lm8: tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1
proof
A1: delta(1, -1, -1) = (-1) ^2 - (4 * 1 * (-1)) by QUIN_1:def 1
    .= 5;
  then
A2: (- (-1) - sqrt delta(1, -1, -1)) / (2 * 1) = tau_bar;
A3: for x holds (x = tau or x = tau_bar) implies x^2 = x + 1
  proof
    let x;
    assume x = tau or x = tau_bar;
    then 1 * x^2 + (-1) * x + (-1) = 0 by A1,A2,Th6;
    hence thesis;
  end;
  hence tau^2 = tau + 1;
  thus thesis by A3;
end;

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

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

Lm11: sqrt 5 < 3
proof
  3 ^2 = 9;
  then sqrt 9 = 3 by SQUARE_1:22;
  hence thesis by SQUARE_1:27;
end;

1 < tau
proof
  2 < sqrt 5 by SQUARE_1:20,27;
  then 1 < sqrt 5 by XXREAL_0:2;
  then 1 + 1 < (1 + sqrt 5) by XREAL_1:8;
  then 2/2 < (1 + sqrt 5)/2 by XREAL_1:74;
  hence thesis;
end;
then

Lm12: 0 < tau by XXREAL_0:2;

Lm13: tau_bar < 0
proof
  2 < sqrt 5 by SQUARE_1:20,27;
  then not (0 + sqrt 5) <= 1 by XXREAL_0:2;
  then 0 * 2 > (1 - sqrt 5)/1 by XREAL_1:19;
  then (1 - sqrt 5)/2 < 0 * 1 by XREAL_1:113;
  hence thesis;
end;

Lm14: abs(tau_bar) < 1
proof
  sqrt 5 - 1 < 3 - 1 by Lm11,XREAL_1:9;
  then
A1: (sqrt 5 - 1)/2 < 2/2 by XREAL_1:74;
  abs(tau_bar) = -(1 - sqrt 5)/2 by Lm13,ABSVALUE:def 1
    .= (sqrt 5 - 1)/2;
  hence thesis by A1;
end;

theorem Th7:
  for n being Nat holds Fib(n) = ((tau to_power n) - (tau_bar
  to_power n))/(sqrt 5)
proof
  defpred P[Nat] means Fib($1) = ((tau to_power $1) - (tau_bar to_power $1))/(
  sqrt 5);
A1: tau_bar to_power 1 = tau_bar by POWER:25;
  tau_bar to_power 0 = 1 by POWER:24;
  then
  ((tau to_power 0) - (tau_bar to_power 0))/(sqrt 5) = (1 - 1)/(sqrt 5) by
POWER:24
    .= 0;
  then
A2: P[0] by PRE_FF:1;
A3: for k being Nat st P[k] & P[k+1] holds P[k+2]
  proof
    let k be Nat;
    assume that
A4: P[k] and
A5: P[k+1];
    set a = tau to_power k, a1 = tau_bar to_power k, b = tau to_power (k+1),
b1 = tau_bar to_power (k+1), c = tau to_power (k+2), c1 = tau_bar to_power (k+2
    );
A6: c1 = tau_bar |^ (k + 2) by POWER:41
      .= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:8
      .= (tau_bar |^ k) * (tau_bar * (tau_bar |^ 1)) by NEWTON:6
      .= (tau_bar |^ k) * (tau_bar + 1) by Lm8,NEWTON:5
      .= (tau_bar |^ k * tau_bar) + (tau_bar |^ k) * 1
      .= (tau_bar |^ (k+1)) + (tau_bar |^ k) * 1 by NEWTON:6
      .= b1 + (tau_bar |^ k) by POWER:41
      .= a1 + b1 by POWER:41;
A7: c = (tau to_power 2) * (tau to_power k) by Lm12,POWER:27
      .= (tau to_power k) * (tau + 1) by Lm8,POWER:46
      .= (tau to_power k) * tau + (tau to_power k) * 1
      .= (tau to_power k) * (tau to_power 1) + a by POWER:25
      .= a + b by Lm12,POWER:27;
    Fib(k+2) = Fib((k + 1) + 1)
      .= (a - a1)/(sqrt 5) + (b - b1)/(sqrt 5) by A4,A5,PRE_FF:1
      .= (c - c1)/(sqrt 5) by A7,A6;
    hence thesis;
  end;
  tau - tau_bar = sqrt 5;
  then ((tau to_power 1) - (tau_bar to_power 1))/(sqrt 5) = (sqrt 5)/(sqrt 5)
  by A1,POWER:25
    .= Fib(1) by Lm10,PRE_FF:1,XCMPLX_1:60;
  then
A8: P[1];
  thus for n being Nat holds P[n] from FibInd(A2, A8, A3);
end;

Lm15: for x being real number st abs(x) <= 1 holds abs(x |^ n) <= 1
proof
  let x;
  defpred P[Element of NAT] means abs(x |^ $1) <= 1;
  assume
A1: abs(x) <= 1;
A2: for k being Element of NAT st P[k] holds P[k+1]
  proof
    let k;
A3: abs(x |^ (k+1)) = abs ((x |^ k) * x) by NEWTON:6
      .= abs(x |^ k) * abs(x) by COMPLEX1:65;
    assume P[k];
    hence thesis by A1,A3,COMPLEX1:46,XREAL_1:160;
  end;
  abs(x |^ 0) = abs(1) by NEWTON:4
    .= 1 by ABSVALUE:def 1;
  then
A4: P[0];
  for k holds P[k] from NAT_1:sch 1(A4, A2);
  hence thesis;
end;

Lm16: for n holds abs((tau_bar to_power n)/(sqrt 5)) < 1
proof
  let n;
  set y = (tau_bar to_power n), z = sqrt 5;
A1: abs(y) = abs(tau_bar |^ n) by POWER:41;
A2: abs(y/z) = abs(y * z") .= abs(y) * abs(z") by COMPLEX1:65;
A3: 1/z < 1/2 by Lm9,XREAL_1:88;
  z > 0 by Lm9,XXREAL_0:2;
  then
A4: z" > 0 by XREAL_1:122;
  then abs(z") = z" by ABSVALUE:def 1;
  then
A5: abs(z") < 1 by A3,XXREAL_0:2;
  abs(z") >= 0 by A4,ABSVALUE:def 1;
  hence thesis by A1,A2,A5,Lm14,Lm15,XREAL_1:162;
end;

theorem
  for n being Element of NAT holds abs(Fib(n) - (tau to_power n)/(sqrt 5 )) < 1
proof
  let n;
  set k = Fib(n), x = (tau to_power n), y = (tau_bar to_power n), z = sqrt 5;
  k = (x - y)/z by Th7
    .= x/z - y/z;
  then abs(-(k - x/z)) < 1 by Lm16;
  hence thesis by COMPLEX1:52;
end;

reserve F, f, g, h for Real_Sequence;

theorem Th9:
  for f, g, h being Real_Sequence st g is non-zero holds (f /" g)
  (#) (g /" h) = (f /" h)
proof
  let f, g, h be Real_Sequence;
  set f3 = (f /" g), g3 = (g /" h), h3 = (f /" h);
  assume
A1: g is non-zero;
  for n holds (f3 (#) g3).n = h3.n
  proof
    let n;
    set a = f.n, b = (g.n)", c = g.n, d = (h.n)";
A2: g3.n = c * (h".n) by SEQ_1:8
      .= c * d by VALUED_1:10;
A3: h3.n = a * (h".n) by SEQ_1:8
      .= a * d by VALUED_1:10;
A4: g.n <> 0 by A1,SEQ_1:5;
A5: b * c = (1/c) * c .= 1 by A4,XCMPLX_1:106;
    f3.n = a * (g".n) by SEQ_1:8
      .= a * b by VALUED_1:10;
    then (f3 (#) g3).n = (a * b) * (c * d) by A2,SEQ_1:8
      .= ((b * c) * a) * d
      .= h3.n by A3,A5;
    hence thesis;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th10:
  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)"
proof
  let f, g;
  let n;
A1: (f /" g). n = (f.n) * (g".n) by SEQ_1:8
    .= (f.n) * (g.n)" by VALUED_1:10;
  hence (f /" g). n = (f.n) / (g.n);
  thus thesis by A1;
end;

theorem
  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
proof
  deffunc ff(Element of NAT) = (tau to_power $1)/(sqrt 5);
  let F;
  consider f such that
A1: for n holds f.n = Fib(n) from SEQ_1:sch 1;
  set f2 = f ^\ 2;
  set f1 = (f ^\ 1);
A2: f1 ^\ 1 = f ^\ (1 + 1) by NAT_1:48
    .= f2;
A3: for n holds f2.n <> 0
  proof
    let n;
    f2.n = f.(n+2) by NAT_1:def 3
      .= Fib((n+1) + 1) by A1;
    hence thesis by Lm3,NAT_1:5;
  end;
A4: for n being Nat holds (f2 /" f2) . n = 1
  proof
    let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
    then (f2 /" f2).n = (f2.n) * (f2.n)" by Th10
      .= (f2.n) * ( 1/ (f2.n))
      .= 1 by A3,A5,XCMPLX_1:106;
    hence thesis;
  end;
  then
A6: (f2 /" f2) is constant by VALUED_0:def 18;
A7: (f /" f) ^\ 2 = (f2 /" f2) by SEQM_3:20;
  then
A8: f /" f is convergent by A6,SEQ_4:21;
  (f2 /" f2) . 0 = 1 by A4;
  then lim (f2 /" f2) = 1 by A6,SEQ_4:25;
  then
A9: lim (f /" f) = 1 by A6,A7,SEQ_4:22;
  ex g st for n holds g . n = ff(n) from SEQ_1:sch 1;
  then consider g such that
A10: for n holds g.n = ff(n);
  set g1 = g ^\ 1;
A11: for n holds g.n <> 0
  proof
    let n;
A12: (sqrt 5) " <> 0 by SQUARE_1:20,27,XCMPLX_1:202;
A13: (tau |^ n) <> 0 by Lm12,PREPOWER:5;
    g.n = (tau to_power n) / (sqrt 5) by A10
      .= (tau to_power n) * (sqrt 5)"
      .= (tau |^ n) * (sqrt 5)" by POWER:41;
    hence thesis by A13,A12,XCMPLX_1:6;
  end;
  then
A14: g is non-zero by SEQ_1:5;
  then
A15: (f2 /" f1) = (f2 /" g1) (#) (g1 /" f1) by Th9;
  set g2 = g1 ^\ 1;
  for n holds f1.n <> 0
  proof
    let n;
    f1.n = f.(n+1) by NAT_1:def 3
      .= Fib(n+1) by A1;
    hence thesis by Lm6;
  end;
  then
A16: f1 is non-zero by SEQ_1:5;
  for n holds (g2 /" f2).n <> 0
  proof
    let n;
A17: (g2.n) <> 0 by A14,SEQ_1:5;
A18: (g2 /" f2).n = (g2.n) * (f2.n)" by Th10;
    (f2.n)" <> 0 by A16,A2,SEQ_1:5,XCMPLX_1:202;
    hence thesis by A17,A18,XCMPLX_1:6;
  end;
  then
A19: (g2 /" f2) is non-zero by SEQ_1:5;
  g2 = g ^\ (1 + 1) by NAT_1:48;
  then
A20: (g2 /" f2) = (g /" f) ^\ 2 by SEQM_3:20;
A21: for n holds f1.n = Fib(n+1)
  proof
    let n;
    f1.n = f.(n+1) by NAT_1:def 3
      .= Fib(n+1) by A1;
    hence thesis;
  end;
  assume
A22: for n being Element of NAT holds F.n = Fib(n+1)/Fib(n);
  for n holds F.n = (f1 /" f). n
  proof
    let n;
    (f1 /" f). n = (f1 . n) / (f . n) by Th10
      .= Fib(n+1)/ (f.n) by A21
      .= Fib(n+1)/Fib(n) by A1;
    hence thesis by A22;
  end;
  then F = f1 /" f by FUNCT_2:63;
  then
A23: (f2 /" f1) = F ^\ 1 by A2,SEQM_3:20;
A24: (g2 /" g1) = (g1 /" g) ^\ 1 by SEQM_3:20;
A25: for n being Nat holds (g1 /" g) . n = tau
  proof
    let n be Nat;
A26: n in NAT by ORDINAL1:def 12;
    then
A27: g.n = (tau to_power n) / (sqrt 5) by A10
      .= (tau to_power n) * (sqrt 5)"
      .= (tau |^ n) * (sqrt 5)" by POWER:41;
A28: g.n <> 0 by A11,A26;
    g1.n = g.(n+1) by NAT_1:def 3
      .= (tau to_power (n + 1)) / (sqrt 5) by A10
      .= (tau to_power (n+1)) * (sqrt 5)"
      .= (tau |^ (n+1)) * (sqrt 5)" by POWER:41
      .= (tau * (tau |^ n)) * (sqrt 5)" by NEWTON:6
      .= tau * (g.n) by A27;
    then (g1 /" g).n = (tau * (g.n)) * ((g.n)") by A26,Th10
      .= tau * ((g.n) * (g.n)")
      .= tau * 1 by A28,XCMPLX_0:def 7
      .= tau;
    hence thesis;
  end;
  tau in REAL by XREAL_0:def 1;
  then
A29: (g1 /" g) is constant by A25,VALUED_0:def 18;
A30: for x st 0 < x ex n st for m st n <= m holds abs ((f".m) - 0) < x
  proof
    let x;
    assume 0 < x;
    then consider k such that
A31: k > 0 and
    0 < 1/k and
A32: 1/k <= x by Th3;
    for m st (k+2) <= m holds abs((f" . m) - 0) < x
    proof
      let m;
      k + 2 = (k + 1) + 1;
      then
A33:  Fib(k+2) >= k+1 by Lm3;
      assume (k+2) <= m;
      then Fib(k+2) <= Fib(m) by Lm5;
      then k + 1 <= Fib(m) by A33,XXREAL_0:2;
      then
A34:  k + 1 <= f.m by A1;
      then 0 < f.m by NAT_1:5,XXREAL_0:2;
      then
A35:  0 <= (f.m)" by XREAL_1:122;
      k + 0 < (k+1) by XREAL_1:6;
      then
A36:  1/(k+1) < 1/k by A31,XREAL_1:88;
A37:  abs((f".m) - 0) = abs ((f.m)") by VALUED_1:10
        .= (f.m)" by A35,ABSVALUE:def 1
        .= 1/(f.m);
      1/(f.m) <= 1/(k+1) by A34,NAT_1:5,XREAL_1:85;
      then 1/(f.m) < 1/k by A36,XXREAL_0:2;
      hence thesis by A32,A37,XXREAL_0:2;
    end;
    hence thesis;
  end;
  then
A38: f" is convergent by SEQ_2:def 6;
  then
A39: lim f" = 0 by A30,SEQ_2:def 7;
  deffunc ff(Element of NAT) = (tau_bar to_power $1)/(sqrt 5);
  ex h st for n holds h . n = ff(n) from SEQ_1:sch 1;
  then consider h such that
A40: for n holds h.n = ff(n);
A41: for n holds f.n = g.n - h.n
  proof
    let n;
    f.n = Fib(n) by A1
      .= ((tau to_power n) - (tau_bar to_power n))/(sqrt 5) by Th7
      .= (tau to_power n)/(sqrt 5) - (tau_bar to_power n)/(sqrt 5)
      .= g.n - (tau_bar to_power n)/(sqrt 5) by A10
      .= g.n - h.n by A40;
    hence thesis;
  end;
  for n holds g.n = f.n + h.n
  proof
    let n;
    f.n = g.n - h.n by A41;
    hence thesis;
  end;
  then g = f + h by SEQ_1:7;
  then
A42: (g /" f) = (f /" f) + (h /" f) by SEQ_1:49;
  for n holds abs(h.n) < 1
  proof
    let n;
    h.n = (tau_bar to_power n)/(sqrt 5) by A40;
    hence thesis by Lm16;
  end;
  then
A43: h is bounded by SEQ_2:3;
  f" is convergent by A30,SEQ_2:def 6;
  then
A44: h /" f is convergent by A43,A39,SEQ_2:25;
  then
A45: (g /" f) is convergent by A8,A42,SEQ_2:5;
  (g1 /" g) . 0 = tau by A25;
  then lim (g1 /" g) = tau by A29,SEQ_4:25;
  then
A46: lim (g2 /" g1) = tau by A29,A24,SEQ_4:20;
A47: (g1 /" f1) = (g /" f) ^\ 1 by SEQM_3:20;
  lim (h /" f) = 0 by A43,A38,A39,SEQ_2:26;
  then
A48: lim (g /" f) = 1 + 0 by A44,A8,A9,A42,SEQ_2:6
    .= 1;
  then
A49: lim (g2 /" f2) = 1 by A45,A20,SEQ_4:20;
  then (g2 /" f2)" is convergent by A45,A20,A19,SEQ_2:21;
  then
A50: (f2 /" g2) is convergent by SEQ_1:40;
A51: f2 /" g1 = (f2 /" g2) (#) (g2 /" g1) by A14,Th9;
  then
A52: f2 /" g1 is convergent by A29,A50,A24,SEQ_2:14;
  then
A53: (f2 /" f1) is convergent by A45,A47,A15,SEQ_2:14;
  hence F is convergent by A23,SEQ_4:21;
  lim (g2 /" f2)" = 1" by A45,A20,A49,A19,SEQ_2:22
    .= 1;
  then lim (f2 /" g2) = 1 by SEQ_1:40;
  then
A54: lim (f2 /" g1) = 1 * tau by A29,A51,A50,A24,A46,SEQ_2:15
    .= tau;
  lim (g1 /" f1) = 1 by A45,A48,A47,SEQ_4:20;
  then lim (f2 /" f1) = tau * 1 by A45,A54,A52,A47,A15,SEQ_2:15;
  hence thesis by A53,A23,SEQ_4:22;
end;