:: Lucas Numbers and Generalized {F}ibonacci Numbers
:: by Piotr Wojtecki and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


theorem :: FIB_NUM3:1
for a being Real
for n being Element of NAT st a to_power n = 0 holds
a = 0
proof end;

theorem Th2: :: FIB_NUM3:2
for a being non negative Real holds (sqrt a) * (sqrt a) = a
proof end;

theorem Th3: :: FIB_NUM3:3
for a being Real holds a to_power 2 = (- a) to_power 2
proof end;

theorem Th4: :: FIB_NUM3:4
for k being non zero Nat holds (k -' 1) + 2 = (k + 2) -' 1
proof end;

theorem Th5: :: FIB_NUM3:5
for a, b being Element of NAT holds (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b)
proof end;

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

theorem Th7: :: FIB_NUM3:7
for a, b being Real holds (a + b) * (a - b) = (a to_power 2) - (b to_power 2)
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)
proof end;

registration
cluster tau -> positive ;
coherence
tau is positive by FIB_NUM2:33;
cluster tau_bar -> negative ;
coherence
tau_bar is negative by FIB_NUM2:36;
end;

theorem Th9: :: FIB_NUM3:9
for n being Nat holds (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2)
proof end;

theorem Th10: :: FIB_NUM3:10
for n being Nat holds (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2)
proof end;

deffunc H1( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];

definition
func Lucas -> sequence of [:NAT,NAT:] means :Def1: :: FIB_NUM3:def 1
( it . 0 = [2,1] & ( for n being Nat holds it . (n + 1) = [((it . n) `2),(((it . n) `1) + ((it . n) `2))] ) );
existence
ex b1 being sequence of [:NAT,NAT:] st
( b1 . 0 = [2,1] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) `2),(((b1 . n) `1) + ((b1 . n) `2))] ) )
proof end;
uniqueness
for b1, b2 being sequence of [:NAT,NAT:] st b1 . 0 = [2,1] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) `2),(((b1 . n) `1) + ((b1 . n) `2))] ) & b2 . 0 = [2,1] & ( for n being Nat holds b2 . (n + 1) = [((b2 . n) `2),(((b2 . n) `1) + ((b2 . n) `2))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Lucas FIB_NUM3:def 1 :
for b1 being sequence of [:NAT,NAT:] holds
( b1 = Lucas iff ( b1 . 0 = [2,1] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) `2),(((b1 . n) `1) + ((b1 . n) `2))] ) ) );

definition
let n be Nat;
:: WP: Lucas numbers
func Lucas n -> Element of NAT equals :: FIB_NUM3:def 2
(Lucas . n) `1 ;
coherence
(Lucas . n) `1 is Element of NAT ;
end;

:: deftheorem defines Lucas FIB_NUM3:def 2 :
for n being Nat holds Lucas n = (Lucas . n) `1 ;

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;

theorem Th12: :: FIB_NUM3:12
for n being Nat holds Lucas (n + 2) = (Lucas n) + (Lucas (n + 1))
proof end;

theorem Th13: :: FIB_NUM3:13
for n being Nat holds (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3)
proof end;

theorem Th14: :: FIB_NUM3:14
Lucas 2 = 3
proof end;

theorem Th15: :: FIB_NUM3:15
Lucas 3 = 4
proof end;

theorem Th16: :: FIB_NUM3:16
Lucas 4 = 7
proof end;

theorem Th17: :: FIB_NUM3:17
for k being Nat holds Lucas k >= k
proof end;

theorem :: FIB_NUM3:18
for m being non zero Element of NAT holds Lucas (m + 1) >= Lucas m
proof end;

registration
let n be Element of NAT ;
cluster Lucas n -> positive ;
coherence
Lucas n is positive
proof end;
end;

theorem :: FIB_NUM3:19
for n being Element of NAT holds 2 * (Lucas (n + 2)) = (Lucas n) + (Lucas (n + 3))
proof end;

theorem :: FIB_NUM3:20
for n being Nat holds Lucas (n + 1) = (Fib n) + (Fib (n + 2))
proof end;

theorem Th21: :: FIB_NUM3:21
for n being Nat holds Lucas n = (tau to_power n) + (tau_bar to_power n)
proof end;

theorem :: FIB_NUM3:22
for n being Nat holds (2 * (Lucas n)) + (Lucas (n + 1)) = 5 * (Fib (n + 1))
proof end;

theorem Th23: :: FIB_NUM3:23
for n being Nat holds (Lucas (n + 3)) - (2 * (Lucas n)) = 5 * (Fib n)
proof end;

theorem :: FIB_NUM3:24
for n being Nat holds (Lucas n) + (Fib n) = 2 * (Fib (n + 1))
proof end;

theorem :: FIB_NUM3:25
for n being Nat holds (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2))
proof 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 Th28: :: FIB_NUM3:28
for n being Nat holds Fib (2 * n) = (Fib n) * (Lucas n)
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:]
proof end;
end;

