:: by Piotr Wojtecki and Adam Grabowski

::

:: Received May 24, 2004

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

theorem Th6: :: FIB_NUM3:6

for n being Element of NAT

for a being non zero Real holds (a to_power n) to_power 2 = a to_power (2 * n)

for a being non zero Real holds (a to_power n) to_power 2 = a to_power (2 * n)

proof end;

theorem Th8: :: FIB_NUM3:8

for n being Element of NAT

for a, b being non zero Real holds (a * b) to_power n = (a to_power n) * (b to_power n)

for a, b being non zero Real holds (a * b) to_power n = (a to_power n) * (b to_power n)

proof end;

registration
end;

definition

let n be Nat;

ex b_{1} being Element of NAT ex L being sequence of [:NAT,NAT:] st

( b_{1} = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )

for b_{1}, b_{2} being Element of NAT st ex L being sequence of [:NAT,NAT:] st

( b_{1} = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being sequence of [:NAT,NAT:] st

( b_{2} = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) holds

b_{1} = b_{2}

end;
:: Lucas numbers

func Lucas n -> Element of NAT means :Def1: :: FIB_NUM3:def 1

ex L being sequence of [:NAT,NAT:] st

( it = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) );

existence ex L being sequence of [:NAT,NAT:] st

( it = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def1 defines Lucas FIB_NUM3:def 1 :

for n being Nat

for b_{2} being Element of NAT holds

( b_{2} = Lucas n iff ex L being sequence of [:NAT,NAT:] st

( b_{2} = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) );

for n being Nat

for b

( b

( b

theorem Th11: :: FIB_NUM3:11

( Lucas 0 = 2 & Lucas 1 = 1 & ( for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1)) ) )

proof end;

registration
end;

theorem :: FIB_NUM3:26

for n, m being Element of NAT holds 2 * (Lucas (n + m)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m))

proof end;

theorem :: FIB_NUM3:27

for n being Element of NAT holds (Lucas (n + 3)) * (Lucas n) = ((Lucas (n + 2)) |^ 2) - ((Lucas (n + 1)) |^ 2)

proof end;

theorem :: FIB_NUM3:29

for n being Element of NAT holds 2 * (Fib ((2 * n) + 1)) = ((Lucas (n + 1)) * (Fib n)) + ((Lucas n) * (Fib (n + 1)))

proof end;

theorem :: FIB_NUM3:30

for n being Element of NAT holds (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))

proof end;

theorem :: FIB_NUM3:31

for n being Element of NAT holds Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n))

proof end;

definition

let a, b be Nat;

:: original: [

redefine func [a,b] -> Element of [:NAT,NAT:];

coherence

[a,b] is Element of [:NAT,NAT:]

end;
:: original: [

redefine func [a,b] -> Element of [:NAT,NAT:];

coherence

[a,b] is Element of [:NAT,NAT:]

proof end;

definition

let a, b, n be Nat;

ex b_{1} being Element of NAT ex L being sequence of [:NAT,NAT:] st

( b_{1} = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )

for b_{1}, b_{2} being Element of NAT st ex L being sequence of [:NAT,NAT:] st

( b_{1} = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being sequence of [:NAT,NAT:] st

( b_{2} = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) holds

b_{1} = b_{2}

end;
func GenFib (a,b,n) -> Element of NAT means :Def2: :: FIB_NUM3:def 2

ex L being sequence of [:NAT,NAT:] st

( it = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) );

existence ex L being sequence of [:NAT,NAT:] st

( it = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def2 defines GenFib FIB_NUM3:def 2 :

for a, b, n being Nat

for b_{4} being Element of NAT holds

( b_{4} = GenFib (a,b,n) iff ex L being sequence of [:NAT,NAT:] st

( b_{4} = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) );

for a, b, n being Nat

for b

( b

( b

theorem Th32: :: FIB_NUM3:32

for a, b being Nat holds

( GenFib (a,b,0) = a & GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )

( GenFib (a,b,0) = a & GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )

proof end;

theorem Th33: :: FIB_NUM3:33

for a, b being Element of NAT

for k being Nat holds ((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2 = (((GenFib (a,b,(k + 1))) |^ 2) + ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) |^ 2)

for k being Nat holds ((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2 = (((GenFib (a,b,(k + 1))) |^ 2) + ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) |^ 2)

proof end;

theorem Th36: :: FIB_NUM3:36

for a, b, n being Element of NAT holds (GenFib (a,b,(n + 2))) + (GenFib (a,b,(n + 3))) = GenFib (a,b,(n + 4))

proof end;

theorem Th39: :: FIB_NUM3:39

for a, b, n being Element of NAT holds (GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = 2 * (GenFib (a,b,(n + 2)))

proof end;

theorem :: FIB_NUM3:40

for a, b, n being Element of NAT holds (GenFib (a,b,n)) + (GenFib (a,b,(n + 4))) = 3 * (GenFib (a,b,(n + 2)))

proof end;

theorem :: FIB_NUM3:41

for a, b, n being Element of NAT holds (GenFib (a,b,(n + 3))) - (GenFib (a,b,n)) = 2 * (GenFib (a,b,(n + 1)))

proof end;

theorem :: FIB_NUM3:42

for a, b, n being non zero Element of NAT holds GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))

proof end;

theorem :: FIB_NUM3:43

for n, m being Nat holds ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib ((Fib 0),(Lucas 0),(n + m))

proof end;

theorem :: FIB_NUM3:47

for a, b, n being Element of NAT holds ((GenFib (a,b,(n + 2))) * (GenFib (a,b,n))) - ((GenFib (a,b,(n + 1))) |^ 2) = ((- 1) to_power n) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3))))

proof end;

theorem :: FIB_NUM3:48

for a, b, k, n being Element of NAT holds GenFib ((GenFib (a,b,k)),(GenFib (a,b,(k + 1))),n) = GenFib (a,b,(n + k))

proof end;

theorem :: FIB_NUM3:52

for a, b, c, d, n being Element of NAT holds (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n)

proof end;

theorem :: FIB_NUM3:54

for a, b, n being Element of NAT holds GenFib (a,b,n) = ((((a * (- tau_bar)) + b) * (tau to_power n)) + (((a * tau) - b) * (tau_bar to_power n))) / (sqrt 5)

proof end;

theorem :: FIB_NUM3:55

for a, n being Element of NAT holds GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = ((2 * a) + 1) * (Fib (n + 2))

proof end;