:: FIB_NUM3 semantic presentation

theorem Th1: :: FIB_NUM3:1
for b1 being real number
for b2 being Nat st b1 to_power b2 = 0 holds
b1 = 0
proof end;

theorem Th2: :: FIB_NUM3:2
for b1 being real non negative number holds (sqrt b1) * (sqrt b1) = b1
proof end;

theorem Th3: :: FIB_NUM3:3
for b1 being non empty real number holds b1 to_power 2 = (- b1) to_power 2
proof end;

Lemma4: - 1 <> 0
;

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

theorem Th5: :: FIB_NUM3:5
for b1, b2 being Nat holds (b1 + b2) |^ 2 = (((b1 * b1) + (b1 * b2)) + (b1 * b2)) + (b2 * b2)
proof end;

Lemma7: tau_bar < 0
proof end;

theorem Th6: :: FIB_NUM3:6
for b1 being Nat
for b2 being non empty real number holds (b2 to_power b1) to_power 2 = b2 to_power (2 * b1)
proof end;

theorem Th7: :: FIB_NUM3:7
for b1, b2 being real number holds (b1 + b2) * (b1 - b2) = (b1 to_power 2) - (b2 to_power 2)
proof end;

theorem Th8: :: FIB_NUM3:8
for b1 being Nat
for b2, b3 being non empty real number holds (b2 * b3) to_power b1 = (b2 to_power b1) * (b3 to_power b1)
proof end;

registration
cluster tau -> positive ;
coherence
tau is positive by FIB_NUM2:35;
cluster tau_bar -> negative ;
coherence
tau_bar is negative by Lemma7;
end;

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

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

definition
let c1 be Nat;
func Lucas c1 -> Nat means :Def1: :: FIB_NUM3:def 1
ex b1 being Function of NAT ,[:NAT ,NAT :] st
( a2 = (b1 . a1) `1 & b1 . 0 = [2,1] & ( for b2 being Nat holds b1 . (b2 + 1) = [((b1 . b2) `2 ),(((b1 . b2) `1 ) + ((b1 . b2) `2 ))] ) );
existence
ex b1 being Natex b2 being Function of NAT ,[:NAT ,NAT :] st
( b1 = (b2 . c1) `1 & b2 . 0 = [2,1] & ( for b3 being Nat holds b2 . (b3 + 1) = [((b2 . b3) `2 ),(((b2 . b3) `1 ) + ((b2 . b3) `2 ))] ) )
proof end;
uniqueness
for b1, b2 being Nat st ex b3 being Function of NAT ,[:NAT ,NAT :] st
( b1 = (b3 . c1) `1 & b3 . 0 = [2,1] & ( for b4 being Nat holds b3 . (b4 + 1) = [((b3 . b4) `2 ),(((b3 . b4) `1 ) + ((b3 . b4) `2 ))] ) ) & ex b3 being Function of NAT ,[:NAT ,NAT :] st
( b2 = (b3 . c1) `1 & b3 . 0 = [2,1] & ( for b4 being Nat holds b3 . (b4 + 1) = [((b3 . b4) `2 ),(((b3 . b4) `1 ) + ((b3 . b4) `2 ))] ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Lucas FIB_NUM3:def 1 :
for b1, b2 being Nat holds
( b2 = Lucas b1 iff ex b3 being Function of NAT ,[:NAT ,NAT :] st
( b2 = (b3 . b1) `1 & b3 . 0 = [2,1] & ( for b4 being Nat holds b3 . (b4 + 1) = [((b3 . b4) `2 ),(((b3 . b4) `1 ) + ((b3 . b4) `2 ))] ) ) );

theorem Th11: :: FIB_NUM3:11
( Lucas 0 = 2 & Lucas 1 = 1 & ( for b1 being Nat holds Lucas ((b1 + 1) + 1) = (Lucas b1) + (Lucas (b1 + 1)) ) )
proof end;

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

