:: by Magdalena Jastrz\c{e}bska and Adam Grabowski

::

:: Received May 10, 2004

:: Copyright (c) 2004-2016 Association of Mizar Users

theorem Th4: :: FIB_NUM2:4

for m being non zero Real

for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)

for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)

proof end;

theorem Th6: :: FIB_NUM2:6

for n being Nat

for k being non zero Real

for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)

for k being non zero Real

for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)

proof end;

theorem Th8: :: FIB_NUM2:8

for k, m being Nat

for a being non zero Real holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)

for a being non zero Real holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)

proof end;

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)

for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds

k divides (m * m1) + (n * n1)

proof end;

registration

existence

ex b_{1} being set st

( b_{1} is finite & not b_{1} is empty & b_{1} is natural-membered & b_{1} is with_non-empty_elements )

end;
ex b

( b

proof end;

registration

let f be sequence of NAT;

let A be finite with_non-empty_elements natural-membered set ;

coherence

f | A is FinSubsequence-like

end;
let A be finite with_non-empty_elements natural-membered set ;

coherence

f | A is FinSubsequence-like

proof end;

definition

let f be sequence of NAT;

let A be finite with_non-empty_elements natural-membered set ;

coherence

Seq (f | A) is FinSequence of NAT

end;
let A be finite with_non-empty_elements natural-membered set ;

coherence

Seq (f | A) is FinSequence of NAT

proof end;

:: deftheorem defines Prefix FIB_NUM2:def 1 :

for f being sequence of NAT

for A being finite with_non-empty_elements natural-membered set holds Prefix (f,A) = Seq (f | A);

for f being sequence of NAT

for A being finite with_non-empty_elements natural-membered set holds Prefix (f,A) = Seq (f | A);

theorem Th16: :: FIB_NUM2:16

for i, j being Nat

for x, y being set

for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds

Seq q = <*x,y*>

for x, y being set

for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds

Seq q = <*x,y*>

proof end;

registration

let A be with_non-empty_elements set ;

coherence

for b_{1} being Subset of A holds b_{1} is with_non-empty_elements

end;
coherence

for b

proof end;

registration

let A be with_non-empty_elements set ;

let B be set ;

coherence

A /\ B is with_non-empty_elements

B /\ A is with_non-empty_elements ;

end;
let B be set ;

coherence

A /\ B is with_non-empty_elements

proof end;

coherence B /\ A is with_non-empty_elements ;

theorem Th18: :: FIB_NUM2:18

for i being Element of NAT

for y being set

for f being FinSubsequence st f = {[1,y]} holds

Shift (f,i) = {[(1 + i),y]}

for y being set

for f being FinSubsequence st f = {[1,y]} holds

Shift (f,i) = {[(1 + i),y]}

proof end;

theorem Th19: :: FIB_NUM2:19

for q being FinSubsequence

for k, n being Element of NAT st dom q c= Seg k & n > k holds

ex p being FinSequence st

( q c= p & dom p = Seg n )

for k, n being Element of NAT st dom q c= Seg k & n > k holds

ex p being FinSequence st

( q c= p & dom p = Seg n )

proof end;

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

proof end;

theorem :: FIB_NUM2:32

for n being non zero Element of NAT holds ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n

proof end;

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

proof end;

theorem :: FIB_NUM2:38

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)

((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)

proof end;

theorem Th40: :: FIB_NUM2:40

for n being Nat

for k being non zero Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))

for k being non zero Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))

proof end;

theorem Th49: :: FIB_NUM2:49

for n being Element of NAT st n > 1 & n <> 4 & not n is prime holds

ex k being non zero Element of NAT st

( k <> 1 & k <> 2 & k <> n & k divides n )

ex k being non zero Element of NAT st

( k <> 1 & k <> 2 & k <> n & k divides n )

proof end;

definition

ex b_{1} being sequence of NAT st

for k being Element of NAT holds b_{1} . k = Fib k

for b_{1}, b_{2} being sequence of NAT st ( for k being Element of NAT holds b_{1} . k = Fib k ) & ( for k being Element of NAT holds b_{2} . k = Fib k ) holds

b_{1} = b_{2}
end;

func FIB -> sequence of NAT means :Def2: :: FIB_NUM2:def 2

for k being Element of NAT holds it . k = Fib k;

existence for k being Element of NAT holds it . k = Fib k;

ex b

for k being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines FIB FIB_NUM2:def 2 :

for b_{1} being sequence of NAT holds

( b_{1} = FIB iff for k being Element of NAT holds b_{1} . k = Fib k );

for b

( b

definition

coherence

{ (2 * k) where k is Nat : verum } is Subset of NAT

{ ((2 * k) + 1) where k is Element of NAT : verum } is Subset of NAT

end;
{ (2 * k) where k is Nat : verum } is Subset of NAT

proof end;

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

{ ((2 * k) + 1) where k is Element of NAT : verum } is Subset of NAT

proof end;

:: deftheorem defines OddNAT FIB_NUM2:def 4 :

OddNAT = { ((2 * k) + 1) where k is Element of NAT : verum } ;

OddNAT = { ((2 * k) + 1) where k is Element of NAT : verum } ;

definition

let n be Nat;

coherence

Prefix (FIB,(EvenNAT /\ (Seg n))) is FinSequence of NAT ;

coherence

Prefix (FIB,(OddNAT /\ (Seg n))) is FinSequence of NAT ;

end;
coherence

Prefix (FIB,(EvenNAT /\ (Seg n))) is FinSequence of NAT ;

coherence

Prefix (FIB,(OddNAT /\ (Seg n))) is FinSequence of NAT ;

:: deftheorem defines EvenFibs FIB_NUM2:def 5 :

for n being Nat holds EvenFibs n = Prefix (FIB,(EvenNAT /\ (Seg n)));

for n being Nat holds EvenFibs n = Prefix (FIB,(EvenNAT /\ (Seg n)));

:: deftheorem defines OddFibs FIB_NUM2:def 6 :

for n being Nat holds OddFibs n = Prefix (FIB,(OddNAT /\ (Seg n)));

for n being Nat holds OddFibs n = Prefix (FIB,(OddNAT /\ (Seg n)));

theorem Th57: :: FIB_NUM2:57

for k being Nat holds (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4))

proof end;

theorem Th58: :: FIB_NUM2:58

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

theorem Th59: :: FIB_NUM2:59

for n being Element of NAT holds EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>

proof end;

theorem Th62: :: FIB_NUM2:62

for k being Nat holds (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))

proof end;

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

proof end;

theorem Th68: :: FIB_NUM2:68

for n being non zero Nat

for m being Nat st m <> 1 & m divides Fib n holds

not m divides Fib (n -' 1)

for m being Nat st m <> 1 & m divides Fib n holds

not m divides Fib (n -' 1)

proof end;

:: Carmichael's Theorem on Prime Divisors

theorem :: FIB_NUM2:69

for m being Nat

for n being non zero Nat st m is prime & n is prime & m divides Fib n holds

for r being Nat st r < n & r <> 0 holds

not m divides Fib r

for n being non zero Nat st m is prime & n is prime & m divides Fib n holds

for r being Nat st r < n & r <> 0 holds

not m divides Fib r

proof end;

theorem :: FIB_NUM2:70

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