The Mizar article:

Fibonacci Numbers

by
Robert M. Solovay

Received April 19, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: FIB_NUM
[ MML identifier index ]


environ

 vocabulary ARYTM, ARYTM_1, ARYTM_3, SQUARE_1, FUNCT_1, PRE_FF, FILTER_0,
      FUNCT_3, RELAT_1, ORDINAL2, FIB_NUM, ABSVALUE, POWER, SEQ_1, SEQ_2,
      SEQM_3, LATTICES, GROUP_1;
 notation ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, SEQ_1, NAT_1, INT_2,
      PRE_FF, SEQ_2, SEQM_3, LIMFUNC1, QUIN_1, ABSVALUE, PREPOWER, POWER;
 constructors REAL_1, NAT_1, PREPOWER, INT_2, SEQ_2, SEQM_3, PRE_FF, LIMFUNC1,
      QUIN_1, POWER, PARTFUN1, MEMBERED;
 clusters XREAL_0, SQUARE_1, QUIN_1, NEWTON, SEQ_1, RELSET_1, MEMBERED,
      ORDINAL2;
 requirements SUBSET, NUMERALS, REAL, ARITHM;
 theorems NAT_1, PRE_FF, AXIOMS, INT_2, NAT_LAT, REAL_1, SQUARE_1, CQC_THE1,
      WSIERP_1, EULER_1, PYTHTRIP, QUIN_1, REAL_2, ABSVALUE, POWER, NEWTON,
      RLVECT_1, SEQM_3, SEQ_1, SEQ_2, SEQ_4, PREPOWER, XCMPLX_0, XCMPLX_1;
 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 a,k,m, n, p,r,s for Nat;


:: Preliminary lemmas

theorem
Th1:for m, n being Nat holds m hcf n = m hcf (n + m)
proof
let m, n;
set a = m hcf n;
set b = m hcf (n + m);
A1:a divides m & a divides n by NAT_1:def 5;
   then a divides n + m by NAT_1:55;
then A2:a divides b by A1,NAT_1:def 5;
A3:b divides m & b divides n + m by NAT_1:def 5;
then b divides n by NAT_1:57;
    then b divides a by A3,NAT_1:def 5;
hence thesis by A2,NAT_1:52;
end;

theorem
Th2: for k, m, n being Nat st k hcf m = 1 holds k hcf m * n = k hcf n
proof
defpred P[Nat] means
for m, n holds $1 hcf m = 1 implies $1 hcf m * n = $1 hcf n;
A1:for k holds (for a st a < k holds P[a]) implies P[k]
proof
let k; assume
    A2: for a st a < k holds P[a];
      per cases by CQC_THE1:2;
      suppose A3:k = 0;
      let m, n; assume k hcf m = 1;
       then 1 = m by A3,NAT_LAT:36;
       hence thesis;

      suppose A4:k = 1;
      let m, n; assume k hcf m = 1;
        k hcf m * n = 1 by A4,NAT_LAT:35;
      hence thesis by A4,NAT_LAT:35;

      suppose A5:k > 1;
      let m, n; assume
      A6: k hcf m = 1; set b = k hcf m * n;
      thus thesis
          proof
          per cases by CQC_THE1:2;

          suppose b = 0;
          then 0 divides k by NAT_1:def 5;
          then k = 0 by INT_2:3;
          hence thesis by A5;

          suppose A7:b = 1; set c = k hcf n;
          A8: c divides k by NAT_1:def 5;
          A9:c divides n by NAT_1:def 5;
            n divides m * n by NAT_1:def 3;
          then c divides m * n by A9,NAT_1:51;
          then c divides 1 by A7,A8,NAT_1:def 5;
          hence thesis by A7,WSIERP_1:20;

          suppose b > 1; then b >= 1 + 1 by NAT_1:38;
          then consider p such that
             A10: p is prime and
             A11: p divides b
             by INT_2:48;

             A12: p divides k
    proof
      b divides k by NAT_1:def 5;
    hence thesis by A11,NAT_1:51;
    end;
    then consider s such that
    A13:k = p * s by NAT_1:def 3;
    A14:s < k
       proof
         p > 1 by A10,INT_2:def 5;
       then p >= 1 + 1 by NAT_1:38;
       then s * p >= s * (1 + 1) by NAT_1:20;
       then A15:k >= s * 1 + s * 1 by A13,XCMPLX_1:8;
         s <> 0 by A5,A13;
       then s > 0 by NAT_1:19;
       then s + s > s by REAL_1:69;
       then s + s >= s + 1 by NAT_1:38;
       then A16:k >= s + 1 by A15,AXIOMS:22;
         s + 1 > s by REAL_1:69;
       hence thesis by A16,AXIOMS:22;
       end;
    A17: not p divides m
    proof
       assume p divides m;
       then p divides 1 by A6,A12,NAT_1:def 5;
       then p = 1 by WSIERP_1:20;
       hence thesis by A10,INT_2:def 5;
    end;
      p divides m * n
    proof
         b divides m * n by NAT_1:def 5;
       hence thesis by A11,NAT_1:51;
    end;
    then p divides n by A10,A17,NAT_LAT:95;
