:: Some Properties of {F}ibonacci Numbers
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received May 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem :: FIB_NUM2:1
for n being non empty Element of NAT holds (n -' 1) + 2 = n + 1
proofend;

theorem Th2: :: FIB_NUM2:2
for n being odd Integer holds (- 1) to_power n = - 1
proofend;

theorem Th3: :: FIB_NUM2:3
for n being even Integer holds (- 1) to_power n = 1
proofend;

theorem Th4: :: FIB_NUM2:4
for m being non empty real number
for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
proofend;

theorem Th5: :: FIB_NUM2:5
for k, m being Nat
for a being real number holds a to_power (k + m) = (a to_power k) * (a to_power m)
proofend;

theorem Th6: :: FIB_NUM2:6
for n being Nat
for k being non empty real number
for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)
proofend;

theorem Th7: :: FIB_NUM2:7
for n being Nat holds ((- 1) to_power (- n)) ^2 = 1
proofend;

theorem Th8: :: FIB_NUM2:8
for k, m being Nat
for a being non empty real number holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)
proofend;

theorem Th9: :: FIB_NUM2:9
for n being Nat holds (- 1) to_power (- (2 * n)) = 1
proofend;

theorem Th10: :: FIB_NUM2:10
for k being Nat
for a being non empty real number holds (a to_power k) * (a to_power (- k)) = 1
proofend;

registration
let n be odd Integer;
cluster - n ->  odd ;
coherence
 not - n is even
proofend;
end;

registration
let n be even Integer;
cluster - n ->  even ;
coherence
 - n is even
proofend;
end;

theorem Th11: :: FIB_NUM2:11
for n being Nat holds (- 1) to_power (- n) = (- 1) to_power n
proofend;

theorem Th12: :: FIB_NUM2:12
for n being Nat
for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
proofend;

registration
cluster non empty finite with_non-empty_elements natural-membered for set ;
existence
 ex b1 being set st
( b1 is finite & not b1 is empty & b1 is natural-membered & b1 is with_non-empty_elements )
proofend;
end;

registration
let f be Function of NAT,NAT;
let A be finite with_non-empty_elements natural-membered set ;
clusterf | A ->  FinSubsequence-like ;
coherence
 f | A is FinSubsequence-like
proofend;
end;

theorem :: FIB_NUM2:13
for p being FinSubsequence holds rng (Seq p) c= rng p by RELAT_1:26;

definition
let f be Function of NAT,NAT;
let A be finite with_non-empty_elements natural-membered set ;
func Prefix (f,A) ->  FinSequence of NAT  equals :: FIB_NUM2:def 1
 Seq (f | A);
coherence
 Seq (f | A) is FinSequence of NAT
proofend;
end;

:: deftheorem  defines Prefix FIB_NUM2:def_1_:_
 for f being Function of NAT,NAT
for A being finite with_non-empty_elements natural-membered set holds Prefix (f,A) = Seq (f | A);

theorem Th14: :: FIB_NUM2:14
for m, n being Nat
for k being Element of NAT st k <> 0 &amp; k + m <= n holds
m < n
proofend;

registration
cluster omega  ->  bounded_below ;
coherence
 NAT is bounded_below ;
end;

theorem Th15: :: FIB_NUM2:15
for i, j being Nat
for x, y being set st 0 < i &amp; i < j holds
{[i,x],[j,y]} is FinSubsequence
proofend;

theorem Th16: :: FIB_NUM2:16
for i, j being Nat
for x, y being set
for q being FinSubsequence st i < j &amp; q = {[i,x],[j,y]} holds
Seq q = <*x,y*>
proofend;

registration
let n be Element of NAT ;
cluster Seg n ->  with_non-empty_elements ;
coherence
 Seg n is with_non-empty_elements
proofend;
end;

registration
let A be with_non-empty_elements set ;
cluster  ->  with_non-empty_elements for Element of bool A;
coherence
 for b1 being Subset of A holds b1 is with_non-empty_elements
proofend;
end;

registration
let A be with_non-empty_elements set ;
let B be set ;
clusterA /\ B ->  with_non-empty_elements ;
coherence
 A /\ B is with_non-empty_elements
proofend;
clusterB /\ A ->  with_non-empty_elements ;
coherence
 B /\ A is with_non-empty_elements ;
end;

theorem Th17: :: FIB_NUM2:17
for k being Element of NAT
for a being set st k >= 1 holds
{[k,a]} is FinSubsequence
proofend;

theorem Th18: :: FIB_NUM2:18
for i being Element of NAT
for y being set
for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}
proofend;

theorem Th19: :: FIB_NUM2:19
for q being FinSubsequence
for k, n being Element of NAT st dom q c= Seg k &amp; n > k holds
ex p being FinSequence st
( q c= p &amp; dom p = Seg n )
proofend;

theorem Th20: :: FIB_NUM2:20
for q being FinSubsequence ex p being FinSequence st q c= p
proofend;

begin

