:: FIB_NUM3 semantic presentation

theorem Th1: :: FIB_NUM3:1

for a being real number
for n being Nat st a to_power n = 0 holds
a = 0

proof end;

theorem Th2: :: FIB_NUM3:2

for a being real non negative number holds (sqrt a) * (sqrt a) = a

proof end;

theorem Th3: :: FIB_NUM3:3

for a being non empty real number holds a to_power 2 = (- a) to_power 2

proof end;

Lm1: - 1 <> 0
;

theorem Th4: :: FIB_NUM3:4

for k being non empty Nat holds (k -' 1) + 2 = (k + 2) -' 1

proof end;

theorem Th5: :: FIB_NUM3:5

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

proof end;

Lm2: tau_bar < 0

proof end;

theorem Th6: :: FIB_NUM3:6

for n being Nat
for a being non empty real number 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 number holds (a + b) * (a - b) = (a to_power 2) - (b to_power 2)

proof end;

theorem Th8: :: FIB_NUM3:8

for n being Nat
for a, b being non empty real number holds (a * b) to_power n = (a to_power n) * (b to_power n)

proof end;

registration

cluster tau -> positive ;
coherence by FIB_NUM2:35;
cluster tau_bar -> negative ;
coherence by Lm2;

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;

definition

let n be Nat;
func Lucas n -> Nat means :Def1: :: FIB_NUM3:def 1
ex L being Function of NAT ,[: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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Lucas FIB_NUM3:def 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 empty Nat holds Lucas (m + 1) >= Lucas m

proof end;

registration

let n be Nat;
cluster Lucas n -> positive ;
coherence

proof end;

end;

theorem :: FIB_NUM3:19

for n being 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 Nat holds 2 * (Lucas (n + m)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m))

proof end;

theorem :: FIB_NUM3:27

for n being 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 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 Nat holds (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))

proof end;

theorem :: FIB_NUM3:31

for n being Nat holds Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n))

proof end;

definition

let a, b, n be Nat;
func GenFib a,b,n -> Nat means :Def2: :: FIB_NUM3:def 2
ex L being Function of NAT ,[: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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines GenFib FIB_NUM3:def 2 :

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, 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 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 Nat holds GenFib 0,1,n = Fib n

proof end;

theorem Th38: :: FIB_NUM3:38

for n being Nat holds GenFib 2,1,n = Lucas n

proof end;

theorem Th39: :: FIB_NUM3:39

for a, b, n being 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 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 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 empty 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 Nat holds (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))

proof end;

theorem :: FIB_NUM3:45

for a, n being 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 Nat holds GenFib b,(a + b),n = GenFib a,b,(n + 1)

proof end;

theorem :: FIB_NUM3:47

for a, b, n being 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 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 Nat holds GenFib a,b,(n + 1) = (a * (Fib n)) + (b * (Fib (n + 1)))

proof end;

theorem :: FIB_NUM3:50

for b, n being Nat holds GenFib 0,b,n = b * (Fib n)

proof end;

theorem :: FIB_NUM3:51

for a, n being Nat holds GenFib a,0,(n + 1) = a * (Fib n)

proof end;

theorem :: FIB_NUM3:52

for a, b, c, d, n being 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 Nat holds GenFib (k * a),(k * b),n = k * (GenFib a,b,n)

proof end;

theorem :: FIB_NUM3:54

for a, b, n being 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 Nat holds GenFib ((2 * a) + 1),((2 * a) + 1),(n + 1) = ((2 * a) + 1) * (Fib (n + 2))

proof end;