then consider r such that A18: n = p * r by NAT_1:def 3;
    A19:s hcf m = 1
    proof
       set c = s hcf m;
       A20:c divides s by NAT_1:def 5;
             s divides k by A13,NAT_1:def 3;
       then A21:c divides k by A20,NAT_1:51;
             c divides m by NAT_1:def 5;
       then c divides 1 by A6,A21,NAT_1:def 5;
       hence thesis by WSIERP_1:20;
    end;
    A22: k hcf m * n = p * s hcf p * (m * r)
by A13,A18,XCMPLX_1:4
    .= p * (s hcf m * r) by PYTHTRIP:8;
      k hcf n = p * (s hcf r) by A13,A18,PYTHTRIP:8;
    hence thesis by A2,A14,A19,A22;
    end;
  end;
  for k holds P[k] from Comp_Ind(A1);
hence thesis;
end;

theorem
Th3: for s being real number st s > 0
ex n being Nat st
(n > 0 & 0 < 1/n & 1/n <= s)
proof
let s be real number;
assume s > 0;
then A1:1/s > 0 by REAL_2:127;
consider n such that
A2:n > 1/s by SEQ_4:10;
A3: n > 0 by A1,A2,AXIOMS:22;
A4: 1/(1/s) = 1/s" by XCMPLX_1:217
     .= s by XCMPLX_1:218;
take n;
thus thesis by A1,A2,A3,A4,REAL_2:127,152;
end;

scheme Fib_Ind {P[Nat] } :
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
    defpred Q[Nat] means P[$1] & P[$1 + 1];
    A4:Q[0] by A1,A2;
    A5:for k st Q[k] holds Q[k+1]
        proof
        let k;
        assume A6:Q[k];
          k + 2 = k + (1 + 1)
        .= (k + 1) + 1 by XCMPLX_1:1;
        hence thesis by A3,A6;
        end;
    A7:for k holds Q[k] from Ind(A4,A5);
    let k;
    thus thesis by A7;
    end;

