:: Fibonacci Numbers
:: by Robert M. Solovay
::
:: Received April 19, 2002
:: Copyright (c) 2002-2026 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, 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,
REAL_1;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, 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, VALUED_1, PARTFUN1, SETFAM_1, RELSET_1, BINOP_2,
RVSUM_1, COMSEQ_2, NUMBERS;
registrations RELSET_1, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, INT_1,
VALUED_0, VALUED_1, FUNCT_2, NUMBERS, SEQ_4, NAT_1, SEQ_2, ORDINAL1,
FDIFF_1;
requirements SUBSET, NUMERALS, REAL, ARITHM;
equalities 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, TARSKI;
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 Nat;
:: Preliminary lemmas
theorem Th1:
for m, n being 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 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 being Element of NAT 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 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 st s > 0
ex n being Element of NAT st n > 0 & 0 < 1/n & 1/n <= s
proof
let s be Real;
consider n being Nat such that
A1: n > 1/s by SEQ_4:3;
A2: 1/(1/s) = 1/s" .= s;
A3: n in NAT by ORDINAL1:def 12;
assume s > 0;
then
A4: 1/s > 0;
take n;
thus thesis by A4,A1,A2,XREAL_1:85,A3;
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 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 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);
A0: s is Nat by TARSKI:1;
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,A0;
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);
A0: s is Nat by TARSKI:1;
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,A0,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);
k is Nat by TARSKI:1;
then 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];
thus for k being Nat holds P[k] from FibInd(A8, A1, A2);
end;
Lm4: for m being Nat holds Fib(m+1) >= Fib(m)
proof
defpred P[Nat] means Fib($1 + 1) >= Fib($1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
Fib((k+1) + 1) = Fib(k+1) + Fib(k) by PRE_FF:1;
then Fib((k+1) + 1) >= Fib(k+1) + 0 by XREAL_1:6;
hence thesis;
end;
A2: P[0] by PRE_FF:1;
thus for k being Nat holds P[k] from NAT_1:sch 2(A2,A1);
end;
Lm5: for m, n being Nat st m >= n holds Fib(m) >= Fib(n)
proof
A1: 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: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
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;
A5: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A5, A2);
hence thesis;
end;
let m, n;
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 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 Nat holds Fib(n) gcd Fib(n + 1) = 1
proof
defpred P[Nat] means Fib($1) gcd Fib($1 + 1) = 1;
A1: now
let k be Nat;
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 Nat holds P[m] from NAT_1:sch 2(A3,A1);
end;
theorem
for m, n being Nat holds Fib(m) gcd Fib(n) = Fib(m gcd n)
proof
defpred P[Nat,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;
thus thesis
proof
per cases;
suppose
A6: m = 0;
then Fib(k) gcd Fib(m) = Fib(k) by NEWTON:52,PRE_FF:1;
hence thesis by A6,NEWTON:52;
end;
suppose
A7: m > 0;
thus thesis
proof
consider r be Nat such that
A8: k = m + r by A3,NAT_1:10;
reconsider r as Element of NAT by ORDINAL1:def 12;
A9: r <= k by A8,NAT_1:11;
r <> 0 by A5,A8;
then consider rr being Nat such that
A10: 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 A8,A10,Th4
;
then
A11: Fib
(k) gcd Fib(m) = Fib(m) gcd (Fib(m+1) * Fib(r)) by A10,EULER_1:8;
Fib(m) gcd Fib(m+1) = 1 by Lm7;
then
A12: Fib(k) gcd Fib(m) = Fib(m) gcd Fib(r) by A11,Th2;
r <> k by A7,A8;
then
A13: r < k by A9,XXREAL_0:1;
k gcd m = m gcd r by A8,Th1;
hence thesis by A2,A5,A12,A13;
end;
end;
end;
end;
end;
A14: for m, n holds P[m,n] implies P[n,m];
thus for m, n holds P[m,n] from BinInd(A14,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;
theorem Th6:
for x, a, b, c being Real 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 equals
(1 + sqrt 5)/2;
correctness;
end;
:: The value of tau_bar is approximately -.618
definition
func tau_bar -> Real 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;
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: |.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;
|.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
.= (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 st |.x.| <= 1 holds |.x |^ n.| <= 1
proof
let x;
defpred P[Nat] means |.x |^ $1.| <= 1;
assume
A1: |.x.| <= 1;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A3: |.x |^ (k+1).| = |.(x |^ k) * x.| by NEWTON:6
.= |.x |^ k.| * |.x.| by COMPLEX1:65;
assume P[k];
hence thesis by A1,A3,COMPLEX1:46,XREAL_1:160;
end;
|.x |^ 0.| = |.1.| by NEWTON:4
.= 1 by ABSVALUE:def 1;
then
A4: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A4, A2);
hence thesis;
end;
Lm16: for n holds |.(tau_bar to_power n)/(sqrt 5).| < 1
proof
let n;
set y = (tau_bar to_power n), z = sqrt 5;
A1: |.y.| = |.tau_bar |^ n.| by POWER:41;
A2: |.y/z.| = |.y * z".| .= |.y.| * |.z".| by COMPLEX1:65;
A3: 1/z < 1/2 by Lm9,XREAL_1:88;
z > 0 by Lm9;
then
A4: z" > 0;
then |.z".| = z" by ABSVALUE:def 1;
then
A5: |.z".| < 1 by A3,XXREAL_0:2;
|.z".| >= 0 by A4,ABSVALUE:def 1;
hence thesis by A1,A2,A5,Lm14,Lm15,XREAL_1:162;
end;
theorem
for n being Nat holds |.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 |.-(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 being Element of NAT holds (f3 (#) g3).n = h3.n
proof
let n be Element of NAT;
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 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(Nat) = (tau to_power $1)/(sqrt 5);
let F;
consider f such that
A1: for n being Nat 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;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
A4: for n being Nat holds (f2 /" f2) . n = jj
proof
let n be Nat;
(f2 /" f2).n = (f2.n) * (f2.n)" by Th10
.= (f2.n) * ( 1/ (f2.n))
.= 1 by A3,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 being Nat holds g . n = ff(n) from SEQ_1:sch 1;
then consider g such that
A10: for n being Nat holds g.n = ff(n);
set g1 = g ^\ 1;
A11: for n being Nat holds g.n <> 0
proof
let n be Nat;
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;
A15: (f2 /" f1) = (f2 /" g1) (#) (g1 /" f1) by Th9,A14;
set g2 = g1 ^\ 1;
for n being Nat holds f1.n <> 0
proof
let n be Nat ;
f1.n = f.(n+1) by NAT_1:def 3
.= Fib(n+1) by A1;
hence thesis by Lm6;
end;
then
A17: f1 is non-zero by SEQ_1:5;
for n being Nat holds (g2 /" f2).n <> 0
proof
let n be Nat ;
A19: (g2.n) <> 0 by A14,SEQ_1:5;
A20: (g2 /" f2).n = (g2.n) * (f2.n)" by Th10;
(f2.n)" <> 0 by A17,A2,SEQ_1:5,XCMPLX_1:202;
hence thesis by A19,A20,XCMPLX_1:6;
end;
then
A21: (g2 /" f2) is non-zero by SEQ_1:5;
g2 = g ^\ (1 + 1) by NAT_1:48;
then
A22: (g2 /" f2) = (g /" f) ^\ 2 by SEQM_3:20;
A23: 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
A24: for n being Element of NAT holds F.n = Fib(n+1)/Fib(n);
for n being Element of NAT holds F.n = (f1 /" f). n
proof
let n be Element of NAT;
(f1 /" f). n = (f1 . n) / (f . n) by Th10
.= Fib(n+1)/ (f.n) by A23
.= Fib(n+1)/Fib(n) by A1;
hence thesis by A24;
end;
then F = f1 /" f by FUNCT_2:63;
then
A25: (f2 /" f1) = F ^\ 1 by A2,SEQM_3:20;
A26: (g2 /" g1) = (g1 /" g) ^\ 1 by SEQM_3:20;
A27: for n being Nat holds (g1 /" g) . n = tau
proof
let n be Nat;
A29: g.n = (tau to_power n) / (sqrt 5) by A10
.= (tau to_power n) * (sqrt 5)"
.= (tau |^ n) * (sqrt 5)" by POWER:41;
A30: g.n <> 0 by A11;
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 A29;
then (g1 /" g).n = (tau * (g.n)) * ((g.n)") by Th10
.= tau * ((g.n) * (g.n)")
.= tau * 1 by A30,XCMPLX_0:def 7
.= tau;
hence thesis;
end;
tau in REAL by XREAL_0:def 1;
then
A31: (g1 /" g) is constant by A27,VALUED_0:def 18;
A32: for x st 0 < x
ex n being Nat st for m being Nat st n <= m holds |.(f".m) - 0.| < x
proof
let x;
assume 0 < x;
then consider k being Element of NAT such that
A33: k > 0 and
0 < 1/k and
A34: 1/k <= x by Th3;
for m being Nat st (k+2) <= m holds |.(f" . m) - 0.| < x
proof
let m be Nat;
k + 2 = (k + 1) + 1;
then
A36: 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 A36,XXREAL_0:2;
then
A37: k + 1 <= f.m by A1;
then 0 < f.m;
then
A38: 0 <= (f.m)";
k + 0 < (k+1) by XREAL_1:6;
then
A39: 1/(k+1) < 1/k by A33,XREAL_1:88;
A40: |.(f".m) - 0.| = |.(f.m)".| by VALUED_1:10
.= (f.m)" by A38,ABSVALUE:def 1
.= 1/(f.m);
1/(f.m) <= 1/(k+1) by A37,XREAL_1:85;
then 1/(f.m) < 1/k by A39,XXREAL_0:2;
hence thesis by A34,A40,XXREAL_0:2;
end;
hence thesis;
end;
then
A41: f" is convergent by SEQ_2:def 6;
then
A42: lim f" = 0 by A32,SEQ_2:def 7;
deffunc ff(Nat) = (tau_bar to_power $1)/(sqrt 5);
ex h st for n being Nat holds h . n = ff(n) from SEQ_1:sch 1;
then consider h such that
A43: for n being Nat holds h.n = ff(n);
A44: 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 A43;
hence thesis;
end;
for n being Nat holds g.n = f.n + h.n
proof
let n being Nat ;
f.n = g.n - h.n by A44;
hence thesis;
end;
then g = f + h by SEQ_1:7;
then
A46: (g /" f) = (f /" f) + (h /" f) by SEQ_1:49;
for n being Nat holds |.h.n.| < 1
proof
let n being Nat ;
h.n = (tau_bar to_power n)/(sqrt 5) by A43;
hence thesis by Lm16;
end;
then
A48: h is bounded by SEQ_2:3;
f" is convergent by A32,SEQ_2:def 6;
then
A49: h /" f is convergent by A48,A42,SEQ_2:25;
then
A50: (g /" f) is convergent by A8,A46;
(g1 /" g) . 0 = tau by A27;
then lim (g1 /" g) = tau by A31,SEQ_4:25;
then
A51: lim (g2 /" g1) = tau by A31,A26,SEQ_4:20;
A52: (g1 /" f1) = (g /" f) ^\ 1 by SEQM_3:20;
lim (h /" f) = 0 by A48,A41,A42,SEQ_2:26;
then
A53: lim (g /" f) = 1 + 0 by A49,A8,A9,A46,SEQ_2:6
.= 1;
then
A54: lim (g2 /" f2) = 1 by A50,A22,SEQ_4:20;
then (g2 /" f2)" is convergent by A50,A22,A21,SEQ_2:21;
then
A55: (f2 /" g2) is convergent by SEQ_1:40;
A56: f2 /" g1 = (f2 /" g2) (#) (g2 /" g1) by A14,Th9;
then
A57: f2 /" g1 is convergent by A31,A55,A26;
then
A58: (f2 /" f1) is convergent by A50,A52,A15;
hence F is convergent by A25,SEQ_4:21;
lim (g2 /" f2)" = 1" by A50,A22,A54,A21,SEQ_2:22
.= 1;
then lim (f2 /" g2) = 1 by SEQ_1:40;
then
A59: lim (f2 /" g1) = 1 * tau by A31,A56,A55,A26,A51,SEQ_2:15
.= tau;
lim (g1 /" f1) = 1 by A50,A53,A52,SEQ_4:20;
then lim (f2 /" f1) = tau * 1 by A50,A59,A57,A52,A15,SEQ_2:15;
hence thesis by A58,A25,SEQ_4:22;
end;