Copyright (c) 2002 Association of Mizar Users
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;