:: Some Properties of {F}ibonacci Numbers
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received May 10, 2004
:: Copyright (c) 2004-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, NAT_1, XBOOLE_0, SUBSET_1, ARYTM_1, ARYTM_3, XXREAL_0,
ABIAN, INT_1, POWER, RELAT_1, NEWTON, PREPOWER, SQUARE_1, FINSET_1,
MEMBERED, SETFAM_1, FUNCT_1, FINSEQ_1, TARSKI, TURING_1, CARD_1,
XXREAL_2, FUNCOP_1, VALUED_1, FUNCT_4, ZFMISC_1, PRE_FF, FIB_NUM, INT_2,
ORDINAL4, CARD_3, PYTHTRIP, FIB_NUM2, REAL_1, XCMPLX_0;
notations TARSKI, ORDINAL1, ENUMSET1, SUBSET_1, XBOOLE_0, SETFAM_1, CARD_1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, VALUED_1, SQUARE_1, INT_1, NAT_1,
INT_2, NAT_D, FINSET_1, MEMBERED, RELAT_1, FUNCT_1, FUNCT_2, PRE_FF,
RVSUM_1, ZFMISC_1, NEWTON, PREPOWER, POWER, XXREAL_2, ABIAN, DOMAIN_1,
FINSEQ_1, FUNCT_4, FIB_NUM, PYTHTRIP, PEPIN, TREES_4;
constructors REAL_1, NAT_D, FINSOP_1, NEWTON, PREPOWER, POWER, PRE_FF,
BINARITH, WSIERP_1, ABIAN, PEPIN, PYTHTRIP, FIB_NUM, XXREAL_2, RELSET_1,
DOMAIN_1, NUMBERS;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, MEMBERED, FINSEQ_1, NEWTON,
PREPOWER, ABIAN, NAT_2, VALUED_0, XXREAL_2, RELSET_1, XCMPLX_0;
requirements SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities SQUARE_1, FINSEQ_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1;
theorems NAT_1, PRE_FF, INT_2, SQUARE_1, WSIERP_1, PYTHTRIP, POWER, NEWTON,
PREPOWER, XCMPLX_1, NAT_2, FINSEQ_1, XBOOLE_1, RELAT_1, ORDINAL1, CARD_2,
FINSEQ_3, RVSUM_1, XBOOLE_0, FIB_NUM, TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1,
PEPIN, GRFUNC_1, FUNCT_4, FINSEQ_2, ENUMSET1, SETFAM_1, XREAL_1,
XXREAL_0, NAT_D, XXREAL_2, XREAL_0, XTUPLE_0, VALUED_1, NUMBERS;
schemes NAT_1, FIB_NUM, FUNCT_2, DOMAIN_1, BINOP_2;
begin :: Preliminaries
reserve n, k, r, m, i, j for Nat;
theorem
for n being non zero Element of NAT holds n -' 1 + 2 = n + 1
proof
let n be non zero Element of NAT;
n >= 1 by NAT_2:19;
then n -' 1 + 2 = n + 2 -' 1 by NAT_D:38
.= n + 2 - 1 by NAT_D:37;
hence thesis;
end;
theorem Th2:
for n being odd Integer holds (-1) to_power n = -1
proof
let n be odd Integer;
(-1) to_power n = -(1 to_power n) by POWER:48
.= -1 by POWER:26;
hence thesis;
end;
theorem Th3:
for n being even Integer holds (-1) to_power n = 1
proof
let n be even Integer;
(-1) to_power n = 1 to_power n by POWER:47;
hence thesis by POWER:26;
end;
theorem Th4:
for m being non zero Real, n being Integer holds
((-1) * m) to_power n = ((-1) to_power n) * (m to_power n)
proof
let m be non zero Real, n be Integer;
per cases;
suppose
A1: n is odd;
then (-m) to_power n = -(m to_power n) by POWER:48
.= (-1) * (m to_power n)
.= ((-1) to_power n) * (m to_power n) by A1,Th2;
hence thesis;
end;
suppose
A2: n is even;
then (-m) to_power n = 1 * (m to_power n) by POWER:47
.= ((-1) to_power n) * (m to_power n) by A2,Th3;
hence thesis;
end;
end;
theorem Th5:
for a being Real holds a to_power (k+m) = (a to_power k) *
(a to_power m)
proof
let a be Real;
thus a to_power (k+m) = a |^ (k+m) by POWER:41
.= a |^ k * a |^ m by NEWTON:8
.= (a to_power k) * a |^ m by POWER:41
.= (a to_power k) * (a to_power m) by POWER:41;
end;
theorem Th6:
for k being non zero Real, m being odd Integer holds k
to_power m to_power n = k to_power (m * n)
proof
let k be non zero Real, m be odd Integer;
k to_power (m * n) = k #Z (m * n) by POWER:def 2
.= k #Z m #Z n by PREPOWER:45
.= k to_power m #Z n by POWER:def 2
.= k to_power m to_power n by POWER:def 2;
hence thesis;
end;
theorem Th7:
((-1) to_power (-n)) ^2 = 1
proof
((-1) to_power (-n)) ^2 = ((-1) #Z (-n)) ^2 by POWER:def 2
.= (1 / (-1) #Z n) ^2 by PREPOWER:41
.= (1 / ((-1) #Z n)) to_power 2 by POWER:46
.= (1 / ((-1) #Z n)) |^2 by POWER:41
.= 1 / (((-1) #Z n) |^ 2) by PREPOWER:7
.= 1 / (((-1) #Z n) #Z 2) by PREPOWER:36
.= 1 / ((-1) #Z (n*2)) by PREPOWER:45
.= 1 / ((-1) |^ (2*n)) by PREPOWER:36
.= 1 / (1 |^ (2*n)) by WSIERP_1:2
.= 1 / ((1 |^2) |^ n)
.= 1 / (1 |^ n)
.= 1 / 1;
hence thesis;
end;
theorem Th8:
for a being non zero Real holds (a to_power (-k)) * (a
to_power (-m)) = a to_power (-k-m)
proof
set K = -k;
set M = -m;
let a be non zero Real;
(a to_power (-k)) *(a to_power (-m)) = (a #Z (-k)) * (a to_power (- m))
by POWER:def 2
.= (a #Z K) * (a #Z M) by POWER:def 2
.= a #Z (K+M) by PREPOWER:44
.= a to_power (-k-m) by POWER:def 2;
hence thesis;
end;
theorem Th9:
(-1) to_power (-2 * n) = 1
proof
(-1) to_power (-2 * n) = (-1) #Z ((-1) * (2 * n)) by POWER:def 2
.= ((-1) #Z (-1)) #Z (2 * n) by PREPOWER:45
.= (1 / (-1) #Z 1) #Z (2 * n) by PREPOWER:41
.= (1 / (-1)) #Z (2 * n) by PREPOWER:35
.= (-1) |^ (2 * n) by PREPOWER:36
.= 1 |^ (2 * n) by WSIERP_1:2
.= (1 |^2) |^ n
.= 1 |^ n
.= 1;
hence thesis;
end;
theorem Th10:
for a being non zero Real holds (a to_power k) * (a
to_power (-k)) = 1
proof
let a be non zero Real;
(a to_power k) * (a to_power (-k)) = (a #Z k) * (a to_power (-k)) by
POWER:def 2
.= (a #Z k) * (a #Z (-k)) by POWER:def 2
.= a #Z (k + (-k)) by PREPOWER:44
.= 1 by PREPOWER:34;
hence thesis;
end;
registration
let n be odd Integer;
cluster -n -> odd;
coherence
proof
-1 = 2 * (-1) + 1;
then reconsider e = -1 as odd Integer;
e * n is odd;
hence thesis;
end;
end;
registration
let n be even Integer;
cluster -n -> even;
coherence
proof
reconsider e = -1 as Integer;
e * n is even;
hence thesis;
end;
end;
theorem Th11:
(-1) to_power (-n) = (-1) to_power n
proof
per cases;
suppose
n is odd;
then reconsider n as odd Integer;
(-1) to_power (-n) = -1 by Th2
.= (-1) to_power n by Th2;
hence thesis;
end;
suppose
n is even;
then reconsider n as even Integer;
(-1) to_power (-n) = 1 by Th3
.= (-1) to_power n by Th3;
hence thesis;
end;
end;
theorem Th12:
for k, m, m1, n1 being Element of NAT st k divides m & k divides
n holds k divides m * m1 + n * n1
proof
let k, m, m1, n1 be Element of NAT;
assume k divides m & k divides n;
then k divides m * m1 & k divides n * n1 by NAT_D:9;
hence thesis by NAT_D:8;
end;
registration
cluster finite non empty natural-membered with_non-empty_elements for set;
existence
proof
take X = {1};
thus X is finite non empty;
thus X is natural-membered;
thus thesis;
end;
end;
registration
let f be sequence of NAT;
let A be finite natural-membered with_non-empty_elements set;
cluster f | A -> FinSubsequence-like;
coherence
proof
per cases;
suppose
A is non empty;
then reconsider A9 = A as non empty finite natural-membered
with_non-empty_elements set;
reconsider k = max A9 as Element of NAT by ORDINAL1:def 12;
A1: dom (f | A) c= A by RELAT_1:58;
dom (f | A) c= Seg k
proof
let x be object;
assume
A2: x in dom (f | A);
then reconsider x9 = x as Nat by A1;
reconsider x9 as Element of NAT by ORDINAL1:def 12;
1 <= x9 & x9 <= k by A1,A2,NAT_1:14,XXREAL_2:def 8;
hence thesis;
end;
hence thesis;
end;
suppose
A is empty;
hence thesis;
end;
end;
end;
theorem
for p being FinSubsequence holds rng Seq p c= rng p by RELAT_1:26;
definition
let f be sequence of NAT;
let A be finite with_non-empty_elements natural-membered set;
func Prefix (f, A) -> FinSequence of NAT equals
Seq (f | A);
coherence
proof
rng Seq (f | A) c= NAT by RELAT_1:def 19;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th14:
for k being Element of NAT st k <> 0 holds k + m <= n implies m < n
proof
let k be Element of NAT;
assume
A1: k <> 0;
assume
A2: k + m <= n;
per cases by A2,XXREAL_0:1;
suppose
k + m < n;
hence thesis by NAT_1:12;
end;
suppose
A3: k + m = n;
assume not m < n;
then m + k >= n + k by XREAL_1:7;
then n - n >= n + k - n by A3,XREAL_1:9;
hence contradiction by A1;
end;
end;
registration
cluster NAT -> bounded_below;
coherence;
end;
theorem Th15:
for x, y being set st 0 < i & i < j holds {[i,x], [j,y]} is FinSubsequence
proof
let x, y be set;
assume that
A1: 0 < i and
A2: i < j;
reconsider X = {[i,x],[j,y]} as Function by A2,GRFUNC_1:8;
A3: 0 + 1 <= i by A1,NAT_1:13;
now
let x be object;
assume x in {i,j};
then
A4: x = i or x = j by TARSKI:def 2;
thus x in Seg j by A2,A3,A4,FINSEQ_1:3;
end;
then dom X = {i,j} & {i,j} c= Seg j by RELAT_1:10;
hence thesis by FINSEQ_1:def 12;
end;
theorem Th16:
for x, y being set, q being FinSubsequence st i < j & q = {[i,x]
, [j,y]} holds Seq q = <*x,y*>
proof
let x, y be set, q be FinSubsequence;
assume that
A1: i < j and
A2: q = {[i,x],[j,y]};
A3: q = (i,j) --> (x,y) by A1,A2,FUNCT_4:67;
[i,x] in q by A2,TARSKI:def 2;
then
A4: i in dom q by XTUPLE_0:def 12;
[j,y] in q by A2,TARSKI:def 2;
then
A5: j in dom q by XTUPLE_0:def 12;
A6: dom q = {i,j} by A2,RELAT_1:10;
ex k be Nat st dom q c= Seg k by FINSEQ_1:def 12;
then i >= 0+1 by A4,FINSEQ_1:1;
then Seq q = q*<*i,j*> by A1,A6,FINSEQ_3:45
.= <*q.i,q.j*> by A4,A5,FINSEQ_2:125
.= <*x,q.j*> by A1,A3,FUNCT_4:63
.= <*x,y*> by A3,FUNCT_4:63;
hence thesis;
end;
registration
let n be Nat;
cluster Seg n -> with_non-empty_elements;
coherence
proof
not 0 in Seg n by FINSEQ_1:1;
hence thesis by SETFAM_1:def 8;
end;
end;
registration
let A be with_non-empty_elements set;
cluster -> with_non-empty_elements for Subset of A;
coherence
proof
let L be Subset of A;
not 0 in L;
hence thesis by SETFAM_1:def 8;
end;
end;
registration
let A be with_non-empty_elements set;
let B be set;
cluster A /\ B -> with_non-empty_elements;
coherence
proof
reconsider AB = A /\ B as Subset of A by XBOOLE_1:17;
AB is with_non-empty_elements;
hence thesis;
end;
cluster B /\ A -> with_non-empty_elements;
coherence;
end;
theorem Th17:
for k being Element of NAT, a being set st k >= 1 holds {[k, a]}
is FinSubsequence
proof
let k be Element of NAT, a be set;
reconsider H = {[k,a]} as Function;
A1: dom H = {k} by RELAT_1:9;
assume
A2: k >= 1;
dom H c= Seg k
proof
let x be object;
assume x in dom H;
then x = k by A1,TARSKI:def 1;
hence thesis by A2;
end;
hence thesis by FINSEQ_1:def 12;
end;
theorem Th18:
for i being Element of NAT, y being set, f being FinSubsequence
st f = { [1,y] } holds Shift(f,i) = { [1+i,y] }
proof
let i be Element of NAT, y be set, f be FinSubsequence;
set g = Shift(f,i);
assume
A1: f = { [1,y] };
then card f = 1 by CARD_2:42;
then card (Shift(f,i)) = 1 by VALUED_1:42;
then
A2: ex x being object st Shift(f,i) = {x} by CARD_2:42;
A3: dom f = {1} by A1,RELAT_1:9;
dom g = {1+i}
proof
hereby
let x be object;
assume x in dom g;
then x in {o+i where o is Nat : o in dom f } by VALUED_1:def 12;
then consider w being Nat such that
A4: w+i = x and
A5: w in dom f;
w = 1 by A3,A5,TARSKI:def 1;
hence x in {1+i} by A4,TARSKI:def 1;
end;
let x be object;
assume x in {1+i};
then
A6: x = 1 + i by TARSKI:def 1;
1 in dom f by A3,TARSKI:def 1;
then x in {o+i where o is Nat : o in dom f } by A6;
hence thesis by VALUED_1:def 12;
end;
then
A7: 1 + i in dom g by TARSKI:def 1;
1 in dom f by A3,TARSKI:def 1;
then g.(1+i) = f.1 by VALUED_1:def 12
.= y by A1,GRFUNC_1:6;
then [1+i,y] in g by A7,FUNCT_1:def 2;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th19:
for q being FinSubsequence, k, n being Element of NAT st dom q
c= Seg k & n > k ex p being FinSequence st q c= p & dom p = Seg n
proof
let q be FinSubsequence, k, n be Element of NAT;
assume that
A1: dom q c= Seg k and
A2: n > k;
reconsider IK = id Seg n as Function;
set IS = IK +* q;
A3: Seg k c= Seg n by A2,FINSEQ_1:5;
A4: dom IS = dom IK \/ dom q by FUNCT_4:def 1
.= Seg n \/ dom q
.= Seg n by A1,A3,XBOOLE_1:1,12;
then reconsider IS as FinSequence by FINSEQ_1:def 2;
q c= IS by FUNCT_4:25;
hence thesis by A4;
end;
theorem Th20:
for q being FinSubsequence holds ex p being FinSequence st q c= p
proof
let q be FinSubsequence;
consider k being Nat such that
A1: dom q c= Seg k by FINSEQ_1:def 12;
reconsider IK = id Seg k as Function;
set IS = IK +* q;
dom IS = dom IK \/ dom q by FUNCT_4:def 1
.= Seg k \/ dom q
.= Seg k by A1,XBOOLE_1:12;
then reconsider IS as FinSequence by FINSEQ_1:def 2;
q c= IS by FUNCT_4:25;
hence thesis;
end;
begin :: Fibonacci Numbers
scheme
FibInd1 {P[set] } : for k being non zero Nat holds P[k]
provided
A1: P[1] and
A2: P[2] and
A3: for k being non zero Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be non zero Nat;
defpred Q[Nat] means P[$1] & P[$1 + 1];
A4: for k being non zero Nat st Q[k] holds Q[k+1]
proof
let k be non zero Nat;
A5: k + 2 = (k + 1) + 1;
assume Q[k];
hence thesis by A3,A5;
end;
A6: Q[1] by A1,A2;
for k being non zero Nat holds Q[k] from NAT_1:sch 10(A6,A4);
hence thesis;
end;
scheme
FibInd2 {P[set] } : for k be non trivial Nat holds P[k]
provided
A1: P[2] and
A2: P[3] and
A3: for k be non trivial Nat st P[k] & P[k+1] holds P[k+2]
proof
defpred Q[Nat] means P[$1+1] & P[$1+2];
A4: for k being non zero Nat st Q[k] holds Q[k+1]
proof
let k be non zero Nat;
k+1 <> 0 + 1;
then
A5: k+1 is non trivial Nat by NAT_2:def 1;
assume
A6: Q[k];
then P[k+1+1];
hence thesis by A3,A5,A6;
end;
let k be non trivial Nat;
k <> 1 by NAT_2:def 1;
then
A7: k > 1 by NAT_2:19;
then k - 1 > 1 - 1 by XREAL_1:9;
then
A8: k - 1 > 0;
A9: Q[1] by A1,A2;
A10: for k being non zero Nat holds Q[k] from NAT_1:sch 10(A9,A4);
k -' 1 + 1 = k by A7,XREAL_1:235;
hence thesis by A10,A8;
end;
theorem Th21:
Fib (2) = 1
proof
Fib (2) = Fib (0+1+1) .= 1 by PRE_FF:1;
hence thesis;
end;
theorem Th22:
Fib (3) = 2
proof
Fib (3) = Fib (1+1+1) .= 2 by Th21,PRE_FF:1;
hence thesis;
end;
theorem Th23:
Fib (4) = 3
proof
Fib (4) = Fib (2 + 1 + 1) .= 3 by Th21,Th22,PRE_FF:1;
hence thesis;
end;
theorem Th24:
for n being Nat holds Fib (n + 2) = Fib (n) + Fib (n + 1)
proof
defpred P[Nat] means Fib($1 + 2) = Fib($1) + Fib($1 + 1);
let n be Nat;
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume P[k];
assume P[k+1];
Fib (k+2+2) = Fib ((k+2+1)+1) .= Fib (k+2) + Fib (k+2+1) by PRE_FF:1;
hence thesis;
end;
Fib (0+2) = Fib (0+1+1) .= Fib (0) + Fib (1) by PRE_FF:1;
then
A2: P[0];
A3: P[1] by PRE_FF:1;
for n being Nat holds P[n] from FIB_NUM:sch 1(A2,A3,A1);
hence thesis;
end;
theorem Th25:
for n being Nat holds Fib (n + 3) = Fib (n + 2) + Fib (n + 1)
proof
let n be Nat;
Fib (n+3) = Fib ((n+1)+2) .= Fib (n+1+1) + Fib (n+1) by Th24
.= Fib (n+2) + Fib (n+1);
hence thesis;
end;
theorem Th26:
Fib (n + 4) = Fib (n + 2) + Fib (n + 3)
proof
Fib (n + 4) = Fib (n + 2 + 1 + 1)
.= Fib (n + 2) + Fib (n + 2 + 1) by PRE_FF:1;
hence thesis;
end;
theorem Th27:
Fib (n + 5) = Fib (n + 3) + Fib (n + 4)
proof
Fib (n + 5) = Fib (n + 3 + 1 + 1)
.= Fib (n + 3) + Fib (n + 3 + 1) by PRE_FF:1;
hence thesis;
end;
Lm1: for k being Nat holds Fib (2 * (k + 2) + 1) = Fib (2 * k + 3) + Fib (2 *
k + 4)
proof
let k be Nat;
Fib (2 * (k + 2) + 1) = Fib (2 * k + 2 + 1) + Fib (2 * k + 2 + 1 + 1) by
PRE_FF:1
.= Fib (2 * k + 3) + Fib (2 * k + 4);
hence thesis;
end;
theorem Th28:
Fib (n + 2) = Fib (n + 3) - Fib (n + 1)
proof
Fib (n + 3) = Fib (n + 1 + 1 + 1) .= Fib (n + 1) + Fib (n + 2) by PRE_FF:1;
hence thesis;
end;
theorem Th29:
for n being Nat holds Fib (n + 1) = Fib (n + 2) - Fib (n)
proof
let n be Nat;
Fib (n+2) - Fib (n) = Fib (n+1+1) - Fib (n)
.= Fib (n) + Fib (n+1) - Fib (n) by PRE_FF:1
.= Fib (n+1);
hence thesis;
end;
theorem Th30:
Fib (n) = Fib (n+2) - Fib (n+1)
proof
Fib (n+2) - Fib (n+1) = Fib (n) + Fib (n+1) - Fib (n+1) by Th24
.= Fib (n);
hence thesis;
end;
begin :: Cassini's and Catalan's Identities
theorem Th31:
Fib (n) * Fib (n+2) - (Fib (n+1)) ^2 = (-1) |^ (n+1)
proof
defpred P[Nat] means Fib ($1) * Fib ($1+2) - (Fib ($1+1)) ^2 = (-1) |^ ($1+1
);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A2: Fib (k+2) - Fib (k+1) = Fib (k+1) + Fib (k) - Fib (k+1) by Th24
.= Fib (k);
A3: Fib (k+3) - Fib (k+1) = Fib (k+2) + Fib (k+1) - Fib (k+1) by Th25
.= Fib (k+2);
assume P[k];
then (-1) |^ (k+1+1) = (-1) * (Fib (k) * Fib (k+2) - (Fib (k+1)) ^2) by
NEWTON:6
.= Fib (k+1) * Fib ((k+1)+2) - ( Fib ((k+1)+1)) ^2 by A2,A3;
hence thesis;
end;
A4: P[0] by PRE_FF:1;
for n being Nat holds P[n] from NAT_1:sch 2(A4, A1);
hence thesis;
end;
theorem
for n being non zero Element of NAT holds Fib (n-'1) * Fib (n+1) - (
Fib (n)) ^2 = (-1) |^n
proof
let n be non zero Element of NAT;
set a = n-'1;
A1: n >= 1 by NAT_2:19;
then n = a + 1 by XREAL_1:235;
then
Fib (n-'1) * Fib (n+1) - (Fib (n)) ^2 = Fib (a) * Fib (a+2) - (Fib (a+1) ) ^2
.= (-1) |^(n-'1+1) by Th31
.= (-1) |^(n) by A1,XREAL_1:235;
hence thesis;
end;
theorem Th33:
tau > 0
proof
sqrt 5 > 0 by SQUARE_1:25;
hence thesis by FIB_NUM:def 1;
end;
theorem Th34:
tau_bar = (- tau) to_power (-1)
proof
A1: 1 - sqrt 5 <> 0 by SQUARE_1:20,27;
(- tau) to_power (-1) = ((- 1 - sqrt 5) / 2) #Z (-1) by FIB_NUM:def 1
,POWER:def 2
.= 1 / ((- 1 - sqrt 5) / 2) #Z 1 by PREPOWER:41
.= 1 / ((- 1 - sqrt 5) / 2) by PREPOWER:35
.= 2 / (-(1 + sqrt 5)) by XCMPLX_1:57
.= -2 / (1 + sqrt 5) by XCMPLX_1:188
.= (-2) / (1 + sqrt 5) by XCMPLX_1:187
.= ((-2) * (1 - sqrt 5)) / ((1 + sqrt 5) * (1 - sqrt 5)) by A1,XCMPLX_1:91
.= ((-2) * (1 - sqrt 5)) / (1 ^2 - (sqrt 5) ^2)
.= ((-2) * (1 - sqrt 5)) / (1 - 5) by SQUARE_1:def 2
.= tau_bar by FIB_NUM:def 2;
hence thesis;
end;
theorem Th35:
(-tau) to_power ((-1) * n) = (-tau) to_power (-1) to_power n
proof
(- tau) to_power ((-1) * n) = (- tau) #Z ((-1) * n) by POWER:def 2
.= ((- tau) #Z (-1)) #Z n by PREPOWER:45
.= (1 / (- tau) #Z 1) #Z n by PREPOWER:41
.= (1 / (- tau)) #Z n by PREPOWER:35
.= (1 / (- tau)) to_power n by POWER:def 2
.= ((1 / (- tau)) to_power 1) to_power n by POWER:25
.= ((1 / (- tau)) #Z 1) to_power n by POWER:def 2
.= (1 / (- tau) #Z 1) to_power n by PREPOWER:42
.= ((- tau) #Z (-1)) to_power n by PREPOWER:41;
hence thesis by POWER:def 2;
end;
theorem Th36:
- 1 / tau = tau_bar
proof
A1: 1 - sqrt 5 <> 0 by SQUARE_1:20,27;
- 1 / tau = -1 * (2 / (1 + sqrt 5)) by FIB_NUM:def 1,XCMPLX_1:57
.= -1 * ((2 * (1 - sqrt 5)) / ((1 + sqrt 5) * (1 - sqrt 5))) by A1,
XCMPLX_1:91
.= -1 * ((2 * (1 - sqrt 5)) / (1 - (sqrt 5) ^2))
.= -1 * ((2 * (1 - sqrt 5)) / (1 - 5)) by SQUARE_1:def 2
.= (1 - sqrt 5) / 2;
hence thesis by FIB_NUM:def 2;
end;
theorem Th37:
(tau to_power r) ^2 - 2 * ((-1) to_power r) + (tau to_power (-r)
) ^2 = ((tau to_power r) - (tau_bar to_power r)) ^2
proof
(-1) / tau < 0 by Th33;
then -1 / tau < 0 by XCMPLX_1:187;
then
A1: 1 / tau > -(0 qua Nat);
((tau to_power r) - (tau_bar to_power r)) ^2 = (tau to_power r) ^2 - 2 *
(tau to_power r) * ((-1 / tau) to_power r) + ((-1 / tau) to_power r) ^2 by Th36
.= (tau to_power r) ^2 - 2 * (tau to_power r) * (((-1) * (1 / tau)) #Z r
) + ((-1 / tau) to_power r) ^2 by POWER:def 2
.= (tau to_power r) ^2 - 2 * (tau to_power r) * (((-1) #Z r) * ((1 / tau
) #Z r)) + ((-1 / tau) to_power r) ^2 by PREPOWER:40
.= (tau to_power r) ^2 - 2 * (tau to_power r) * (((1 / tau) |^ r) * ((-1
) #Z r)) + ((-1 / tau) to_power r) ^2 by PREPOWER:36
.= (tau to_power r) ^2 - 2 * (tau |^ r) * (((1 / tau) |^ r) * ((-1) #Z r
)) + ((-1 / tau) to_power r) ^2 by POWER:41
.= (tau to_power r) ^2 - 2 * ((tau |^ r) * ((1 / tau) |^ r)) * ((-1) #Z
r) + ((-1 / tau) to_power r) ^2
.= (tau to_power r) ^2 - 2 * ((tau * (1 / tau))|^ r) * ((-1) #Z r) + ((-
1 / tau) to_power r) ^2 by NEWTON:7
.= (tau to_power r) ^2 - 2 * (1 |^ r) * ((-1) #Z r) + ((-1 / tau)
to_power r) ^2 by Th33,XCMPLX_1:106
.= (tau to_power r) ^2 - 2 * 1 * ((-1) #Z r) + ((-1 / tau) to_power r)
^2
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + ((-1 / tau) to_power r)
^2 by POWER:def 2
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + ((-1 / tau) #Z r) ^2 by
POWER:def 2
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + (((-1 / tau) * (-1 /
tau)) #Z r) by PREPOWER:40
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + (((-1 / tau) ^2) |^ r)
by PREPOWER:36
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + (((1 / tau) ^2)
to_power r) by POWER:41
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + ((1 / tau) to_power r)
^2 by A1,POWER:30
.= (tau to_power r) ^2 - 2 * ((-1) to_power r) + (tau to_power (-r)) ^2
by Th33,POWER:32;
hence thesis;
end;
theorem
for n,r being non zero Element of NAT st r <= n holds (Fib (n)) ^2 -
Fib (n+r) * Fib (n-'r) = ((-1) |^(n-'r)) * (Fib (r)) ^2
proof
set T = tau;
set S = 1 / (sqrt 5);
reconsider T as non zero Real by Th33;
let n,r be non zero Element of NAT such that
A1: r <= n;
set Y = n -' r;
set X = n + r;
A2: X + Y = r + n + (n - r) by A1,XREAL_1:233
.= (r + n + n) - r
.= r + 2 * n -' r by NAT_1:12,XREAL_1:233
.= r -' r + 2 * n by NAT_D:38
.= 0 + 2 * n by XREAL_1:232
.= 2 * n;
A3: X - Y = n + r - (n - r) by A1,XREAL_1:233
.= 2 * r;
set tyu = T to_power (-Y);
set txu = T to_power (-X);
set tnu = T to_power (-n);
set ty = T to_power Y;
set tx = T to_power X;
set tn = T to_power n;
A4: -T <> 0 & - 1 = 2 * (-1) + 1;
(Fib (n)) ^2 - Fib (X) * Fib (Y) = ((tn - (tau_bar to_power n)) / (sqrt
5)) ^2 -Fib (X) * Fib (Y) by FIB_NUM:7
.= ((tn - (tau_bar to_power n)) / (sqrt 5)) ^2 - ((tx - (tau_bar
to_power X)) / (sqrt 5)) * (Fib (Y)) by FIB_NUM:7
.= ((tn - (tau_bar to_power n)) / (sqrt 5)) ^2 - ((tx - (tau_bar
to_power X)) / (sqrt 5)) * ((ty - (tau_bar to_power Y)) / (sqrt 5)) by
FIB_NUM:7
.= ((tn - (tau_bar to_power n)) * S) ^2 - ((tx - (tau_bar to_power X)) /
(sqrt 5)) * ((ty - (tau_bar to_power Y)) / (sqrt 5)) by XCMPLX_1:99
.= ((tn - (tau_bar to_power n)) * S) ^2 - ((tx - (tau_bar to_power X)) *
S) * ((ty - (tau_bar to_power Y)) / (sqrt 5)) by XCMPLX_1:99
.= ((tn - (tau_bar to_power n)) * S) ^2 - ((tx - (tau_bar to_power X)) *
S) * ((ty - (tau_bar to_power Y)) * S) by XCMPLX_1:99
.= (S ^2) * ((tn) ^2 - 2 * (tn) * ((-T) to_power (-1) to_power n) + ((-T
) to_power (-1) to_power n) ^2 - (tx - ((-T) to_power (-1) to_power X)) * (ty -
((-T) to_power (-1) to_power Y))) by Th34
.= (S ^2) * ((tn) ^2 - 2 * (tn) * ((-T) to_power ((-1) * n)) + ((-T)
to_power (-1) to_power n) ^2 - (tx - ((-T) to_power (-1) to_power X)) * (ty - (
(-T) to_power (-1) to_power Y))) by A4,Th6
.= (S ^2) * ((tn) ^2 - 2 * tn * ((-T) to_power (- n)) + ((-T) to_power (
(-1) * n)) ^2 - (tx - ((-T) to_power (-1) to_power X)) * (ty - ((-T) to_power (
-1) to_power Y))) by A4,Th6
.= (S ^2) * (tn ^2 - 2 * tn * ((-T) to_power (- n)) + ((-T) to_power (-
n)) ^2 - (tx - ((-T) to_power ((-1) * X))) * (ty - ((-T) to_power (-1) to_power
Y))) by Th35
.= (S ^2) * (tn ^2 - 2 * tn * ((-T) to_power (- n)) + ((-T) to_power (-
n)) ^2 - (tx - ((-T) to_power (- X))) * (ty - ((-T) to_power ((-1) * Y))))
by Th35
.= (S ^2) * ((tn) ^2 - 2 * tn * (((-1) * T) to_power (-n)) + (((-1) * T)
to_power (-n)) ^2 - tx * ty + tx * (((-1) * T) to_power (-Y)) + (((-1) * T)
to_power (-X)) * ty - (((-1) * T) to_power (-X)) * (((-1) * T) to_power (-Y)))
.= (S ^2) * (tn ^2 - 2 * tn * (((-1) * T) to_power (-n)) + (((-1) * T)
to_power (-n)) ^2 - tx * ty + tx * (((-1) * T) to_power (-Y)) + (((-1) * T)
to_power (-X)) * ty - (((-1) * T) to_power (-X)) * (((-1) to_power (-Y)) * tyu)
) by Th4
.= (S ^2) * ((tn) ^2 - 2 * tn * (((-1) to_power (-n)) * tnu) + (((-1) *
T) to_power (-n)) ^2 - tx * ty + tx * (((-1) * T) to_power (-Y)) + (((-1) * T)
to_power (-X)) * ty - (((-1) * T) to_power (-X)) * (((-1) to_power (-Y)) * tyu)
) by Th4
.= (S ^2) * (tn ^2 - 2 * tn * (((-1) to_power (-n)) * tnu) + (((-1)
to_power (-n)) * tnu) ^2 - tx * ty + tx * (((-1) * T) to_power (-Y)) + (((-1) *
T) to_power (-X)) * ty - (((-1) * T) to_power (-X)) * (((-1) to_power (-Y)) *
tyu)) by Th4
.= (S ^2) * (tn ^2 - 2 * tn * (((-1) to_power (-n)) * tnu) + (((-1)
to_power (-n)) * tnu) ^2 - tx * ty + tx * (((-1) to_power (-Y)) * tyu) + (((-1)
* T) to_power (-X)) * ty - (((-1) * T) to_power (-X)) * (((-1) to_power (-Y)) *
tyu)) by Th4
.= (S ^2) * (tn ^2 - 2 * tn * (((-1) to_power (-n)) * tnu) + (((-1)
to_power (-n)) * tnu) ^2 - tx * ty + tx * (((-1) to_power (-Y)) * tyu) + (((-1)
to_power (-X)) * txu) * ty - (((-1) * T) to_power (-X)) * (((-1) to_power (-Y))
* tyu)) by Th4
.= (S ^2) * (tn ^2 - 2 * tn * (((-1) to_power (-n)) * tnu) + (((-1)
to_power (-n)) * tnu) ^2 - tx * ty + tx * (((-1) to_power (-Y)) * tyu) + (((-1)
to_power (-X)) * txu) * ty - (((-1) to_power (-X)) * txu) * (((-1) to_power (-Y
)) * tyu)) by Th4
.= (S ^2) * ((tn) ^2 - 2 * (tn * tnu) * ((-1) to_power (-n)) + ((-1)
to_power (-n)) ^2 * tnu ^2 - tx * ty + tx * ((-1) to_power (-Y)) * tyu + ((-1)
to_power (-X)) * txu * ty - (((-1) to_power (-X)) * txu * ((-1) to_power (-Y)))
* tyu)
.= (S ^2) * ((tn) ^2 - 2 * 1 * ((-1) to_power (-n)) + ((-1) to_power (-n
)) ^2 * tnu ^2 - tx * ty + tx * ((-1) to_power (-Y)) * tyu + ((-1) to_power (-X
)) * txu * ty - (((-1) to_power (-X)) * txu * ((-1) to_power (-Y))) * tyu)
by Th10
.= (S ^2) * (tn ^2 - 2 * ((-1) to_power (-n)) + 1 * tnu ^2 - tx * ty +
tx * tyu * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * txu * ty - (((-1)
to_power (-X)) * ((-1) to_power (-Y)) * txu) * tyu) by Th7
.= (S ^2) * ((tn) ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - tx * ty + tx
* (1 / ty) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * txu * ty - (((-1)
to_power (-X)) * ((-1) to_power (-Y)) * txu) * tyu) by Th33,POWER:28
.= (S ^2) * ((tn) ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - tx * ty + (tx
/ ty) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * txu * ty - (((-1)
to_power (-X)) * ((-1) to_power (-Y)) * txu) * tyu) by XCMPLX_1:99
.= (S ^2) * (tn ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - tx * ty + (T
to_power (X-Y)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * txu * ty - (((-
1) to_power (-X)) * ((-1) to_power (-Y)) * txu) * tyu) by Th33,POWER:29
.= (S ^2) * ((tn) ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (
X+Y)) + (T to_power (X-Y)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * (ty
* txu) - (((-1) to_power (-X)) * ((-1) to_power (-Y))) * (txu * tyu)) by Th33,
POWER:27
.= (S ^2) * (tn ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (X+
Y)) + (T to_power (X-Y)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * (ty *
(1 / tx)) - (((-1) to_power (-X)) * ((-1) to_power (-Y))) * (txu * tyu)) by
Th33,POWER:28
.= (S ^2) * (tn ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (X+
Y)) + (T to_power (X-Y)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * (ty /
tx) - (((-1) to_power (-X)) * ((-1) to_power (-Y))) * ((txu) * (tyu))) by
XCMPLX_1:99
.= (S ^2) * (tn ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (X+
Y)) + (T to_power (X-Y)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * (T
to_power (Y-X)) - (((-1) to_power (-X)) * ((-1) to_power (-Y))) * (txu * tyu))
by Th33,POWER:29
.= (S ^2) * (tn ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (X+
Y)) + (T to_power (X-Y)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) * (T
to_power (Y-X)) - ((-1) to_power (-X-Y)) * (txu * tyu)) by Th8
.= (S ^2) * ((tn) ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (
2 * n)) + (T to_power (2 * r)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) *
(T to_power (-2 * r)) - ((-1) to_power (-2 * n)) * (T to_power (-2 * n))) by A2
,Th8
.= (S ^2) * ((tn) ^2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T to_power (
2 * n)) + (T to_power (2 * r)) * ((-1) to_power (-Y)) + ((-1) to_power (-X)) *
(T to_power (-2 * r)) - 1 * (T to_power (-2 * n))) by Th9
.= (S ^2) * (tn to_power 2 - 2 * ((-1) to_power (-n)) + tnu ^2 - (T
to_power (2 * n)) + (T to_power (2 * r)) * ((-1) to_power (-Y)) + ((-1)
to_power (-X)) * (T to_power (-2 * r)) - 1 * (T to_power (-2 * n))) by POWER:46
.= (S ^2) * (T to_power (2 * n) - 2 * ((-1) to_power (-n)) + tnu ^2 - (T
to_power (2 * n)) + (T to_power (2 * r)) * ((-1) to_power (-Y)) + ((-1)
to_power (-X)) * (T to_power (-2 * r)) - (T to_power (-2 * n))) by Th33,
POWER:33
.= (S ^2) * (T to_power (2 * n) - 2 * ((-1) to_power n) + tnu ^2 - (T
to_power (2 * n)) + (T to_power (2 * r)) * ((-1) to_power (-Y)) + ((-1)
to_power (-X)) * (T to_power (-2 * r)) - (T to_power (-2 * n))) by Th11
.= (S ^2) * (T to_power (2 * n) - (T to_power (2 * n)) - 2 * ((-1)
to_power n) + (tnu) ^2 + (T to_power (2 * r)) * ((-1) to_power Y) + ((-1)
to_power (-X)) * (T to_power (-2 * r)) - (T to_power (-2 * n))) by Th11
.= (S ^2) * (- 2 * ((-1) to_power n) + tnu ^2 + (T to_power (2 * r)) * (
(-1) to_power Y) + ((-1) to_power X) * (T to_power (-2 * r)) - (T to_power (2 *
(-n)))) by Th11
.= (S ^2) * (- 2 * ((-1) to_power n) + tnu ^2 + (T to_power (2 * r)) * (
(-1) to_power Y) + ((-1) to_power X) * (T to_power (-2 * r)) - (T to_power (-n)
to_power 2)) by Th33,POWER:33
.= (S ^2) * (- 2 * ((-1) to_power n) + (T to_power (2 * r)) * ((-1)
to_power Y) + ((-1) to_power X) * (T to_power (-2 * r)) + (tnu) ^2 - tnu ^2)
by POWER:46
.= (S ^2) * (-2 * ((-1) to_power (n-'r+r)) + ((-1) to_power Y) * (T
to_power (2 * r)) + ((-1) to_power (2 * r + Y)) * (T to_power (-2 * r))) by A3
.= (S ^2) * (- 2 * (((-1) to_power r) * ((-1) to_power (n -' r))) + ((-1
) to_power Y) * (T to_power (2 * r)) + ((-1) to_power (2 * r + Y)) * (T
to_power (-2 * r))) by Th5
.= (S ^2) * (- 2 * (((-1) to_power r) * ((-1) to_power (n -' r))) + ((-1
) to_power (n-'r)) * (T to_power (2 * r)) + (((-1) to_power (2 * r)) * ((-1)
to_power (n -'r))) * (T to_power (-2 * r))) by Th5
.= (S ^2) * (-2 * (((-1) to_power r)) + T to_power (2 * r) + T to_power
(-2 * r) * ((-1) to_power (2 * r))) * ((-1) to_power (n-'r))
.= (S ^2) * (-2 * (((-1) to_power r)) + T to_power (2 * r) + T to_power
(-2 * r) * 1) * ((-1) to_power (n-'r)) by Th3
.= (S ^2) * (T to_power (2 * r) - 2 * ((-1) to_power r) + T to_power (2
* (-r))) * ((-1) to_power (n-'r))
.= (S ^2) * (T to_power r to_power 2 - 2 * ((-1) to_power r) + T
to_power ((-r) * 2)) * ((-1) to_power (n-'r)) by Th33,POWER:33
.= (S ^2) * ((T to_power r) ^2 - 2 * ((-1) to_power r) + T to_power ((-r
) * 2)) * ((-1) to_power (n-'r)) by POWER:46
.= ((-1) to_power (n-'r)) * ((S^2) * ((T to_power r) ^2 - 2 * ((-1)
to_power r) + T to_power (-r) to_power 2)) by Th33,POWER:33
.= ((-1) to_power (n-'r)) * ((S^2) * ((T to_power r) ^2 - 2 * ((-1)
to_power r) + (T to_power (-r)) ^2)) by POWER:46
.= ((-1) to_power (n-'r)) * ((S^2) * (((tau to_power r) - (tau_bar
to_power r)) ^2)) by Th37
.= ((-1) to_power (n-'r)) * (((tau to_power r) - (tau_bar to_power r)) *
S) ^2
.= ((-1) to_power (n-'r)) * (((tau to_power r) - (tau_bar to_power r)) /
(sqrt 5)) ^2 by XCMPLX_1:99
.= ((-1) |^(n-'r)) * (((T to_power r) - (tau_bar to_power r)) / (sqrt 5)
) ^2 by POWER:41
.= ((-1) |^(n-'r)) * (Fib (r)) ^2 by FIB_NUM:7;
hence thesis;
end;
theorem
(Fib (n)) ^2 + (Fib (n+1)) ^2 = Fib (2*n + 1)
proof
defpred P[Nat] means (Fib ($1)) ^2 + (Fib ($1+1)) ^2 = Fib (2*$1 + 1);
A1: P[0] 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
A3: P[k];
assume
A4: P[k+1];
Fib (2 * (k+2) + 1) = Fib (2*k + 3) + Fib (2 * k + 4) by Lm1
.= Fib (2 * k + 3) + (Fib (2 * k + 3) + Fib (2 * k + 2)) by Th26
.= Fib (2 * k + 3) + Fib (2 * k + 3) + Fib (2 * k + 2)
.= 2 * Fib (2 * k + 3) + (Fib (2 * k + 3) - Fib (2 * k + 1)) by Th28
.= 2 * (Fib (k+1)) ^2 + 2 * (Fib (k+2)) ^2 + (Fib (k+2) - Fib (k)) * (
Fib (k+2) + Fib (k)) by A3,A4
.= 2 * (Fib (k+1)) ^2 + 2 * (Fib (k+2)) ^2 + Fib (k+1) * (Fib (k+2) +
Fib (k)) by Th29
.= Fib (k+1) * (Fib (k+1) + (Fib (k+1) + Fib (k))) + Fib (k+2) * (Fib
(k+2) + (Fib (k+2) + Fib (k+1)))
.= Fib (k+1) * (Fib (k+1) + Fib (k+2)) + Fib (k+2) * (Fib (k+2) + (Fib
(k+2) + Fib (k+1))) by Th24
.= Fib (k+1) * (Fib (k+2) + Fib (k+1)) + Fib (k+2) * (Fib (k+2) + Fib
(k+3)) by Th25
.= Fib (k+1) * Fib (k+3) + (Fib (k+2) * Fib (k+2) + Fib (k+2) * Fib (k
+3)) by Th25
.= Fib (k+3) * (Fib (k+1) + Fib (k+2)) + (Fib (k+2)) ^2
.= (Fib (k+3)) ^2 + (Fib (k+2)) ^2 by Th25;
hence thesis;
end;
A5: P[1] by Th21,PRE_FF:1;
for n being Nat holds P[n] from FIB_NUM:sch 1(A1,A5,A2);
hence thesis;
end;
theorem Th40:
for k being non zero Element of NAT holds Fib (n+k) = Fib (k) *
Fib (n+1) + Fib (k-'1) * Fib (n)
proof
defpred P[Nat] means Fib (n+$1) = Fib ($1) * Fib (n+1) + Fib ($1-'1) * Fib (
n);
Fib (1) * Fib (n+1) + Fib (1-'1) * Fib (n) = 1 * Fib (n+1) + 0 * Fib (n
) by PRE_FF:1,XREAL_1:232
.= Fib (n+1);
then
A1: P[1];
A2: for m being non zero Nat st P[m] & P[m+1] holds P[m+2]
proof
let m be non zero Nat;
A3: m >= 1 by NAT_2:19;
set F2 = Fib (m+2) * Fib (n+1);
set F1 = Fib (n+1) * Fib (m+2);
set k = m-'1;
assume
A4: ( P[m])& P[m+1];
Fib (n+(m+2)) = Fib ((n+m)+2) .= Fib (n+m) + Fib (n+m+1) by Th24
.= (Fib (m) * Fib (n+1) + Fib (k) * Fib (n)) + (Fib (m+1) * Fib (n+1)
+ Fib (m+(1-'1)) * Fib (n)) by A4,NAT_D:38
.= (Fib (m) * Fib (n+1) + Fib (k) * Fib (n)) + (Fib (m+1) * Fib (n+1)
+ Fib (m+(0 qua Nat)) * Fib (n)) by XREAL_1:232
.= Fib (n+1) * (Fib (m) + Fib (m+1)) + Fib (n) * (Fib (k) + Fib (m))
.= F1 + Fib (n) * (Fib (k) + Fib (m)) by Th24
.= F1 + Fib (n) * (Fib (k) + Fib (k+1)) by A3,XREAL_1:235
.= F2 + Fib (n) * Fib (m-'1+2) by Th24
.= F2 + Fib (m+2-'1) * Fib (n) by A3,NAT_D:38;
hence thesis;
end;
2 -' 1 = 2 - 1 by NAT_D:39;
then
A5: P[2] by Th21,Th24,PRE_FF:1;
for k being non zero Nat holds P[k] from FibInd1(A1,A5,A2);
hence thesis;
end;
theorem Th41:
for n being non zero Element of NAT holds Fib (n) divides Fib ( n*k)
proof
let n be non zero Element of NAT;
defpred P[Nat] means Fib (n) divides Fib (n*$1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
Fib (n * (k+1)) = Fib ((n*k) + n)
.= Fib (n) * Fib (n*k + 1) + Fib (n*k) * Fib (n -' 1) by Th40;
hence thesis by A2,Th12;
end;
A3: P[0] by NAT_D:6,PRE_FF:1;
for n being Nat holds P[n] from NAT_1:sch 2(A3, A1);
hence thesis;
end;
theorem Th42:
for k being non zero Element of NAT holds k divides n implies
Fib (k) divides Fib (n)
proof
let k be non zero Element of NAT;
assume k divides n;
then ex m being Nat st n = k * m by NAT_D:def 3;
hence thesis by Th41;
end;
theorem Th43:
Fib (n) <= Fib (n + 1)
proof
defpred P[Nat] means Fib ($1) <= Fib ($1 + 1);
A1: P[0] 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
A3: P[k];
assume P[k+1];
then Fib (k) + Fib (k+1) <= Fib (k+1) + Fib (k+2) by A3,XREAL_1:7;
then Fib (k+2) <= Fib (k+1) + Fib (k+2) by Th24;
then Fib (k+2) <= Fib (k+3) by Th25;
hence thesis;
end;
A4: P[1] by Th21,PRE_FF:1;
for n being Nat holds P[n] from FIB_NUM:sch 1(A1,A4,A2);
hence thesis;
end;
theorem Th44:
for n being Nat st n > 1 holds Fib (n) < Fib (n+1)
proof
defpred P[Nat] means Fib ($1) < Fib ($1 + 1);
let n be Nat;
assume n > 1;
then
A1: n is non trivial by NAT_2:def 1;
A2: P[3] by Th22,Th23;
A3: for k being non trivial Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be non trivial Nat;
assume
A4: P[k];
assume P[k+1];
then Fib (k) + Fib (k+1) < Fib (k+1) + Fib (k+2) by A4,XREAL_1:8;
then Fib (k+2) < Fib (k+1) + Fib (k+2) by Th24;
then Fib (k+2) < Fib (k+3) by Th25;
hence thesis;
end;
A5: P[2] by Th21,Th22;
for n being non trivial Nat holds P[n] from FibInd2(A5,A2,A3);
hence thesis by A1;
end;
theorem
for m, n st m >= n holds Fib(m) >= Fib(n)
proof
let m, n;
assume m >= n;
then consider k be Nat such that
A1: m = n + k by NAT_1:10;
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;
assume
A3: P[k];
let n;
n + (k+1) = (n+k) + 1;
then
A4: Fib(n + (k+1)) >= Fib(n+k) by Th43;
Fib(n+k) >= Fib(n) by A3;
hence thesis by A4,XXREAL_0:2;
end;
let k;
let n;
A5: P[0];
for k holds P[k] from NAT_1:sch 2(A5, A2);
hence thesis;
end;
hence thesis by A1;
end;
theorem Th46:
for k being Nat st k > 1 holds k < n implies Fib (k) < Fib (n)
proof
let k be Nat such that
A1: k > 1;
assume
A2: k < n;
then consider m being Nat such that
A3: n = k + m by NAT_1:10;
reconsider k as non zero Element of NAT by A1,ORDINAL1:def 12;
reconsider m as non zero Element of NAT by A2,A3,ORDINAL1:def 12;
for k, m being non zero Element of NAT st k > 1 holds Fib (k) < Fib (k + m)
proof
let k, m be non zero Element of NAT such that
A4: k > 1;
defpred P[Nat] means Fib (k) < Fib (k + $1);
A5: for r being non zero Nat st P[r] holds P[r+1]
proof
let r be non zero Nat;
k + r > 0 + 1 by A4,XREAL_1:8;
then
A6: Fib (k + r) < Fib ((k + r) + 1) by Th44;
assume P[r];
hence thesis by A6,XXREAL_0:2;
end;
A7: P[1] by A4,Th44;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A7,A5);
hence thesis;
end;
then Fib (k) < Fib (k + m) by A1;
hence thesis by A3;
end;
theorem Th47:
Fib (k) = 1 iff k = 1 or k = 2
proof
Fib (k) = 1 implies k = 1 or k = 2
proof
assume
A1: Fib (k) = 1;
assume that
A2: not k = 1 and
A3: not k = 2;
A4: k < 2 or k > 2 by A3,XXREAL_0:1;
k = 0 or k > 1 by A2,NAT_2:19;
hence contradiction by A1,A4,Th21,Th46,PRE_FF:1;
end;
hence thesis by Th21,PRE_FF:1;
end;
theorem Th48:
for k,n being Element of NAT st n > 1 & k <> 0 & k <> 1 holds
Fib (k) = Fib (n) iff k = n
proof
let k, n be Element of NAT such that
A1: n > 1 and
A2: k <> 0 & k <> 1;
k is non trivial by A2,NAT_2:def 1;
then k >= 1 + 1 by NAT_2:29;
then
A3: k > 1 by NAT_1:13;
Fib (k) = Fib (n) implies k = n
proof
assume
A4: Fib (k) = Fib (n);
assume
A5: k <> n;
per cases by A5,XXREAL_0:1;
suppose
k > n;
hence contradiction by A1,A4,Th46;
end;
suppose
k < n;
hence contradiction by A3,A4,Th46;
end;
end;
hence thesis;
end;
theorem Th49:
for n being Element of NAT st n > 1 & n <> 4 holds n is non
prime implies ex k being non zero Element of NAT st k <> 1 & k <> 2 & k <> n &
k divides n
proof
let n be Element of NAT such that
A1: n > 1 and
A2: n <> 4;
assume
A3: n is non prime;
per cases by A3,INT_2:def 4;
suppose
n <= 1;
hence thesis by A1;
end;
suppose
not for k being Nat holds k divides n implies k = 1 or k = n;
then consider k being Nat such that
A4: k divides n and
A5: k <> 1 & k <> n;
consider m being Nat such that
A6: n = k*m by A4,NAT_D:def 3;
A7: m divides n & m is non zero Element of NAT by A1,A6,NAT_D:def 3
,ORDINAL1:def 12;
A8: k is non zero Element of NAT by A1,A4,INT_2:3,ORDINAL1:def 12;
A9: k <> 2 or m <> 2 by A2,A6;
m <> 1 & m <> n by A1,A5,A6,XCMPLX_1:7;
hence thesis by A4,A5,A8,A7,A9;
end;
end;
theorem
for n being Element of NAT st n > 1 & n <> 4 holds Fib (n) is prime
implies n is prime
proof
let n be Element of NAT such that
A1: n > 1 and
A2: n <> 4;
assume
A3: Fib (n) is prime;
assume not n is prime;
then consider k being non zero Element of NAT such that
A4: k <> 1 and
A5: k <> 2 and
A6: k <> n and
A7: k divides n by A1,A2,Th49;
A8: Fib (k) <> Fib (n) by A1,A4,A6,Th48;
Fib (k) <> 1 & Fib (k) divides Fib (n) by A4,A5,A7,Th42,Th47;
hence contradiction by A3,A8,INT_2:def 4;
end;
begin :: Sequence of Fibonacci Numbers
definition
func FIB -> sequence of NAT means
:Def2:
for k being Element of NAT holds it.k = Fib(k);
existence
proof
ex f being sequence of NAT st for x being Element of NAT holds f.x
= Fib(x) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
A1: for f1, f2 be sequence of NAT st (for x being Element of NAT
holds f1.x = Fib(x)) & (for x being Element of NAT holds f2.x = Fib(x)) holds
f1 = f2 from BINOP_2:sch 1;
let f1, f2 be sequence of NAT;
assume ( for k being Element of NAT holds f1.k = Fib(k))& for k being
Element of NAT holds f2.k = Fib(k);
hence thesis by A1;
end;
end;
definition
func EvenNAT -> Subset of NAT equals
the set of all 2 * k where k is Nat ;
coherence
proof
the set of all 2*k where k is Nat c= NAT
proof let x be object;
assume x in the set of all 2*k where k is Nat ;
then ex k being Nat st x = 2*k;
hence thesis by ORDINAL1:def 12;
end;
hence thesis;
end;
func OddNAT -> Subset of NAT equals
the set of all 2 * k + 1 where k is Element of NAT ;
coherence
proof
defpred P[set] means not contradiction;
deffunc F(Element of NAT) = 2 * $1 + 1;
{ F(k) where k is Element of NAT : P[k] } is Subset of NAT from
DOMAIN_1:sch 8;
hence thesis;
end;
end;
theorem Th51:
for k being Nat holds 2 * k in EvenNAT & not 2 * k + 1 in EvenNAT
proof
let k be Nat;
thus 2 * k in EvenNAT;
assume 2 * k + 1 in EvenNAT;
then ex p being Nat st 2 * k + 1 = 2 * p;
hence thesis;
end;
theorem Th52:
for k being Element of NAT holds 2 * k + 1 in OddNAT & not 2 * k in OddNAT
proof
let k be Element of NAT;
thus 2 * k + 1 in OddNAT;
assume 2 * k in OddNAT;
then ex p being Element of NAT st 2 * k = 2 * p + 1;
hence thesis;
end;
definition
let n be Nat;
func EvenFibs (n) -> FinSequence of NAT equals
Prefix (FIB, EvenNAT /\ Seg n);
coherence;
func OddFibs (n) -> FinSequence of NAT equals
Prefix (FIB, OddNAT /\ Seg n);
coherence;
end;
theorem Th53:
EvenFibs (0) = {};
theorem
Seq (FIB| {2}) = <*1*>
proof
reconsider H = {[2,FIB.2]} as Function;
A1: dom H = {2} by RELAT_1:9;
dom H c= Seg 2
proof
let x be object;
assume x in dom H;
then x = 2 by A1,TARSKI:def 1;
hence thesis;
end;
then reconsider H as FinSubsequence by FINSEQ_1:def 12;
2 in NAT;
then 2 in dom FIB by FUNCT_2:def 1;
then Seq (FIB | {2}) = Seq H by GRFUNC_1:28
.= <*FIB.2*> by FINSEQ_3:157
.= <*1*> by Def2,Th21;
hence thesis;
end;
theorem Th55:
EvenFibs (2) = <*1*>
proof
now
let x be object;
assume
A1: x in EvenNAT /\ {1,2};
then
A2: x in EvenNAT by XBOOLE_0:def 4;
A3: x in {1,2} by A1,XBOOLE_0:def 4;
per cases by A3,TARSKI:def 2;
suppose x = 1;
then x = 0 + 1;
then
A4: x = 2 * (0 qua Nat) + 1;
ex k being Nat st x = 2*k by A2;
hence x in {2} by A4;
end;
suppose
x = 2 * 1;
hence x in {2} by TARSKI:def 1;
end;
end;
then
A5: EvenNAT /\ {1,2} c= {2};
set q = {[2,FIB.2]};
reconsider q as FinSubsequence by Th17;
2 in NAT;
then
A6: 2 in dom FIB by FUNCT_2:def 1;
now
let x be object;
assume x in {2};
then x = 2 * 1 by TARSKI:def 1;
then x in EvenNAT & x in {1,2} by TARSKI:def 2;
hence x in EvenNAT /\ {1,2} by XBOOLE_0:def 4;
end;
then {2} c= EvenNAT /\ {1,2};
then EvenNAT /\ {1,2} = {2} by A5;
then EvenFibs (2) = Seq q by A6,FINSEQ_1:2,GRFUNC_1:28
.= <*FIB.2*> by FINSEQ_3:157
.= <*1*> by Def2,Th21;
hence thesis;
end;
theorem
EvenFibs (4) = <*1,3*>
proof
now
let x be object;
assume
A1: x in EvenNAT /\ {1,2,3,4};
then
A2: x in EvenNAT by XBOOLE_0:def 4;
A3: x in {1,2,3,4} by A1,XBOOLE_0:def 4;
per cases by A3,ENUMSET1:def 2;
suppose
x = 2 * (0 qua Nat) + 1;
hence x in {2,4} by A2,Th51;
end;
suppose
x = 2 * 1;
hence x in {2,4} by TARSKI:def 2;
end;
suppose
x = 2 * 1 + 1;
hence x in {2,4} by A2,Th51;
end;
suppose
x = 2 * 2;
hence x in {2,4} by TARSKI:def 2;
end;
end;
then
A4: EvenNAT /\ {1,2,3,4} c= {2,4};
set q = {[2,FIB.2],[4,FIB.4]};
4 in NAT;
then
A5: 4 in dom FIB by FUNCT_2:def 1;
reconsider q as FinSubsequence by Th15;
2 in NAT;
then
A6: 2 in dom FIB by FUNCT_2:def 1;
A7: FIB | ({2} \/ {4}) = (FIB | {2}) \/ (FIB | {4}) by RELAT_1:78
.= {[2,FIB.2]} \/ (FIB | {4}) by A6,GRFUNC_1:28
.= {[2,FIB.2]} \/ {[4,FIB.4]} by A5,GRFUNC_1:28
.= q by ENUMSET1:1;
now
let x be object;
assume
A8: x in {2,4};
then x = 2 * 1 or x = 2 * 2 by TARSKI:def 2;
then
A9: x in EvenNAT;
x = 2 or x = 4 by A8,TARSKI:def 2;
then x in {1,2,3,4} by ENUMSET1:def 2;
hence x in EvenNAT /\ {1,2,3,4} by A9,XBOOLE_0:def 4;
end;
then {2,4} c= EvenNAT /\ {1,2,3,4};
then EvenNAT /\ {1,2,3,4} = {2,4} by A4;
then EvenFibs (4) = Seq q by A7,ENUMSET1:1,FINSEQ_3:2
.= <*FIB.2,FIB.4*> by Th16
.= <*(Fib (2)),FIB.4*> by Def2
.= <*1,3*> by Def2,Th21,Th23;
hence thesis;
end;
theorem Th57:
for k being Nat holds (EvenNAT /\ Seg (2 * k + 2)) \/
{2 * k + 4} = EvenNAT /\ Seg (2 * k + 4)
proof
let k be Nat;
2 * k + 4 = 2 * (k + 2);
then
A1: 2 * k + 4 in EvenNAT;
2 * k + 3 = 2 * (k + 1) + 1;
then
A2: {2*k+3} misses EvenNAT by Th51,ZFMISC_1:50;
EvenNAT /\ Seg (2 * k + 4) = EvenNAT /\ Seg (2 * k + 3 + 1)
.= EvenNAT /\ (Seg (2 * k + 3) \/ {2 * k + 4}) by FINSEQ_1:9
.= EvenNAT /\ Seg (2 * k + 3) \/ EvenNAT /\ {2 * k + 4} by XBOOLE_1:23
.= EvenNAT /\ Seg (2 * k + 2 + 1) \/ {2 * k + 4} by A1,ZFMISC_1:46
.= EvenNAT /\ (Seg (2 * k + 2) \/ {2 * k + 3}) \/ {2 * k + 4} by FINSEQ_1:9
.= EvenNAT /\ Seg (2 * k + 2) \/ EvenNAT /\ {2 * k + 3} \/ {2 * k + 4}
by XBOOLE_1:23
.= EvenNAT /\ Seg (2 * k + 2) \/ {} \/ {2 * k + 4} by A2
.= EvenNAT /\ Seg (2 * k + 2) \/ {2 * k + 4};
hence thesis;
end;
theorem Th58:
for k being Nat holds FIB | (EvenNAT /\ Seg (2 * k +
2)) \/ {[2*k+4,FIB.(2 * k + 4)]} = FIB | (EvenNAT /\ Seg (2 * k + 4))
proof
let k be Nat;
A1: dom FIB = NAT by FUNCT_2:def 1;
FIB | (EvenNAT /\ Seg (2 * k + 4)) = FIB | ((EvenNAT /\ Seg (2 * k + 2))
\/ {2 * k + 4}) by Th57
.= (FIB | (EvenNAT /\ Seg (2 * k + 2))) \/ (FIB |{2 * k + 4}) by RELAT_1:78
.= FIB | (EvenNAT /\ Seg (2 * k + 2)) \/ {[2*k+4,FIB.(2*k+4)]} by A1,
GRFUNC_1:28;
hence thesis;
end;
theorem Th59:
for n being Element of NAT holds EvenFibs (2 * n + 2) = EvenFibs
(2 * n) ^ <* Fib (2 * n + 2) *>
proof
defpred P[Nat] means
EvenFibs (2 * $1 + 2) = EvenFibs (2 * $1) ^
<* Fib (2 * $1 + 2) *>;
let n be Element of NAT;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider ARR = {[1,FIB.(2*k+4)]} as FinSubsequence by Th17;
assume P[k];
set LEFTk = EvenFibs (2 * (k+1) + 2);
set RIGHTk = EvenFibs (2 * (k+1)) ^ <*Fib (2 * (k+1) + 2)*>;
reconsider RS = FIB | (EvenNAT /\ Seg (2 * k + 2)) as FinSubsequence;
set RR = Shift(ARR,2*k+3);
A2: 2 * k + 3 > 2 * k + 2 by XREAL_1:6;
dom RS c= EvenNAT /\ Seg (2 * k + 2) & EvenNAT /\ Seg (2 * k + 2) c=
Seg (2 * k + 2) by RELAT_1:58,XBOOLE_1:17;
then consider p1 being FinSequence such that
A3: RS c= p1 and
A4: dom p1 = Seg (2*k+3) by A2,Th19,XBOOLE_1:1;
A5: ex p2 being FinSequence st ARR c= p2 by Th20;
1 + (2 * k + 3) = 2*k+4;
then
A6: RR = {[2*k+4,FIB.(2*k+4)]} by Th18;
len p1 = 2*k + 3 by A4,FINSEQ_1:def 3;
then consider RSR being FinSubsequence such that
A7: RSR = RS \/ RR and
A8: (Seq RS)^(Seq ARR) = Seq RSR by A3,A5,VALUED_1:64;
RIGHTk = Seq (FIB | (EvenNAT /\ Seg (2 * k + 2))) ^ <* FIB.(2 * k + 4
) *> by Def2
.= Seq (RSR) by A8,FINSEQ_3:157
.= LEFTk by A7,A6,Th58;
hence thesis;
end;
A9: P[0] by Th21,Th53,Th55,FINSEQ_1:34;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A1);
hence thesis;
end;
theorem Th60:
OddFibs (1) = <*1*>
proof
now
let x be object;
assume
A1: x in {1};
then x = 2 * (0 qua Nat) + 1 by TARSKI:def 1;
then x in OddNAT;
hence x in OddNAT /\ {1} by A1,XBOOLE_0:def 4;
end;
then
A2: {1} c= OddNAT /\ {1};
1 in NAT;
then
A3: 1 in dom FIB by FUNCT_2:def 1;
for x be object st x in OddNAT /\ {1} holds x in {1} by XBOOLE_0:def 4;
then OddNAT /\ {1} c= {1};
then OddNAT /\ {1} = {1} by A2;
then OddFibs (1) = <*FIB.1*> by A3,FINSEQ_1:2,FINSEQ_3:157,GRFUNC_1:28
.= <*1*> by Def2,PRE_FF:1;
hence thesis;
end;
theorem Th61:
OddFibs (3) = <*1,2*>
proof
now
let x be object;
assume
A1: x in OddNAT /\ {1,2,3};
then
A2: x in OddNAT by XBOOLE_0:def 4;
A3: x in {1,2,3} by A1,XBOOLE_0:def 4;
per cases by A3,ENUMSET1:def 1;
suppose
x = 2 * (0 qua Nat) + 1;
hence x in {1,3} by TARSKI:def 2;
end;
suppose
x = 2 * 1;
hence x in {1,3} by A2,Th52;
end;
suppose
x = 2 * 1 + 1;
hence x in {1,3} by TARSKI:def 2;
end;
end;
then
A4: OddNAT /\ {1,2,3} c= {1,3};
set q = {[1,FIB.1],[3,FIB.3]};
3 in NAT;
then
A5: 3 in dom FIB by FUNCT_2:def 1;
reconsider q as FinSubsequence by Th15;
1 in NAT;
then
A6: 1 in dom FIB by FUNCT_2:def 1;
A7: FIB | ({1} \/ {3}) = (FIB | {1}) \/ (FIB | {3}) by RELAT_1:78
.= {[1,FIB.1]} \/ (FIB | {3}) by A6,GRFUNC_1:28
.= {[1,FIB.1]} \/ {[3,FIB.3]} by A5,GRFUNC_1:28
.= q by ENUMSET1:1;
now
let x be object;
assume
A8: x in {1,3};
then x = 2 * (0 qua Nat) + 1 or x = 2 * 1 + 1 by TARSKI:def 2;
then
A9: x in OddNAT;
x = 1 or x = 3 by A8,TARSKI:def 2;
then x in {1,2,3} by ENUMSET1:def 1;
hence x in OddNAT /\ {1,2,3} by A9,XBOOLE_0:def 4;
end;
then {1,3} c= OddNAT /\ {1,2,3};
then OddNAT /\ {1,2,3} = {1,3} by A4;
then OddFibs (3) = Seq (FIB | ({1} \/ {3})) by ENUMSET1:1,FINSEQ_3:1
.= <*FIB.1,FIB.3*> by A7,Th16
.= <* Fib (1), FIB.3 *> by Def2
.= <* 1, 2 *> by Def2,Th22,PRE_FF:1;
hence thesis;
end;
theorem Th62:
for k being Nat holds OddNAT /\ Seg (2 * k + 3) \/ {2 * k + 5} =
OddNAT /\ Seg (2 * k + 5)
proof
let k be Nat;
2 * k + 5 = 2 * (k + 2) + 1;
then
A1: 2 * k + 5 in OddNAT;
2 * k + 4 = 2 * ((k+1) +1);
then
A2: {2 * k + 4} misses OddNAT by Th52,ZFMISC_1:50;
OddNAT /\ Seg (2 * k + 5) = OddNAT /\ Seg (2 * k + 4 + 1)
.= OddNAT /\ (Seg (2 * k + 4) \/ {2 * k + 5}) by FINSEQ_1:9
.= OddNAT /\ Seg (2 * k + 3 + 1) \/ OddNAT /\ {2 * k + 5} by XBOOLE_1:23
.= OddNAT /\ (Seg (2 * k + 3) \/ {2 * k + 4}) \/ OddNAT /\ {2 * k + 5}
by FINSEQ_1:9
.= OddNAT /\ Seg (2 * k + 3) \/ OddNAT /\ {2 * k + 4} \/ OddNAT /\ {2 *
k + 5} by XBOOLE_1:23
.= OddNAT /\ Seg (2 * k + 3) \/ {} \/ OddNAT /\ {2 * k + 5} by A2
.= OddNAT /\ Seg (2 * k + 3) \/ {2 * k + 5} by A1,ZFMISC_1:46;
hence thesis;
end;
theorem Th63:
for k being Nat holds (FIB | (OddNAT /\ Seg (2 * k + 3))) \/ {[2
*k+5,FIB.(2 * k + 5)]} = (FIB | (OddNAT /\ Seg (2 * k + 5)))
proof
let k be Nat;
A1: dom FIB = NAT by FUNCT_2:def 1;
(FIB | (OddNAT /\ Seg (2 * k + 5))) = (FIB | (OddNAT /\ Seg (2 * k + 3)
\/ {2 * k + 5})) by Th62
.= FIB | (OddNAT /\ Seg (2 * k + 3)) \/ (FIB | ({2 * k + 5})) by RELAT_1:78
.= FIB | (OddNAT /\ Seg (2 * k + 3)) \/ {[2*k+5,FIB.(2 * k + 5)]} by A1,
GRFUNC_1:28;
hence thesis;
end;
theorem Th64:
for n being Nat holds OddFibs (2 * n + 3) = OddFibs (2 * n + 1)
^ <* Fib (2 * n + 3) *>
proof
defpred P[Nat] means OddFibs (2 * $1 + 3) = OddFibs (2 * $1 + 1) ^ <* Fib (2
* $1 + 3) *>;
let n be Nat;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider ARR = {[1,FIB.(2 * k + 5)]} as FinSubsequence by Th17;
assume P[k];
set LEFTk = OddFibs (2 * (k + 1) + 3);
set RIGHTk = OddFibs (2 * (k + 1) + 1) ^ <* Fib (2 * (k + 1) + 3)*>;
reconsider RS = FIB | (OddNAT /\ Seg (2 * k + 3)) as FinSubsequence;
set RR = Shift(ARR,2*k+4);
A2: 2 * k + 4 > 2 * k + 3 by XREAL_1:6;
dom RS c= OddNAT /\ Seg (2 * k + 3) & OddNAT /\ Seg (2 * k + 3) c= Seg
(2 * k + 3) by RELAT_1:58,XBOOLE_1:17;
then consider p1 being FinSequence such that
A3: RS c= p1 and
A4: dom p1 = Seg (2 * k + 4) by A2,Th19,XBOOLE_1:1;
A5: ex p2 being FinSequence st ARR c= p2 by Th20;
1 + (2 * k + 4) = 2 * k + 5;
then
A6: RR = {[2 * k + 5,FIB.(2 * k + 5)]} by Th18;
len p1 = 2 * k + 4 by A4,FINSEQ_1:def 3;
then consider RSR being FinSubsequence such that
A7: RSR = RS \/ RR and
A8: (Seq RS) ^ (Seq ARR) = Seq RSR by A3,A5,VALUED_1:64;
RIGHTk = Seq (FIB | (OddNAT /\ Seg (2 * k + 3))) ^ <* FIB.(2 * k + 5)
*> by Def2
.= Seq (RSR) by A8,FINSEQ_3:157
.= LEFTk by A7,A6,Th63;
hence thesis;
end;
A9: P[0] by Th22,Th60,Th61;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A1);
hence thesis;
end;
theorem
for n being Element of NAT holds Sum EvenFibs (2 * n + 2) = Fib (2 * n
+ 3) - 1
proof
defpred P[Nat] means Sum EvenFibs (2 * $1 + 2) = Fib (2 * $1 + 3) - 1;
let n be Element of NAT;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider EE = EvenFibs (2 * ( k + 1)) as FinSequence of REAL
by FINSEQ_2:24,NUMBERS:19;
assume
A2: P[k];
Sum EvenFibs (2 * (k + 1) + 2) = Sum ((EvenFibs (2 * ( k + 1)) qua
FinSequence of NAT) ^ <*Fib (2 * (k + 1) + 2)*>) by Th59
.= Sum EE + Fib (2 * (k + 1) + 2) by RVSUM_1:74
.= Fib (2 * k + 3) + Fib (2 * k + 4) - 1 by A2
.= Fib (2 * k + 5) - 1 by Th27;
hence thesis;
end;
A3: P[0] by Th22,Th55,RVSUM_1:73;
for n being Nat holds P[n] from NAT_1:sch 2(A3, A1);
hence thesis;
end;
theorem
for n being Nat holds Sum OddFibs (2 * n + 1) = Fib (2 * n + 2)
proof
defpred P[Nat] means Sum OddFibs (2 * $1 + 1) = Fib (2 * $1 + 2);
let n be Nat;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider EE = OddFibs (2 * k + 1) as FinSequence of REAL
by FINSEQ_2:24,NUMBERS:19;
assume
A2: P[k];
Sum OddFibs (2 * (k + 1) + 1) = Sum ((OddFibs (2 * k + 1)) ^ <*(Fib (2
* k + 3) qua Element of NAT)*>) by Th64
.= Sum EE + Fib (2 * k + 3) by RVSUM_1:74
.= Fib (2 * k + 4) by A2,Th26;
hence thesis;
end;
A3: P[0] by Th21,Th60,RVSUM_1:73;
for n being Nat holds P[n] from NAT_1:sch 2(A3, A1);
hence thesis;
end;
begin :: Carmichael's Theorem on Prime Divisors
theorem Th67:
for n being Element of NAT holds Fib (n), Fib (n+1) are_coprime
proof
let n be Element of NAT;
A1: n,n + 1 are_coprime by PEPIN:1;
Fib (n) gcd Fib (n + 1) = Fib (n gcd (n + 1)) by FIB_NUM:5
.= 1 by A1,INT_2:def 3,PRE_FF:1;
hence thesis by INT_2:def 3;
end;
theorem Th68:
for n being non zero Nat, m being Nat st m <> 1 holds m divides
Fib (n) implies not m divides Fib (n-'1)
proof
let n be non zero Nat;
let m be Nat;
assume
A1: m <> 1;
assume
A2: m divides Fib (n);
n >= 1 by NAT_2:19;
then n = n -' 1 + 1 by XREAL_1:235;
then Fib (n-'1), Fib (n) are_coprime by Th67;
then
A3: Fib (n-'1) gcd Fib (n) = 1 by INT_2:def 3;
assume m divides Fib (n-'1);
then m divides 1 by A2,A3,NAT_D:def 5;
hence contradiction by A1,WSIERP_1:15;
end;
::$N Carmichael's Theorem on Prime Divisors
theorem
for n being non zero Nat holds m is prime & n is prime & m divides
Fib (n) implies for r being Nat st r < n & r <> 0 holds not m divides Fib (r)
proof
let n be non zero Nat;
assume
A1: m is prime;
defpred R[Element of NAT] means $1 < n & $1 <> 0 & m divides Fib ($1);
assume
A2: n is prime;
reconsider C = {x where x is Element of NAT : R[x]} as Subset of NAT from
DOMAIN_1:sch 7;
assume
A3: m divides Fib(n);
assume
A4: not for r being Nat st (r < n & r <> 0) holds not m divides Fib (r);
C is non empty Subset of NAT
proof
consider r being Nat such that
A5: r < n & r <> 0 & m divides Fib (r) by A4;
r in NAT by ORDINAL1:def 12;
then r in C by A5;
hence thesis;
end;
then reconsider C as non empty Subset of NAT;
reconsider r = min C as Nat by TARSKI:1;
defpred P[Nat] means (m divides Fib (n -' r * ($1 + 1)) & r <= n / ($1 + 2));
r in C by XXREAL_2:def 7;
then
A6: ex r9 being Element of NAT st r9 = r & R[r9];
then
A7: n -' r < n by NAT_2:9;
m <> 1 by A1,INT_2:def 4;
then
A8: not m divides Fib (r-'1) by A6,Th68;
A9: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A10: m divides Fib (r) * Fib (n-'(k+2) * r+1) by A6,NAT_D:9;
A11: n - r * (k+2) <> 0
proof
assume
A12: n - r * (k+2) = 0;
then
A13: r divides n & k+2 divides n by NAT_D:def 3;
per cases by A2,A13,INT_2:def 4;
suppose
r = 1 & k+2 = n;
then m = 1 by A6,PRE_FF:1,WSIERP_1:15;
hence contradiction by A1,INT_2:def 4;
end;
suppose
r=1 & k+2=1;
hence contradiction by A2,A12,INT_2:def 4;
end;
suppose
r=n & k+2=n;
hence contradiction by A6;
end;
suppose
r=n & k+2=1;
hence contradiction by A6;
end;
end;
- r < -(0 qua Nat) by A6;
then (- r) * (k+2) < 0 * (k+2);
then - r * (k+2) + n < (0 qua Nat) + n by XREAL_1:6;
then
A14: n -' (k+2) * r < n by A11,XREAL_0:def 2;
assume
A15: P[k];
then
A16: r * (k+2) <= n / (k+2) * (k+2) by XREAL_1:64;
then
A17: r * (k+2) <= n by XCMPLX_1:87;
then
A18: n - r * (k+2) >= r * (k+2) - r * (k+2) by XREAL_1:9;
then
A19: n -' (k+2) * r <> 0 by A11,XREAL_0:def 2;
r + r * (k+1) <= n by A16,XCMPLX_1:87;
then r * (k+1) < n by A6,Th14;
then
A20: (k+1) * r - (k+1) * r < n - (k+1) * r by XREAL_1:9;
n - (k+1) * r - r > 0 by A11,A18;
then n -' (k+1) * r - r > 0 by A20,XREAL_0:def 2;
then
A21: n -' (k+1) * r -' r = n -' (k+1) * r - r by XREAL_0:def 2
.= n - (k+1) * r - r by A20,XREAL_0:def 2
.= n -'((k+2) * r) by A18,XREAL_0:def 2;
n - r * (k+1) >= r + r * (k+1) - r * (k+1) by A17,XREAL_1:9;
then r <= n -' r * (k+1) by XREAL_0:def 2;
then Fib (n -' (k+1) * r) = Fib (n -' (k+2) * r + r) by A21,XREAL_1:235
.= Fib (r) * Fib (n-'(k+2) * r+1) + Fib (r-'1) * Fib (n-'(k+2)*r) by A6
,Th40;
then
A22: m divides Fib (r-'1) * Fib (n-'(k+2) * r) by A15,A10,NAT_D:10;
then m divides Fib (n-'(k+2) * r) by A1,A8,NEWTON:80;
then n -' (k+2) * r in C by A19,A14;
then n -'(k+2) * r >= r by XXREAL_2:def 7;
then n >= r + (k+2) * r by A17,NAT_D:54;
then n * (1/(1+k+2)) >= (r * (1+k+2)) * (1/(1+k+2)) by XREAL_1:64;
then n * (1/(1+k+2)) >= (r * (1+k+2)) / (1+k+2) by XCMPLX_1:99;
then n / (1+k+2) >= r * (1+k+2) / (1+k+2) by XCMPLX_1:99;
hence thesis by A1,A8,A22,NEWTON:80,XCMPLX_1:89;
end;
r - r < n - r by A6,XREAL_1:9;
then
A23: n -' r <> 0 by XREAL_0:def 2;
A24: m divides Fib (r) * Fib (n-'r+1) by A6,NAT_D:9;
Fib (n) = Fib (n -' r + r) by A6,XREAL_1:235
.= Fib (r) * Fib (n-'r+1) + Fib (r-'1) * Fib (n-'r) by A6,Th40;
then
A25: m divides Fib (r-'1) * Fib (n-'r) by A3,A24,NAT_D:10;
then m divides Fib (n-'r) by A1,A8,NEWTON:80;
then n -' r in C by A7,A23;
then n -' r >= r by XXREAL_2:def 7;
then n >= r + r by A6,NAT_D:54;
then n / 2 >= (2*r) / 2 by XREAL_1:72;
then
A26: P[0] by A1,A8,A25,NEWTON:80;
for k being Nat holds P[k] from NAT_1:sch 2(A26,A9);
then n / (n+2) < 1 & r <= n /(n+2) by XREAL_1:29,191;
then r < 1 + 0 by XXREAL_0:2;
hence contradiction by A6,NAT_1:13;
end;
begin :: Fibonacci Numbers and Pythagorean Triples
theorem
for n being non zero Element of NAT holds {Fib (n) * Fib (n+3), 2 *
Fib (n+1) * Fib (n+2), (Fib (n+1)) ^2 + (Fib (n+2)) ^2} is Pythagorean_triple
proof
let n be non zero Element of NAT;
(Fib (n) * Fib (n+3)) ^2 + ((2 * Fib (n+1)) * Fib (n+2)) ^2 = (Fib (n))
^2 * (Fib (n+3)) ^2 + (2 * 2) * (Fib (n+1)) ^2 * (Fib (n+2)) ^2
.= (Fib (n)) ^2 * (Fib (n+2) + Fib (n+1)) ^2 + 4 * (Fib (n+1)) ^2 * (Fib
(n+2)) ^2 by Th25
.= (Fib (n+2) - Fib (n+1)) ^2 * (Fib (n+2) + Fib (n+1)) ^2 + 4 * (Fib (n
+1)) ^2 * (Fib (n+2)) ^2 by Th30
.= ((Fib (n+1)) ^2 + (Fib (n+2)) ^2) ^2;
hence thesis by PYTHTRIP:def 4;
end;