theorem Th13: :: FIB_NUM3:13
for b1 being Nat holds (Lucas (b1 + 1)) + (Lucas (b1 + 2)) = Lucas (b1 + 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 b1 being Nat holds Lucas b1 >= b1
proof end;

theorem Th18: :: FIB_NUM3:18
for b1 being non empty Nat holds Lucas (b1 + 1) >= Lucas b1
proof end;

registration
let c1 be Nat;
cluster Lucas a1 -> positive ;
coherence
Lucas c1 is positive
proof end;
end;

theorem Th19: :: FIB_NUM3:19
for b1 being Nat holds 2 * (Lucas (b1 + 2)) = (Lucas b1) + (Lucas (b1 + 3))
proof end;

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

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

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

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

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

theorem Th25: :: FIB_NUM3:25
for b1 being Nat holds (3 * (Fib b1)) + (Lucas b1) = 2 * (Fib (b1 + 2))
proof end;

theorem Th26: :: FIB_NUM3:26
for b1, b2 being Nat holds 2 * (Lucas (b1 + b2)) = ((Lucas b1) * (Lucas b2)) + ((5 * (Fib b1)) * (Fib b2))
proof end;

theorem Th27: :: FIB_NUM3:27
for b1 being Nat holds (Lucas (b1 + 3)) * (Lucas b1) = ((Lucas (b1 + 2)) |^ 2) - ((Lucas (b1 + 1)) |^ 2)
proof end;

theorem Th28: :: FIB_NUM3:28
for b1 being Nat holds Fib (2 * b1) = (Fib b1) * (Lucas b1)
proof end;

theorem Th29: :: FIB_NUM3:29
for b1 being Nat holds 2 * (Fib ((2 * b1) + 1)) = ((Lucas (b1 + 1)) * (Fib b1)) + ((Lucas b1) * (Fib (b1 + 1)))
proof end;

theorem Th30: :: FIB_NUM3:30
for b1 being Nat holds (5 * ((Fib b1) |^ 2)) - ((Lucas b1) |^ 2) = 4 * ((- 1) to_power (b1 + 1))
proof end;

theorem Th31: :: FIB_NUM3:31
for b1 being Nat holds Fib ((2 * b1) + 1) = ((Fib (b1 + 1)) * (Lucas (b1 + 1))) - ((Fib b1) * (Lucas b1))
proof end;

definition
let c1, c2, c3 be Nat;
func GenFib c1,c2,c3 -> Nat means :Def2: :: FIB_NUM3:def 2
ex b1 being Function of NAT ,[:NAT ,NAT :] st
( a4 = (b1 . a3) `1 & b1 . 0 = [a1,a2] & ( for b2 being Nat holds b1 . (b2 + 1) = [((b1 . b2) `2 ),(((b1 . b2) `1 ) + ((b1 . b2) `2 ))] ) );
existence
ex b1 being Natex b2 being Function of NAT ,[:NAT ,NAT :] st
( b1 = (b2 . c3) `1 & b2 . 0 = [c1,c2] & ( for b3 being Nat holds b2 . (b3 + 1) = [((b2 . b3) `2 ),(((b2 . b3) `1 ) + ((b2 . b3) `2 ))] ) )
proof end;
uniqueness
for b1, b2 being Nat st ex b3 being Function of NAT ,[:NAT ,NAT :] st
( b1 = (b3 . c3) `1 & b3 . 0 = [c1,c2] & ( for b4 being Nat holds b3 . (b4 + 1) = [((b3 . b4) `2 ),(((b3 . b4) `1 ) + ((b3 . b4) `2 ))] ) ) & ex b3 being Function of NAT ,[:NAT ,NAT :] st
( b2 = (b3 . c3) `1 & b3 . 0 = [c1,c2] & ( for b4 being Nat holds b3 . (b4 + 1) = [((b3 . b4) `2 ),(((b3 . b4) `1 ) + ((b3 . b4) `2 ))] ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines GenFib FIB_NUM3:def 2 :
for b1, b2, b3, b4 being Nat holds
( b4 = GenFib b1,b2,b3 iff ex b5 being Function of NAT ,[:NAT ,NAT :] st
( b4 = (b5 . b3) `1 & b5 . 0 = [b1,b2] & ( for b6 being Nat holds b5 . (b6 + 1) = [((b5 . b6) `2 ),(((b5 . b6) `1 ) + ((b5 . b6) `2 ))] ) ) );

theorem Th32: :: FIB_NUM3:32
for b1, b2 being Nat holds
( GenFib b1,b2,0 = b1 & GenFib b1,b2,1 = b2 & ( for b3 being Nat holds GenFib b1,b2,((b3 + 1) + 1) = (GenFib b1,b2,b3) + (GenFib b1,b2,(b3 + 1)) ) )
proof end;

theorem Th33: :: FIB_NUM3:33
for b1, b2, b3 being Nat holds ((GenFib b1,b2,(b3 + 1)) + (GenFib b1,b2,((b3 + 1) + 1))) |^ 2 = (((GenFib b1,b2,(b3 + 1)) |^ 2) + ((2 * (GenFib b1,b2,(b3 + 1))) * (GenFib b1,b2,((b3 + 1) + 1)))) + ((GenFib b1,b2,((b3 + 1) + 1)) |^ 2)
proof end;

theorem Th34: :: FIB_NUM3:34
for b1, b2, b3 being Nat holds (GenFib b1,b2,b3) + (GenFib b1,b2,(b3 + 1)) = GenFib b1,b2,(b3 + 2)
proof end;

theorem Th35: :: FIB_NUM3:35
for b1, b2, b3 being Nat holds (GenFib b1,b2,(b3 + 1)) + (GenFib b1,b2,(b3 + 2)) = GenFib b1,b2,(b3 + 3)
proof end;