scheme :: FIB_NUM2:sch 1
FibInd1{ P1[ set ] } :
 for k being non empty Nat holds P1[k]
provided
A1: P1[1] and
A2: P1[2] and
A3: for k being non empty Nat st P1[k] &amp; P1[k + 1] holds
P1[k + 2]
proofend;

scheme :: FIB_NUM2:sch 2
FibInd2{ P1[ set ] } :
 for k being non trivial Nat holds P1[k]
provided
A1: P1[2] and
A2: P1[3] and
A3: for k being non trivial Nat st P1[k] &amp; P1[k + 1] holds
P1[k + 2]
proofend;

theorem Th21: :: FIB_NUM2:21
Fib 2 = 1
proofend;

theorem Th22: :: FIB_NUM2:22
Fib 3 = 2
proofend;

theorem Th23: :: FIB_NUM2:23
Fib 4 = 3
proofend;

theorem Th24: :: FIB_NUM2:24
for n being Nat holds Fib (n + 2) = (Fib n) + (Fib (n + 1))
proofend;

theorem Th25: :: FIB_NUM2:25
for n being Nat holds Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1))
proofend;

theorem Th26: :: FIB_NUM2:26
for n being Nat holds Fib (n + 4) = (Fib (n + 2)) + (Fib (n + 3))
proofend;

theorem Th27: :: FIB_NUM2:27
for n being Nat holds Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4))
proofend;

Lm1:  for k being Nat holds Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4))
proofend;

theorem Th28: :: FIB_NUM2:28
for n being Nat holds Fib (n + 2) = (Fib (n + 3)) - (Fib (n + 1))
proofend;

theorem Th29: :: FIB_NUM2:29
for n being Nat holds Fib (n + 1) = (Fib (n + 2)) - (Fib n)
proofend;

theorem Th30: :: FIB_NUM2:30
for n being Nat holds Fib n = (Fib (n + 2)) - (Fib (n + 1))
proofend;

begin

theorem Th31: :: FIB_NUM2:31
for n being Nat holds ((Fib n) * (Fib (n + 2))) - ((Fib (n + 1)) ^2) = (- 1) |^ (n + 1)
proofend;

theorem :: FIB_NUM2:32
for n being non empty Element of NAT holds ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n
proofend;

theorem Th33: :: FIB_NUM2:33
tau > 0
proofend;

theorem Th34: :: FIB_NUM2:34
tau_bar = (- tau) to_power (- 1)
proofend;