definition
let a, b be Nat;
deffunc H2( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
func GenFib (a,b) -> sequence of [:NAT,NAT:] means :Def2: :: FIB_NUM3:def 3
( it . 0 = [a,b] & ( for n being Nat holds it . (n + 1) = [((it . n) `2),(((it . n) `1) + ((it . n) `2))] ) );
existence
ex b1 being sequence of [:NAT,NAT:] st
( b1 . 0 = [a,b] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) `2),(((b1 . n) `1) + ((b1 . n) `2))] ) )
proof end;
uniqueness
for b1, b2 being sequence of [:NAT,NAT:] st b1 . 0 = [a,b] & ( for n being Nat holds b1 . (n + 1) = [((b1 . n) `2),(((b1 . n) `1) + ((b1 . n) `2))] ) & b2 . 0 = [a,b] & ( for n being Nat holds b2 . (n + 1) = [((b2 . n) `2),(((b2 . n) `1) + ((b2 . n) `2))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines GenFib FIB_NUM3:def 3 :
for a, b being Nat
for b3 being sequence of [:NAT,NAT:] holds
( b3 = GenFib (a,b) iff ( b3 . 0 = [a,b] & ( for n being Nat holds b3 . (n + 1) = [((b3 . n) `2),(((b3 . n) `1) + ((b3 . n) `2))] ) ) );

definition
let a, b, n be Nat;
func GenFib (a,b,n) -> Element of NAT equals :: FIB_NUM3:def 4
((GenFib (a,b)) . n) `1 ;
coherence
((GenFib (a,b)) . n) `1 is Element of NAT ;
end;

:: deftheorem defines GenFib FIB_NUM3:def 4 :
for a, b, n being Nat holds GenFib (a,b,n) = ((GenFib (a,b)) . n) `1 ;

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

theorem Th34: :: FIB_NUM3:34
for a, b, n being Nat holds (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2))
proof end;

theorem Th35: :: FIB_NUM3:35
for a, b, n being Nat holds (GenFib (a,b,(n + 1))) + (GenFib (a,b,(n + 2))) = GenFib (a,b,(n + 3))
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 :: FIB_NUM3:37
for n being Element of NAT holds GenFib (0,1,n) = Fib n
proof end;

theorem Th38: :: FIB_NUM3:38
for n being Element of NAT holds GenFib (2,1,n) = Lucas n
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:44
for n being Element of NAT holds (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))
proof end;

theorem :: FIB_NUM3:45
for a, n being Element of NAT holds GenFib (a,a,n) = ((GenFib (a,a,0)) / 2) * ((Fib n) + (Lucas n))
proof end;

theorem :: FIB_NUM3:46
for a, b, n being Element of NAT holds GenFib (b,(a + b),n) = GenFib (a,b,(n + 1))
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 Th49: :: FIB_NUM3:49
for a, b, n being Element of NAT holds GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1)))
proof end;

theorem :: FIB_NUM3:50
for b, n being Element of NAT holds GenFib (0,b,n) = b * (Fib n)
proof end;

theorem :: FIB_NUM3:51
for a, n being Element of NAT holds GenFib (a,0,(n + 1)) = a * (Fib n)
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:53
for a, b, k, n being Element of NAT holds GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,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;