theorem Th36: :: FIB_NUM3:36
for b1, b2, b3 being Nat holds (GenFib b1,b2,(b3 + 2)) + (GenFib b1,b2,(b3 + 3)) = GenFib b1,b2,(b3 + 4)
proof end;

theorem Th37: :: FIB_NUM3:37
for b1 being Nat holds GenFib 0,1,b1 = Fib b1
proof end;

theorem Th38: :: FIB_NUM3:38
for b1 being Nat holds GenFib 2,1,b1 = Lucas b1
proof end;

theorem Th39: :: FIB_NUM3:39
for b1, b2, b3 being Nat holds (GenFib b1,b2,b3) + (GenFib b1,b2,(b3 + 3)) = 2 * (GenFib b1,b2,(b3 + 2))
proof end;

theorem Th40: :: FIB_NUM3:40
for b1, b2, b3 being Nat holds (GenFib b1,b2,b3) + (GenFib b1,b2,(b3 + 4)) = 3 * (GenFib b1,b2,(b3 + 2))
proof end;

theorem Th41: :: FIB_NUM3:41
for b1, b2, b3 being Nat holds (GenFib b1,b2,(b3 + 3)) - (GenFib b1,b2,b3) = 2 * (GenFib b1,b2,(b3 + 1))
proof end;

theorem Th42: :: FIB_NUM3:42
for b1, b2, b3 being non empty Nat holds GenFib b1,b2,b3 = ((GenFib b1,b2,0) * (Fib (b3 -' 1))) + ((GenFib b1,b2,1) * (Fib b3))
proof end;

theorem Th43: :: FIB_NUM3:43
for b1, b2 being Nat holds ((Fib b2) * (Lucas b1)) + ((Lucas b2) * (Fib b1)) = GenFib (Fib 0),(Lucas 0),(b1 + b2)
proof end;

theorem Th44: :: FIB_NUM3:44
for b1 being Nat holds (Lucas b1) + (Lucas (b1 + 3)) = 2 * (Lucas (b1 + 2))
proof end;

theorem Th45: :: FIB_NUM3:45
for b1, b2 being Nat holds GenFib b1,b1,b2 = ((GenFib b1,b1,0) / 2) * ((Fib b2) + (Lucas b2))
proof end;

theorem Th46: :: FIB_NUM3:46
for b1, b2, b3 being Nat holds GenFib b2,(b1 + b2),b3 = GenFib b1,b2,(b3 + 1)
proof end;

theorem Th47: :: FIB_NUM3:47
for b1, b2, b3 being Nat holds ((GenFib b1,b2,(b3 + 2)) * (GenFib b1,b2,b3)) - ((GenFib b1,b2,(b3 + 1)) |^ 2) = ((- 1) to_power b3) * (((GenFib b1,b2,2) |^ 2) - ((GenFib b1,b2,1) * (GenFib b1,b2,3)))
proof end;

theorem Th48: :: FIB_NUM3:48
for b1, b2, b3, b4 being Nat holds GenFib (GenFib b1,b2,b3),(GenFib b1,b2,(b3 + 1)),b4 = GenFib b1,b2,(b4 + b3)
proof end;

theorem Th49: :: FIB_NUM3:49
for b1, b2, b3 being Nat holds GenFib b1,b2,(b3 + 1) = (b1 * (Fib b3)) + (b2 * (Fib (b3 + 1)))
proof end;

theorem Th50: :: FIB_NUM3:50
for b1, b2 being Nat holds GenFib 0,b1,b2 = b1 * (Fib b2)
proof end;

theorem Th51: :: FIB_NUM3:51
for b1, b2 being Nat holds GenFib b1,0,(b2 + 1) = b1 * (Fib b2)
proof end;

theorem Th52: :: FIB_NUM3:52
for b1, b2, b3, b4, b5 being Nat holds (GenFib b1,b2,b5) + (GenFib b3,b4,b5) = GenFib (b1 + b3),(b2 + b4),b5
proof end;

theorem Th53: :: FIB_NUM3:53
for b1, b2, b3, b4 being Nat holds GenFib (b3 * b1),(b3 * b2),b4 = b3 * (GenFib b1,b2,b4)
proof end;

theorem Th54: :: FIB_NUM3:54
for b1, b2, b3 being Nat holds GenFib b1,b2,b3 = ((((b1 * (- tau_bar )) + b2) * (tau to_power b3)) + (((b1 * tau ) - b2) * (tau_bar to_power b3))) / (sqrt 5)
proof end;

theorem Th55: :: FIB_NUM3:55
for b1, b2 being Nat holds GenFib ((2 * b1) + 1),((2 * b1) + 1),(b2 + 1) = ((2 * b1) + 1) * (Fib (b2 + 2))
proof end;