scheme Bin_Ind { P[Nat,Nat] } :
for m, n  being Nat holds P[m, n]
    provided
    A1: for m, n being Nat st P[m,n] holds P[n,m] and
    A2: for k  being Nat st
        (for m, n  being Nat st (m < k & n < k) holds P[m,n])
        holds
        (for m  being 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 st (for r st r < k holds Q[r]) holds Q[k]
        proof
        let k; assume
        A4:for r st r < k holds Q[r];
        let m, n; assume
        A5: m <= k & n <= k;
        set s = max(m,n);
        A6: s <= k by A5,SQUARE_1:50;
        per cases by A6,AXIOMS:21;
        suppose s < k;
        then (m <= s & n <= s) implies P[m,n] by A4;
        hence thesis by SQUARE_1:46;
        suppose A7:s = k;

        A8:for m, n holds (m < k & n < k) implies P[m,n]
             proof
             let m, n;
             assume A9: m < k & n < k;
             set s = max(m,n);
             A10:s < k by A9,SQUARE_1:49;
             A11:m <= s by SQUARE_1:46;
                   n <= s by SQUARE_1:46;
             hence thesis by A4,A10,A11;
             end;
        thus thesis
            proof
            per cases by A7,SQUARE_1:49;
            suppose k = m;
            hence thesis by A2,A5,A8;
            suppose k = n;
            then P[n,m] by A2,A5,A8;
            hence thesis by A1;
            end;
        end;
    A12:for k holds Q[k] from Comp_Ind(A3);
    let m, n;
    set k = max(m,n);
      (m <= k & n <= k) implies P[m,n] by A12;
    hence thesis by SQUARE_1:50;
    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;
A1:P[0] by PRE_FF:1;
  0 + 1 + 1 = 2;
then A2:P[1] by PRE_FF:1;
A3:for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k;
assume that A4: P[k]
       and A5: P[k+1];
       per cases;
       suppose k = 0;
       hence thesis by Lm1,Lm2,PRE_FF:1;
       suppose k <> 0;
       then A6: 1 <= k by RLVECT_1:99;
        ((k + 1) + 1) + 1 =
       (k+ 1) + (1 + 1) by XCMPLX_1:1
       .= (k+2) + 1 by XCMPLX_1:1;
       then A7:Fib((k + 2) + 1)
       = Fib((k+1) + 1) + Fib(k+1) by PRE_FF:1;
       A8: Fib(k+1) + (k+1) <= Fib((k+1)+1) + Fib(k+1)
       by A5,AXIOMS:24;
         k + (k+1) <= Fib(k+1) + (k+1) by A4,AXIOMS:24;
       then A9:k + (k+1) <= Fib((k+2)+1) by A7,A8,AXIOMS:22;
       A10:1 + (k+1) <= k + (k+1) by A6,AXIOMS:24;
         1 + (k+1) = k + (1 + 1) by XCMPLX_1:1
       .= k + 2;
       hence thesis by A9,A10,AXIOMS:22;
end;
thus for k being Nat holds P[k] from Fib_Ind(A1, A2, A3);
end;

Lm4: for m being Nat holds Fib(m+1) >= Fib(m)
proof
   defpred P[Nat]
   means Fib($1 + 1) >= Fib($1);
   A1:P[0] by PRE_FF:1;
   A2:for k st P[k] holds P[k+1]
   proof
      let k;
      A3:Fib((k+1) + 1) = Fib(k+1) + Fib(k) by PRE_FF:1;
        Fib(k) >= 0 by NAT_1:18;
      then Fib((k+1) + 1) >= Fib(k+1) + 0 by A3,AXIOMS:24;
      hence thesis;
   end;
   thus for k being Nat holds P[k] from Ind(A1,A2);
end;

Lm5: for m, n being Nat st m >= n holds Fib(m) >= Fib(n)
proof
let m, n;
assume m >= n;
then consider k such that A1:m = n +k by NAT_1:28;
  for k , n being Nat holds Fib(n+k) >= Fib(n)
proof
defpred P[Nat] means
for n being Nat holds Fib(n+$1) >= Fib(n);
   A2:P[0];
   A3: for k being Nat st P[k] holds P[k+1]
   proof
      let k;
      assume A4:P[k];
      let n;
        n + (k+1) = (n+k) + 1 by XCMPLX_1:1;
      then A5: Fib(n + (k+1)) >= Fib(n+k) by Lm4;
        Fib(n+k) >= Fib(n) by A4;
      hence thesis by A5,AXIOMS:22;
   end;
   A6: for k holds P[k] from Ind(A2, A3);
   let k;
   let n;
   thus thesis by A6;
end;
hence thesis by A1;
end;

Lm6: for m being Nat holds Fib(m+1) <> 0
proof
let m;
per cases;
suppose m = 0;
hence thesis by PRE_FF:1;
suppose m <> 0;
then m > 0 by NAT_1:19;
hence thesis by Lm3;
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 holds
Fib($1 + (n + 1)) = (Fib(n) * Fib($1)) +
                    (Fib(n + 1) * Fib($1 + 1));
A1:P[0] by PRE_FF:1;
A2:P[1] by Lm1,PRE_FF:1;
A3:now let k;
    assume that A4:  P[k] and
                A5: P[k+1];
    A6: k + 1 + 1 = k + (1+1) by XCMPLX_1:1 .= k+2;
    thus P[k+2]
       proof let n;
          A7: Fib(((k+1) + 1) + (n+1))
             = Fib((k + (1 + 1)) + (n+1)) by XCMPLX_1:1
            .= Fib((k + (n + 1)) + (1+1)) by XCMPLX_1:1
            .= Fib(((k + (n + 1)) + 1) + 1) by XCMPLX_1:1
            .= Fib(k + (n+1)) + Fib((k + (n+1)) + 1) by PRE_FF:1
            .= Fib(k + (n+1)) + Fib((k+1) + (n+1)) by XCMPLX_1:1;

          A8: Fib(k + (n+1)) = Fib(n) * Fib(k) +
                                Fib(n+1) * Fib(k+1) by A4;

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

          A9: (a + b) + (c + d) = (a + (c + d)) + b by XCMPLX_1:1
                                .= ((a + c) + d) + b by XCMPLX_1:1
                                .= (a + c) + (b + d) by XCMPLX_1:1;

          A10: a + c = Fib(n) * (Fib(k) + Fib(k+1)) by XCMPLX_1:8
                    .= Fib(n) * Fib((k+1) + 1) by PRE_FF:1;
                 b + d = Fib(n+1) * (Fib(k+1) + Fib ((k+1) + 1)) by XCMPLX_1:8
                    .= Fib(n+1) * Fib(((k + 1) + 1) + 1) by PRE_FF:1;
               hence thesis by A5,A6,A7,A8,A9,A10;
               end;
            end;
         thus for k holds P[k] from Fib_Ind(A1, A2, A3);
         end;

Lm7: for n being Nat holds Fib(n) hcf Fib(n + 1) = 1
proof
defpred P[Nat] means
Fib($1) hcf Fib($1 + 1) = 1;
A1:P[0] by NAT_LAT:36,PRE_FF:1;
A2:now let k; assume
    A3: P[k];
    thus P[k+1]
     proof
      thus Fib(k +1) hcf Fib((k + 1) + 1)
       = Fib(k +1) hcf (Fib(k + 1) + Fib(k)) by PRE_FF:1
      .= 1 by A3,Th1;
     end;
    end;
thus for m being Nat holds P[m] from Ind(A1,A2);
end;

theorem
  for m, n being Nat holds Fib(m) hcf Fib(n) = Fib(m hcf n)
proof
defpred P[Nat,Nat] means
Fib($1) hcf Fib($2) = Fib($1 hcf $2);
A1:for m, n holds P[m,n] implies P[n,m];
A2: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
    A3:for m, n st m < k & n < k holds P[m,n]; let m; assume
    A4:m <= k;
       per cases by A4,AXIOMS:21;

       suppose m = k;
       hence thesis;

       suppose A5:m < k;
       A6: not m < 0 by NAT_1:18;
       thus thesis
       proof
       per cases by A6,AXIOMS:21;

       suppose A7:m = 0;
       then Fib(k) hcf Fib(m) = Fib(k)
       by NAT_LAT:36,PRE_FF:1;
       hence thesis by A7,NAT_LAT:36;

       suppose A8:m > 0;
       thus thesis
       proof
          consider r such that
          A9:k = m + r by A4,NAT_1:28;
            r <> 0 by A5,A9;
          then consider rr being Nat such that
          A10: r = rr + 1 by NAT_1:22;
           Fib(k) =
          (Fib(rr+1) * Fib(m+1)) + (Fib (rr) * Fib(m))
          by A9,A10,Th4;
          then A11:Fib(k) hcf Fib(m)
          = Fib(m) hcf (Fib(m+1) * Fib(r))
          by A10,EULER_1:9;
           Fib(m) hcf Fib(m+1) = 1 by Lm7;
          then A12:Fib(k) hcf Fib(m) = Fib(m) hcf Fib(r)
          by A11,Th2;
          A13:r <= k by A9,NAT_1:29;
            now assume r = k;
          then m + r = 0 + r by A9;
          hence contradiction by A8,XCMPLX_1:2;
          end;
          then A14:r < k by A13,AXIOMS:21;
            k hcf m = m hcf r by A9,Th1;
          hence thesis by A3,A5,A12,A14;
      end;
   end;
end;
thus for m, n holds P[m,n] from Bin_Ind(A1,A2);
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;
       A3:lh = a * (x - r1) * (x - r2) by A1,A2,QUIN_1:16;
         (x = r1 or x = r2) implies lh = 0
       proof
          assume A4:(x = r1 or x = r2);
          per cases by A4;

          suppose x = r1;
          then x - r1 = 0 by XCMPLX_1:14;
          hence thesis by A3;

          suppose x = r2;
          then x - r2 = 0 by XCMPLX_1:14;
          hence thesis by A3;
       end;
       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
  :Def1: (1 + sqrt 5)/2;
  correctness;
end;

:: The value of tau_bar is approximately -.618

definition
  func tau_bar -> real number equals
  :Def2: (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
       .= 1 - (-4) by SQUARE_1:59,61
       .= 5;
   then A2: (- (-1) - sqrt delta(1, -1, -1)) / (2 * 1)
        = tau_bar by Def2;
   A3:for x holds
       (1 * x ^2 + (-1) * x + (-1) = 0) implies (x^2 = x + 1)
    proof
         let x;
     A4:(1 * x^2 + (-1)* x + (-1)) =
             x^2 + ((-1) * x + (-1) * 1) by XCMPLX_1:1 .=
             x^2 + (-1) * (x + 1) by XCMPLX_1:8 .=
             x^2 + (- 1 *(x + 1)) by XCMPLX_1:175 .=
             x^2 - (x + 1) by XCMPLX_0:def 8;

          assume 1 * x ^2 + (-1) * x + (-1) = 0;
          hence thesis by A4,XCMPLX_1:15;
  end;

   A5: 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,Def1,Th6;
       hence thesis by A3;
     end;
  hence tau^2 = tau + 1;
  thus thesis by A5;
end;

Lm9: 2 < sqrt 5 by SQUARE_1:85,95;
Lm10: sqrt 5 <> 0 by SQUARE_1:85,95;

Lm11: sqrt 5 < 3
proof
       3 ^2 = 3 * 3 by SQUARE_1:def 3
          .= 9;
     then sqrt 9 = 3 by SQUARE_1:89;
     hence thesis by SQUARE_1:95;
end;

  1 < tau
proof
       2 < sqrt 5 by SQUARE_1:85,95;
     then 1 < sqrt 5 by AXIOMS:22;
     then 1 + 1 < (1 + sqrt 5) by REAL_1:67;
     then 2/2 < (1 + sqrt 5)/2 by REAL_1:73;
     hence thesis by Def1;
end;

then Lm12: 0 < tau by AXIOMS:22;

Lm13: tau_bar < 0
proof
       2 < sqrt 5 by SQUARE_1:85,95;
     then not ((0 + sqrt 5) <= 1) by AXIOMS:22;
     then 0 * 2 > (1 - sqrt 5)/1 by REAL_1:84;
     then (1 - sqrt 5)/2 < 0 * 1
     by REAL_2:193;
     hence thesis by Def2;
end;

Lm14: abs(tau_bar) < 1
proof
A1:  abs(tau_bar) = -(1 - sqrt 5)/2 by Def2,Lm13,ABSVALUE:def 1
                  .= (- (1 - sqrt 5))/2 by XCMPLX_1:188
                  .= (sqrt 5 - 1)/2 by XCMPLX_1:143;
        sqrt 5 - 1 < 3 - 1 by Lm11,REAL_1:54;
      then (sqrt 5 - 1)/2 < 2/2 by REAL_1:73;
      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: P[0]
       proof
                tau_bar to_power 0 = 1 by POWER:29;
              then ((tau to_power 0) - (tau_bar to_power 0))/(sqrt 5) =
              (1 - 1)/(sqrt 5) by POWER:29
           .= 0;
       hence thesis by PRE_FF:1;
       end;
  set a = 1 + sqrt 5; set b = 1 - sqrt 5;
  A2: P[1]
       proof
         A3: tau - tau_bar
              = (a - b)/2 by Def1,Def2,XCMPLX_1:121
              .= (a + (-b))/2 by XCMPLX_0:def 8
              .= ((1 + sqrt 5) + (sqrt 5 - 1))/2 by XCMPLX_1:143
              .= ((sqrt 5 + 1) + (-1 + sqrt 5))/2 by XCMPLX_0:def 8
              .= ((sqrt 5 + 1 + -1) + sqrt 5)/2 by XCMPLX_1:1
              .= ((sqrt 5 + (1 + -1)) + sqrt 5)/2 by XCMPLX_1:1
              .= sqrt 5 by XCMPLX_1:65;
            tau_bar to_power 1 = tau_bar by POWER:30;
               then ((tau to_power 1) - (tau_bar to_power 1))/(sqrt 5)
               = (sqrt 5)/(sqrt 5) by A3,POWER:30
              .= Fib(1) by Lm10,PRE_FF:1,XCMPLX_1:60;
          hence thesis;
       end;
  A4: for k being Nat st P[k] & P[k+1] holds P[k+2]
  proof
    let k;
    assume that
    A5: P[k] and
    A6: 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);

       A7: c = (tau to_power 2) * (tau to_power k) by Lm12,POWER:32
              .= (tau to_power k) * (tau + 1) by Lm8,POWER:53
              .= (tau to_power k) * tau + (tau to_power k) * 1
                   by XCMPLX_1:8
              .= (tau to_power k) * (tau to_power 1) + a by POWER:30
              .= a + b by Lm12,POWER:32;
       A8: c1 = tau_bar |^ (k + 2) by Lm13,POWER:46
              .= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:13
              .= (tau_bar |^ k) *
                 (tau_bar * (tau_bar |^ 1)) by NEWTON:11
              .= (tau_bar |^ k) *
                 (tau_bar * tau_bar) by NEWTON:10
              .= (tau_bar |^ k) * (tau_bar + 1) by Lm8,SQUARE_1:def 3
              .= (tau_bar |^ k * tau_bar) +
                  (tau_bar |^ k) * 1 by XCMPLX_1:8
              .= (tau_bar |^ (k+1)) + (tau_bar |^ k) * 1 by NEWTON:11
              .= b1 + (tau_bar |^ k) by Lm13,POWER:46
              .= a1 + b1 by Lm13,POWER:46;
       A9: (a - a1) + (b - b1) =
            (a + (-a1)) + (b - b1) by XCMPLX_0:def 8 .=
            (a + (-a1)) + (b + (-b1)) by XCMPLX_0:def 8 .=
            ((a + (-a1)) + b) + (-b1) by XCMPLX_1:1
            .= c + (- a1) + (- b1) by A7,XCMPLX_1:1
            .= c + ((- a1) + (- b1)) by XCMPLX_1:1
            .= c + ((-1) * a1 + (- b1)) by XCMPLX_1:180
            .= c + ((-1) * a1 + (-1) * b1) by XCMPLX_1:180
            .= c + (-1) * c1 by A8,XCMPLX_1:8
            .= c + (- c1) by XCMPLX_1:180
            .= c - c1 by XCMPLX_0:def 8;

      Fib(k+2) = Fib((k + (1 + 1)))
             .= Fib((k + 1) + 1) by XCMPLX_1:1
             .= (a - a1)/(sqrt 5) +
                (b - b1)/(sqrt 5)
                by A5,A6,PRE_FF:1
             .= (c - c1)/(sqrt 5) by A9,XCMPLX_1:63;
    hence thesis;
  end;
  thus  for n being Nat holds P[n] from Fib_Ind(A1, A2, A4);
  end;

Lm15: for x being real number st abs(x) <= 1
holds abs(x |^ n) <= 1
proof
let x;
assume A1: abs(x) <= 1;

defpred P[Nat] means
   abs(x |^ $1) <= 1;
  for k holds P[k]
proof
   A2:P[0]
   proof
     abs(x |^ 0) = abs(1) by NEWTON:9
   .= 1 by ABSVALUE:def 1;
   hence thesis;
   end;
   A3: for k being Nat st P[k] holds P[k+1]
   proof
      let k;
      assume A4: P[k];
      A5:abs(x |^ (k+1)) = abs ((x |^ k) * x) by NEWTON:11
      .= abs(x |^ k) * abs(x) by ABSVALUE:10;
      A6: 0 <= abs(x) by ABSVALUE:5;
             0 <= abs(x |^ k) by ABSVALUE:5;
      hence thesis by A1,A4,A5,A6,REAL_2:140;
   end;
   thus thesis from Ind(A2, A3);
end;
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;
      abs(y) = abs(tau_bar |^ n) by Lm13,POWER:46;
    then A1:abs(y) <=1 by Lm14,Lm15;
    A2:abs(y) >= 0 by ABSVALUE:5;
    A3:abs(y/z) = abs(y * z") by XCMPLX_0:def 9
             .= abs(y) * abs(z") by ABSVALUE:10;
      z > 0 by Lm9,AXIOMS:22;
    then A4: z" > 0 by REAL_1:72;
    then A5:abs(z") = z" by ABSVALUE:def 1;
      1/z < 1/2 by Lm9,REAL_2:151;
    then 1/z < 1 by AXIOMS:22;
    then A6:abs(z") < 1 by A5,XCMPLX_1:217;
     abs(z") >= 0 by A4,ABSVALUE:def 1;
    hence thesis by A1,A2,A3,A6,REAL_2:139;
end;

theorem
   for n being 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 by XCMPLX_1:121;
    then x/z - k = y/z by XCMPLX_1:18;
    then abs(x/z - k) < 1 by Lm16;
    then abs(-(k - x/z)) < 1 by XCMPLX_1:143;
    hence thesis by ABSVALUE:17;
end;

reserve F, G, f, g, h for Real_Sequence;

:: Preliminary facts on real sequences

theorem
Th9: for F, G being Real_Sequence st
(for n being Nat holds F.n = G.n) holds F = G
proof
   let F, G;
   assume for n being Nat holds F.n = G.n;
   then for x being set st x in NAT holds F.x = G.x;
   hence thesis by SEQ_1:8;
end;

theorem
Th10: for f, g, h being Real_Sequence st g is_not_0 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_not_0;
      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: g.n <> 0 by A1,SEQ_1:7;

      A3:f3.n = (f (#) g").n by SEQ_1:def 9
      .= a * (g".n) by SEQ_1:12
      .= a * b by SEQ_1:def 8;

      A4:g3.n = (g (#) h").n by SEQ_1:def 9
      .= c * (h".n) by SEQ_1:12
      .= c * d by SEQ_1:def 8;

      A5: h3.n = (f (#) h").n by SEQ_1:def 9
      .= a * (h".n) by SEQ_1:12
      .= a * d by SEQ_1:def 8;

      A6: b * c = (1/c) * c by XCMPLX_1:217
           .= 1 by A2,XCMPLX_1:107;

         (f3 (#) g3).n =
       (a * b) * (c * d) by A3,A4,SEQ_1:12
      .= ((a * b) * c) * d by XCMPLX_1:4
      .= ((b * c) * a) * d by XCMPLX_1:4
      .= h3.n by A5,A6;
      hence thesis;
   end;
hence thesis by Th9;
end;

theorem
Th11: for f, g being Real_Sequence for n being 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 (#) g").n by SEQ_1:def 9
       .= (f.n) * (g".n) by SEQ_1:12
       .= (f.n) * (g.n)" by SEQ_1:def 8;
   hence (f /" g). n = (f.n) / (g.n) by XCMPLX_0:def 9;
   thus thesis by A1;
end;

theorem
  for F being Real_Sequence st
(for n being Nat holds F.n = Fib(n+1)/Fib(n))
holds
 F is convergent & lim F = tau
proof
   let F;
   assume A1: for n being Nat holds F.n = Fib(n+1)/Fib(n);
   deffunc ff(Nat) = Fib($1);
     ex f st for n holds f. n = ff(n) from ExRealSeq;
   then consider f such that
   A2:for n holds f.n = ff(n);

   set f1 = (f ^\ 1);
   A3: for n holds f1.n = Fib(n+1)
   proof
      let n;
        f1.n = f.(n+1) by SEQM_3:def 9
      .= Fib(n+1) by A2;
      hence thesis;
   end;

   A4: F = f1 /" f
   proof
        for n holds F.n = (f1 /" f). n
      proof
         let n;
           (f1 /" f). n = (f1 . n) / (f . n) by Th11
         .= Fib(n+1)/ (f.n) by A3
         .= Fib(n+1)/Fib(n) by A2;
         hence thesis by A1;
      end;
      hence thesis by Th9;
   end;

   deffunc ff(Nat) = (tau to_power $1)/(sqrt 5);
     ex g st for n holds g . n = ff(n) from ExRealSeq;
   then consider g such that
   A5: for n holds g.n = ff(n);

   deffunc ff(Nat) = (tau_bar to_power $1)/(sqrt 5);
     ex h st for n holds h . n = ff(n) from ExRealSeq;
   then consider h such that
   A6: for n holds h.n = ff(n);

   A7: g = f + h
   proof
      A8: for n holds f.n = g.n - h.n
      proof
         let n;
           f.n = Fib(n) by A2
             .= ((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)
             by XCMPLX_1:121
             .= g.n - (tau_bar to_power n)/(sqrt 5) by A5
             .= g.n - h.n by A6;
          hence thesis;
      end;
        for n holds g.n = f.n + h.n
      proof
         let n;
           f.n = g.n - h.n by A8;
         hence thesis by XCMPLX_1:27;
      end;
      hence thesis by SEQ_1:11;
   end;

   A9: h /" f is convergent & lim (h /" f) = 0
   proof
      A10: h is bounded
      proof
           for n holds abs(h.n) < 1
         proof
            let n;
              h.n = (tau_bar to_power n)/(sqrt 5) by A6;
            hence thesis by Lm16;
         end;
         hence thesis by SEQ_2:15;
      end;
      A11: f" is convergent & lim f" = 0
      proof
         A12: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
         A13: k > 0 and
                0 < 1/k and
         A14: 1/k <= x by Th3;
           for m st (k+2) <= m holds abs((f" . m) - 0) < x
         proof
         let m;
         assume (k+2) <= m;
         then A15: Fib(k+2) <= Fib(m) by Lm5;
           k + 2 = k + (1 + 1)
         .= (k + 1) + 1 by XCMPLX_1:1;
          then Fib(k+2) >= k+1 by Lm3;
         then k + 1 <= Fib(m) by A15,AXIOMS:22;
         then A16: k + 1 <= f.m by A2;
           0 <> k+1 by NAT_1:21;
         then A17: 0 < k+1 by NAT_1:19;
         then A18: 1/(f.m) <= 1/(k+1)
         by A16,REAL_2:152;
           k + 0 < (k+1) by REAL_1:53;
         then A19: 1/(k+1) < 1/k by A13,REAL_2:151;
           0 < f.m by A16,A17,AXIOMS:22;
         then A20: 0 <= (f.m)" by REAL_1:72;
         A21:abs((f".m) - 0)
         = abs ((f.m)") by SEQ_1:def 8
         .= (f.m)" by A20,ABSVALUE:def 1
         .= 1/(f.m) by XCMPLX_1:217;
           1/(f.m) < 1/k by A18,A19,AXIOMS:22;
         hence thesis by A14,A21,AXIOMS:22;
         end;
         hence thesis;
         end;
         hence f" is convergent by SEQ_2:def 6;
         hence thesis by A12,SEQ_2:def 7;
      end;

      A22: h /" f = h (#) f" by SEQ_1:def 9;
      hence h /" f is convergent by A10,A11,SEQ_2:39;
      thus thesis by A10,A11,A22,SEQ_2:40;
   end;
   set f2 = f ^\ 2;
   A23: f /" f is convergent & lim (f /" f) = 1
   proof
      A24: for n holds f2.n <> 0
         proof
            let n;
            A25:f2.n = f.(n+2) by SEQM_3:def 9
            .= Fib(n + (1+1)) by A2
            .= Fib((n+1) + 1) by XCMPLX_1:1;
              (n+1) <> 0 by NAT_1:21;
            then (n+1) > 0 by NAT_1:19;
            hence thesis by A25,Lm3;
         end;

      A26: for n holds (f2 /" f2) . n = 1
         proof
            let n;
            A27: f2.n <> 0 by A24;
              (f2 /" f2).n =
              (f2.n) * (f2.n)" by Th11
            .= (f2.n) * ( 1/ (f2.n)) by XCMPLX_1:217
            .= 1 by A27,XCMPLX_1:107;
            hence thesis;
         end;
      then A28: (f2 /" f2) is constant by SEQM_3:def 6;
      then A29: (f2 /" f2) is convergent by SEQ_4:39;
        (f2 /" f2) . 0 = 1 by A26;
      then A30: lim (f2 /" f2) = 1 by A28,SEQ_4:40;
      A31: (f /" f) ^\ 2 = (f2 /" f2) by SEQM_3:43;
      hence f /" f is convergent by A29,SEQ_4:35;
      thus thesis by A29,A30,A31,SEQ_4:36;
      end;
   A32: (g /" f) = (f /" f) + (h /" f) by A7,SEQ_1:57;
   then A33: (g /" f) is convergent by A9,A23,SEQ_2:19;
   A34: lim (g /" f) = 1 + 0 by A9,A23,A32,SEQ_2:20
   .= 1;
   set g1 = g ^\ 1;
   A35: g is being_not_0
   proof
        for n holds g.n <> 0
      proof
         let n;
         A36: g.n = (tau to_power n) / (sqrt 5) by A5
                 .= (tau to_power n) * (sqrt 5)" by XCMPLX_0:def 9
                 .= (tau |^ n) * (sqrt 5)" by Lm12,POWER:46;
         A37: (tau |^ n) <> 0 by Lm12,PREPOWER:12;
           (sqrt 5) " <> 0 by Lm10,XCMPLX_1:203;
         hence thesis by A36,A37,XCMPLX_1:6;
      end;
      hence thesis by SEQ_1:7;
   end;
   A38: (g1 /" g) is convergent & lim (g1 /" g) = tau
   proof
      A39: for n holds (g1 /" g) . n = tau
      proof
         let n;
         A40: g.n = (tau to_power n) / (sqrt 5) by A5
                 .= (tau to_power n) * (sqrt 5)" by XCMPLX_0:def 9
                 .= (tau |^ n) * (sqrt 5)" by Lm12,POWER:46;
         A41: g1.n = g.(n+1) by SEQM_3:def 9
         .= (tau to_power (n + 1)) / (sqrt 5) by A5
         .= (tau to_power (n+1)) * (sqrt 5)" by XCMPLX_0:def 9
         .= (tau |^ (n+1)) * (sqrt 5)" by Lm12,POWER:46
         .= (tau * (tau |^ n)) * (sqrt 5)" by NEWTON:11
         .= tau * (g.n) by A40,XCMPLX_1:4;
         A42: g.n <> 0 by A35,SEQ_1:7;
           (g1 /" g).n = (tau * (g.n)) * ((g.n)") by A41,Th11
              .= tau * ((g.n) * (g.n)") by XCMPLX_1:4
              .= tau * 1 by A42,XCMPLX_0:def 7
              .= tau;
         hence thesis;
      end;
      then A43: (g1 /" g) is constant by SEQM_3:def 6;
      hence (g1 /" g) is convergent by SEQ_4:39;
        (g1 /" g) . 0 = tau by A39;
      hence thesis by A43,SEQ_4:40;
   end;
   A44: f1 is being_not_0
   proof
        for n holds f1.n <> 0
      proof
         let n;
           f1.n = f.(n+1) by SEQM_3:def 9
         .= Fib(n+1) by A2;
         hence thesis by Lm6;
      end;
      hence thesis by SEQ_1:7;
   end;
   A45: f2 = f1 ^\ 1
   proof
     f1 ^\ 1 = f ^\ (1 + 1) by SEQM_3:36
   .= f2;
   hence thesis;
   end;
   set g2 = g1 ^\ 1;
   A46: g1 is_not_0 & g2 is_not_0
   proof
       thus g1 is_not_0 by A35,SEQM_3:40;
       hence thesis by SEQM_3:40;
   end;
   A47:  f2 is_not_0 by A44,A45,SEQM_3:40;
   A48: f2 /" g1 is convergent & lim (f2 /" g1 ) = tau
   proof
        A49: f2 /" g1 = (f2 /" g2) (#) (g2 /" g1)
        by A46,Th10;
        A50: g2 = g ^\2
        proof
             g2 = g ^\ (1 + 1) by SEQM_3:36
             .= g ^\ 2;
           hence thesis;
        end;
        A51: (f2 /" g2) is convergent & lim (f2 /" g2) = 1
        proof
           A52: (g2 /" f2) = (g /" f) ^\ 2 by A50,SEQM_3:43;
           then A53: (g2 /" f2) is convergent by A33,SEQ_4:33;
           A54: lim (g2 /" f2) = 1 by A33,A34,A52,SEQ_4:33;
                  for n holds (g2 /" f2).n <> 0
           proof
              let n;
              A55:(g2.n) <> 0 by A46,SEQ_1:7;
                (f2.n) <> 0 by A47,SEQ_1:7;
              then A56:(f2.n)" <> 0 by XCMPLX_1:203;
                (g2 /" f2).n = (g2.n) * (f2.n)" by Th11;
              hence thesis by A55,A56,XCMPLX_1:6;
           end;
           then A57: (g2 /" f2) is_not_0 by SEQ_1:7;
           then (g2 /" f2)" is convergent by A53,A54,SEQ_2:35;
           hence (f2 /" g2) is convergent by SEQ_1:48;
              lim (g2 /" f2)" = 1" by A53,A54,A57,SEQ_2:36
           .= 1;
           hence thesis by SEQ_1:48;
        end;
        A58: (g2 /" g1) is convergent & lim (g2 /" g1) = tau
        proof
             (g2 /" g1) = (g1 /" g) ^\ 1 by SEQM_3:43;
           hence thesis by A38,SEQ_4:33;
        end;
        hence f2 /" g1 is convergent by A49,A51,SEQ_2:28;
          lim (f2 /" g1) = 1 * tau by A49,A51,A58,SEQ_2:29
        .= tau;
        hence thesis;
   end;
   A59: (g1 /" f1) is convergent & lim (g1 /" f1) = 1
   proof
        (g1 /" f1) = (g /" f) ^\ 1 by SEQM_3:43;
      hence thesis by A33,A34,SEQ_4:33;
   end;
   A60: (f2 /" f1) is convergent & lim (f2 /" f1) = tau
   proof
      A61: (f2 /" f1) = (f2 /" g1) (#) (g1 /" f1)
      by A46,Th10;
      hence (f2 /" f1) is convergent by A48,A59,SEQ_2:28;
        lim (f2 /" f1) = tau * 1 by A48,A59,A61,SEQ_2:29;
      hence thesis;
   end;
   A62: (f2 /" f1) = F ^\ 1 by A4,A45,SEQM_3:43;
   hence F is convergent by A60,SEQ_4:35;
   thus thesis by A60,A62,SEQ_4:36;
end;

Back to top