theorem Th35: :: FIB_NUM2:35
for n being Nat holds (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n
proofend;

theorem Th36: :: FIB_NUM2:36
- (1 / tau) = tau_bar
proofend;

theorem Th37: :: FIB_NUM2:37
for r being Nat holds (((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
proofend;

theorem :: FIB_NUM2:38
for n, r being non empty Element of NAT st r <= n holds
((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)
proofend;

theorem :: FIB_NUM2:39
for n being Nat holds ((Fib n) ^2) + ((Fib (n + 1)) ^2) = Fib ((2 * n) + 1)
proofend;

theorem Th40: :: FIB_NUM2:40
for n being Nat
for k being non empty Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))
proofend;

theorem Th41: :: FIB_NUM2:41
for k being Nat
for n being non empty Element of NAT holds Fib n divides Fib (n * k)
proofend;

theorem Th42: :: FIB_NUM2:42
for n being Nat
for k being non empty Element of NAT st k divides n holds
Fib k divides Fib n
proofend;

theorem Th43: :: FIB_NUM2:43
for n being Nat holds Fib n <= Fib (n + 1)
proofend;

theorem Th44: :: FIB_NUM2:44
for n being Element of NAT st n > 1 holds
Fib n < Fib (n + 1)
proofend;

theorem :: FIB_NUM2:45
for m, n being Nat st m >= n holds
Fib m >= Fib n
proofend;

theorem Th46: :: FIB_NUM2:46
for n, k being Nat st k > 1 &amp; k < n holds
Fib k < Fib n
proofend;

theorem Th47: :: FIB_NUM2:47
for k being Nat holds
( Fib k = 1 iff ( k = 1 or k = 2 ) )
proofend;

theorem Th48: :: FIB_NUM2:48
for k, n being Element of NAT st n > 1 &amp; k <> 0 &amp; k <> 1 holds
( Fib k = Fib n iff k = n )
proofend;

theorem Th49: :: FIB_NUM2:49
for n being Element of NAT st n > 1 &amp; n <> 4 &amp; not n is prime holds
ex k being non empty Element of NAT st
( k <> 1 &amp; k <> 2 &amp; k <> n &amp; k divides n )
proofend;

theorem :: FIB_NUM2:50
for n being Element of NAT st n > 1 &amp; n <> 4 &amp; Fib n is prime holds
n is prime
proofend;

begin

definition
func FIB  ->  Function of NAT,NAT means :Def2: :: FIB_NUM2:def 2
 for k being Element of NAT holds it . k = Fib k;
existence
 ex b1 being Function of NAT,NAT st
for k being Element of NAT holds b1 . k = Fib k
proofend;
uniqueness
 for b1, b2 being Function of NAT,NAT st ( for k being Element of NAT holds b1 . k = Fib k ) &amp; ( for k being Element of NAT holds b2 . k = Fib k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines FIB FIB_NUM2:def_2_:_
 for b1 being Function of NAT,NAT holds
( b1 = FIB iff for k being Element of NAT holds b1 . k = Fib k );

definition
func EvenNAT  ->  Subset of NAT equals :: FIB_NUM2:def 3
 {  (2 * k) where k is Element of NAT : verum  }  ;
coherence
  {  (2 * k) where k is Element of NAT : verum  }  is Subset of NAT
proofend;
func OddNAT  ->  Subset of NAT equals :: FIB_NUM2:def 4
 {  ((2 * k) + 1) where k is Element of NAT : verum  }  ;
coherence
  {  ((2 * k) + 1) where k is Element of NAT : verum  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines EvenNAT FIB_NUM2:def_3_:_
 EvenNAT =  {  (2 * k) where k is Element of NAT : verum  }  ;

:: deftheorem  defines OddNAT FIB_NUM2:def_4_:_
 OddNAT =  {  ((2 * k) + 1) where k is Element of NAT : verum  }  ;

theorem Th51: :: FIB_NUM2:51
for k being Element of NAT holds
( 2 * k in EvenNAT &amp; not (2 * k) + 1 in EvenNAT )
proofend;

theorem Th52: :: FIB_NUM2:52
for k being Element of NAT holds
( (2 * k) + 1 in OddNAT &amp; not 2 * k in OddNAT )
proofend;

definition
let n be Element of NAT ;
func EvenFibs n ->  FinSequence of NAT  equals :: FIB_NUM2:def 5
 Prefix (FIB,(EvenNAT /\ (Seg n)));
coherence
 Prefix (FIB,(EvenNAT /\ (Seg n))) is FinSequence of NAT ;
func OddFibs n ->  FinSequence of NAT  equals :: FIB_NUM2:def 6
 Prefix (FIB,(OddNAT /\ (Seg n)));
coherence
 Prefix (FIB,(OddNAT /\ (Seg n))) is FinSequence of NAT ;
end;

:: deftheorem  defines EvenFibs FIB_NUM2:def_5_:_
 for n being Element of NAT holds EvenFibs n = Prefix (FIB,(EvenNAT /\ (Seg n)));

:: deftheorem  defines OddFibs FIB_NUM2:def_6_:_
 for n being Element of NAT holds OddFibs n = Prefix (FIB,(OddNAT /\ (Seg n)));

theorem Th53: :: FIB_NUM2:53
EvenFibs 0 = {} ;

theorem :: FIB_NUM2:54
Seq (FIB | {2}) = <*1*>
proofend;

theorem Th55: :: FIB_NUM2:55
EvenFibs 2 = <*1*>
proofend;

theorem :: FIB_NUM2:56
EvenFibs 4 = <*1,3*>
proofend;

theorem Th57: :: FIB_NUM2:57
for k being Element of NAT holds (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4))
proofend;

theorem Th58: :: FIB_NUM2:58
for k being Element of NAT holds (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} = FIB | (EvenNAT /\ (Seg ((2 * k) + 4)))
proofend;

theorem Th59: :: FIB_NUM2:59
for n being Element of NAT holds EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>
proofend;

theorem Th60: :: FIB_NUM2:60
OddFibs 1 = <*1*>
proofend;

theorem Th61: :: FIB_NUM2:61
OddFibs 3 = <*1,2*>
proofend;

theorem Th62: :: FIB_NUM2:62
for k being Nat holds (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))
proofend;

theorem Th63: :: FIB_NUM2:63
for k being Nat holds (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))
proofend;

theorem Th64: :: FIB_NUM2:64
for n being Nat holds OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>
proofend;

theorem :: FIB_NUM2:65
for n being Element of NAT holds Sum (EvenFibs ((2 * n) + 2)) = (Fib ((2 * n) + 3)) - 1
proofend;

theorem :: FIB_NUM2:66
for n being Nat holds Sum (OddFibs ((2 * n) + 1)) = Fib ((2 * n) + 2)
proofend;

begin

theorem Th67: :: FIB_NUM2:67
for n being Element of NAT holds Fib n, Fib (n + 1) are_relative_prime
proofend;

theorem Th68: :: FIB_NUM2:68
for n being non empty Nat
for m being Nat st m <> 1 &amp; m divides Fib n holds
not m divides Fib (n -' 1)
proofend;

:: [WP: ] Carmichael's_Theorem_on_Prime_Divisors
theorem :: FIB_NUM2:69
for m being Nat
for n being non empty Nat st m is prime &amp; n is prime &amp; m divides Fib n holds
for r being Nat st r < n &amp; r <> 0 holds
not m divides Fib r
proofend;

begin

theorem :: FIB_NUM2:70
for n being non empty 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
proofend;